[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
⊢ Monotone fun s => posTangentConeAt s a
[PROOFSTEP]
rintro s t hst y ⟨c, d, hd, hc, hcd⟩
[GOAL]
case intro.intro.intro.intro
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s t : Set E
hst : s ≤ t
y : E
c : ℕ → ℝ
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
⊢ y ∈ (fun s => posTangentConeAt s a) t
[PROOFSTEP]
exact ⟨c, d, mem_of_superset hd fun h hn => hst hn, hc, hcd⟩
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
x y : E
h : segment ℝ x y ⊆ s
⊢ y - x ∈ posTangentConeAt s x
[PROOFSTEP]
let c := fun n : ℕ => (2 : ℝ) ^ n
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
x y : E
h : segment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ n
⊢ y - x ∈ posTangentConeAt s x
[PROOFSTEP]
let d := fun n : ℕ => (c n)⁻¹ • (y - x)
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
x y : E
h : segment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ n
d : ℕ → E := fun n => (c n)⁻¹ • (y - x)
⊢ y - x ∈ posTangentConeAt s x
[PROOFSTEP]
refine' ⟨c, d, Filter.univ_mem' fun n => h _, tendsto_pow_atTop_atTop_of_one_lt one_lt_two, _⟩
[GOAL]
case refine'_1
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
x y : E
h : segment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ n
d : ℕ → E := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ x + d n ∈ segment ℝ x y
case refine'_2
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
x y : E
h : segment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ n
d : ℕ → E := fun n => (c n)⁻¹ • (y - x)
⊢ Tendsto (fun n => c n • d n) atTop (𝓝 (y - x))
[PROOFSTEP]
show x + d n ∈ segment ℝ x y
[GOAL]
case refine'_1
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
x y : E
h : segment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ n
d : ℕ → E := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ x + d n ∈ segment ℝ x y
[PROOFSTEP]
rw [segment_eq_image']
[GOAL]
case refine'_1
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
x y : E
h : segment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ n
d : ℕ → E := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ x + d n ∈ (fun θ => x + θ • (y - x)) '' Icc 0 1
[PROOFSTEP]
refine' ⟨(c n)⁻¹, ⟨_, _⟩, rfl⟩
[GOAL]
case refine'_1.refine'_1
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
x y : E
h : segment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ n
d : ℕ → E := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ 0 ≤ (c n)⁻¹
case refine'_1.refine'_2
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
x y : E
h : segment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ n
d : ℕ → E := fun n => (c n)⁻¹ • (y - x)
n : ℕ
⊢ (c n)⁻¹ ≤ 1
[PROOFSTEP]
exacts [inv_nonneg.2 (pow_nonneg zero_le_two _), inv_le_one (one_le_pow_of_one_le one_le_two _)]
[GOAL]
case refine'_2
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
x y : E
h : segment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ n
d : ℕ → E := fun n => (c n)⁻¹ • (y - x)
⊢ Tendsto (fun n => c n • d n) atTop (𝓝 (y - x))
[PROOFSTEP]
show Tendsto (fun n => c n • d n) atTop (𝓝 (y - x))
[GOAL]
case refine'_2
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
x y : E
h : segment ℝ x y ⊆ s
c : ℕ → ℝ := fun n => 2 ^ n
d : ℕ → E := fun n => (c n)⁻¹ • (y - x)
⊢ Tendsto (fun n => c n • d n) atTop (𝓝 (y - x))
[PROOFSTEP]
exact tendsto_const_nhds.congr fun n ↦ (smul_inv_smul₀ (pow_ne_zero _ two_ne_zero) _).symm
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
x y : E
h : segment ℝ x (x + y) ⊆ s
⊢ y ∈ posTangentConeAt s x
[PROOFSTEP]
simpa only [add_sub_cancel'] using mem_posTangentConeAt_of_segment_subset h
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
y : E
hy : y ∈ posTangentConeAt s a
⊢ ↑f' y ≤ 0
[PROOFSTEP]
rcases hy with ⟨c, d, hd, hc, hcd⟩
[GOAL]
case intro.intro.intro.intro
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
y : E
c : ℕ → ℝ
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
⊢ ↑f' y ≤ 0
[PROOFSTEP]
have hc' : Tendsto (‖c ·‖) atTop atTop := tendsto_abs_atTop_atTop.comp hc
[GOAL]
case intro.intro.intro.intro
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
y : E
c : ℕ → ℝ
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
hc' : Tendsto (fun x => ‖c x‖) atTop atTop
⊢ ↑f' y ≤ 0
[PROOFSTEP]
suffices : ∀ᶠ n in atTop, c n • (f (a + d n) - f a) ≤ 0
[GOAL]
case intro.intro.intro.intro
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
y : E
c : ℕ → ℝ
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
hc' : Tendsto (fun x => ‖c x‖) atTop atTop
this : ∀ᶠ (n : ℕ) in atTop, c n • (f (a + d n) - f a) ≤ 0
⊢ ↑f' y ≤ 0
[PROOFSTEP]
exact le_of_tendsto (hf.lim atTop hd hc' hcd) this
[GOAL]
case this
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
y : E
c : ℕ → ℝ
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
hc' : Tendsto (fun x => ‖c x‖) atTop atTop
⊢ ∀ᶠ (n : ℕ) in atTop, c n • (f (a + d n) - f a) ≤ 0
[PROOFSTEP]
replace hd : Tendsto (fun n => a + d n) atTop (𝓝[s] (a + 0))
[GOAL]
case hd
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
y : E
c : ℕ → ℝ
d : ℕ → E
hd : ∀ᶠ (n : ℕ) in atTop, a + d n ∈ s
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
hc' : Tendsto (fun x => ‖c x‖) atTop atTop
⊢ Tendsto (fun n => a + d n) atTop (𝓝[s] (a + 0))
[PROOFSTEP]
exact tendsto_nhdsWithin_iff.2 ⟨tendsto_const_nhds.add (tangentConeAt.lim_zero _ hc' hcd), hd⟩
[GOAL]
case this
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
y : E
c : ℕ → ℝ
d : ℕ → E
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
hc' : Tendsto (fun x => ‖c x‖) atTop atTop
hd : Tendsto (fun n => a + d n) atTop (𝓝[s] (a + 0))
⊢ ∀ᶠ (n : ℕ) in atTop, c n • (f (a + d n) - f a) ≤ 0
[PROOFSTEP]
rw [add_zero] at hd 
[GOAL]
case this
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
y : E
c : ℕ → ℝ
d : ℕ → E
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
hc' : Tendsto (fun x => ‖c x‖) atTop atTop
hd : Tendsto (fun n => a + d n) atTop (𝓝[s] a)
⊢ ∀ᶠ (n : ℕ) in atTop, c n • (f (a + d n) - f a) ≤ 0
[PROOFSTEP]
filter_upwards [hd.eventually h, hc.eventually_ge_atTop 0] with n hfn hcn
[GOAL]
case h
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
y : E
c : ℕ → ℝ
d : ℕ → E
hc : Tendsto c atTop atTop
hcd : Tendsto (fun n => c n • d n) atTop (𝓝 y)
hc' : Tendsto (fun x => ‖c x‖) atTop atTop
hd : Tendsto (fun n => a + d n) atTop (𝓝[s] a)
n : ℕ
hfn : f (a + d n) ≤ f a
hcn : 0 ≤ c n
⊢ c n • (f (a + d n) - f a) ≤ 0
[PROOFSTEP]
exact mul_nonpos_of_nonneg_of_nonpos hcn (sub_nonpos.2 hfn)
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
y : E
hy : y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ ↑(fderivWithin ℝ f s a) y ≤ 0
[PROOFSTEP]
rw [fderivWithin_zero_of_not_differentiableWithinAt hf]
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
y : E
hy : y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ ↑0 y ≤ 0
[PROOFSTEP]
rfl
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
hf : HasFDerivWithinAt f f' s a
y : E
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
⊢ 0 ≤ ↑f' y
[PROOFSTEP]
simpa using h.hasFDerivWithinAt_nonpos hf hy'
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
y : E
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ ↑(fderivWithin ℝ f s a) y = 0
[PROOFSTEP]
rw [fderivWithin_zero_of_not_differentiableWithinAt hf]
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMaxOn f s a
y : E
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ ↑0 y = 0
[PROOFSTEP]
rfl
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMinOn f s a
hf : HasFDerivWithinAt f f' s a
y : E
hy : y ∈ posTangentConeAt s a
⊢ 0 ≤ ↑f' y
[PROOFSTEP]
simpa using h.neg.hasFDerivWithinAt_nonpos hf.neg hy
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMinOn f s a
y : E
hy : y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 ≤ ↑(fderivWithin ℝ f s a) y
[PROOFSTEP]
rw [fderivWithin_zero_of_not_differentiableWithinAt hf]
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMinOn f s a
y : E
hy : y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 ≤ ↑0 y
[PROOFSTEP]
rfl
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMinOn f s a
hf : HasFDerivWithinAt f f' s a
y : E
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
⊢ ↑f' y = 0
[PROOFSTEP]
simpa using h.neg.hasFDerivWithinAt_eq_zero hf.neg hy hy'
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMinOn f s a
y : E
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ ↑(fderivWithin ℝ f s a) y = 0
[PROOFSTEP]
rw [fderivWithin_zero_of_not_differentiableWithinAt hf]
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
s : Set E
h : IsLocalMinOn f s a
y : E
hy : y ∈ posTangentConeAt s a
hy' : -y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ ↑0 y = 0
[PROOFSTEP]
rfl
[GOAL]
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
h : IsLocalMin f a
hf : HasFDerivAt f f' a
⊢ f' = 0
[PROOFSTEP]
ext y
[GOAL]
case h
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ ↑f' y = ↑0 y
[PROOFSTEP]
apply (h.on univ).hasFDerivWithinAt_eq_zero hf.hasFDerivWithinAt
[GOAL]
case h.hy
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ y ∈ posTangentConeAt univ a
[PROOFSTEP]
rw [posTangentConeAt_univ]
[GOAL]
case h.hy'
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ -y ∈ posTangentConeAt univ a
[PROOFSTEP]
rw [posTangentConeAt_univ]
[GOAL]
case h.hy
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ y ∈ univ
[PROOFSTEP]
apply mem_univ
[GOAL]
case h.hy'
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
a : E
f' : E →L[ℝ] ℝ
h : IsLocalMin f a
hf : HasFDerivAt f f' a
y : E
⊢ -y ∈ univ
[PROOFSTEP]
apply mem_univ
[GOAL]
f : ℝ → ℝ
f' a b : ℝ
h : IsLocalMin f a
hf : HasDerivAt f f' a
⊢ f' = 0
[PROOFSTEP]
simpa using FunLike.congr_fun (h.hasFDerivAt_eq_zero (hasDerivAt_iff_hasFDerivAt.1 hf)) 1
