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
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
let c := fun n : ℕ => (2 : ℝ) ^ n
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
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
let d := fun n : ℕ => (c n)⁻¹ • (y - x)
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))
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
refine' ⟨c, d, Filter.univ_mem' fun n => h _, tendsto_pow_atTop_atTop_of_one_lt one_lt_two, _⟩
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))
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))
show 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))
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))
show Tendsto (fun n => c n • d n) atTop (𝓝 (y - x))
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
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
rw [segment_eq_image']
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
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
refine' ⟨(c n)⁻¹, ⟨_, _⟩, rfl⟩
no goals
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
exacts [inv_nonneg.2 (pow_nonneg zero_le_two _), inv_le_one (one_le_pow_of_one_le one_le_two _)]
no goals
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))
exact tendsto_const_nhds.congr fun n ↦ (smul_inv_smul₀ (pow_ne_zero _ two_ne_zero) _).symm