Theorem: bottcherNear_le (Ray/Dynamics/BottcherNear.lean)

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (bottcherNear f d z) ≤ 3 * Complex.abs z
Tactic:
simp only [bottcherNear, Complex.abs.map_mul]
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs z * Complex.abs (∏' (n : ℕ), term f d n z) ≤ 3 * Complex.abs z

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs z * Complex.abs (∏' (n : ℕ), term f d n z) ≤ 3 * Complex.abs z
Tactic:
rw [mul_comm]
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (∏' (n : ℕ), term f d n z) * Complex.abs z ≤ 3 * Complex.abs z

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (∏' (n : ℕ), term f d n z) * Complex.abs z ≤ 3 * Complex.abs z
Tactic:
refine mul_le_mul_of_nonneg_right ?_ (Complex.abs.nonneg _)
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (∏' (n : ℕ), term f d n z) ≤ 3

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
⊢ Complex.abs (∏' (n : ℕ), term f d n z) ≤ 3
Tactic:
rcases term_prod_exists s _ zt with ⟨p, h⟩
State after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
h : HasProd (fun n => term f d n z) p
⊢ Complex.abs (∏' (n : ℕ), term f d n z) ≤ 3

State before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
h : HasProd (fun n => term f d n z) p
⊢ Complex.abs (∏' (n : ℕ), term f d n z) ≤ 3
Tactic:
rw [h.tprod_eq]
State after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
h : HasProd (fun n => term f d n z) p
⊢ Complex.abs p ≤ 3

State before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
h : HasProd (fun n => term f d n z) p
⊢ Complex.abs p ≤ 3
Tactic:
simp only [HasProd] at h
State after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
h : Tendsto (fun s => s.prod fun x => term f d x z) atTop (𝓝 p)
⊢ Complex.abs p ≤ 3

State before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
h : Tendsto (fun s => s.prod fun x => term f d x z) atTop (𝓝 p)
⊢ Complex.abs p ≤ 3
Tactic:
apply le_of_tendsto' (Filter.Tendsto.comp Complex.continuous_abs.continuousAt h)
State after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
h : Tendsto (fun s => s.prod fun x => term f d x z) atTop (𝓝 p)
⊢ ∀ (c : Finset ℕ), (⇑Complex.abs ∘ fun s => s.prod fun x => term f d x z) c ≤ 3

State before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
h : Tendsto (fun s => s.prod fun x => term f d x z) atTop (𝓝 p)
⊢ ∀ (c : Finset ℕ), (⇑Complex.abs ∘ fun s => s.prod fun x => term f d x z) c ≤ 3
Tactic:
intro A
State after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
h : Tendsto (fun s => s.prod fun x => term f d x z) atTop (𝓝 p)
A : Finset ℕ
⊢ (⇑Complex.abs ∘ fun s => s.prod fun x => term f d x z) A ≤ 3

State before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
h : Tendsto (fun s => s.prod fun x => term f d x z) atTop (𝓝 p)
A : Finset ℕ
⊢ (⇑Complex.abs ∘ fun s => s.prod fun x => term f d x z) A ≤ 3
Tactic:
clear h
State after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
⊢ (⇑Complex.abs ∘ fun s => s.prod fun x => term f d x z) A ≤ 3

State before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
⊢ (⇑Complex.abs ∘ fun s => s.prod fun x => term f d x z) A ≤ 3
Tactic:
simp only [Function.comp, Complex.abs.map_prod]
State after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
⊢ (A.prod fun i => Complex.abs (term f d i z)) ≤ 3

State before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
⊢ (A.prod fun i => Complex.abs (term f d i z)) ≤ 3
Tactic:
have tb : ∀ n, abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2 : ℝ) ^ n := by
  intro n
  calc abs (term f d n z)
    _ = abs (1 + (term f d n z - 1)) := by ring_nf
    _ ≤ Complex.abs 1 + abs (term f d n z - 1) := by bound
    _ = 1 + abs (term f d n z - 1) := by norm_num
    _ ≤ 1 + 1 / 2 * (1 / 2 : ℝ) ^ n := by bound [term_converges s n zt]
State after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
⊢ (A.prod fun i => Complex.abs (term f d i z)) ≤ 3

State before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
⊢ (A.prod fun i => Complex.abs (term f d i z)) ≤ 3
Tactic:
have p : ∀ n : ℕ, 0 < (1 : ℝ) + 1 / 2 * (1 / 2 : ℝ) ^ n := fun _ ↦ add_pos (by bound) (by bound)
State after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
⊢ (A.prod fun i => Complex.abs (term f d i z)) ≤ 3

State before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
⊢ (A.prod fun i => Complex.abs (term f d i z)) ≤ 3
Tactic:
have lb : ∀ n : ℕ, Real.log ((1 : ℝ) + 1 / 2 * (1 / 2 : ℝ) ^ n) ≤ 1 / 2 * (1 / 2 : ℝ) ^ n :=
  fun n ↦ le_trans (Real.log_le_sub_one_of_pos (p n)) (le_of_eq (by ring))
State after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
⊢ (A.prod fun i => Complex.abs (term f d i z)) ≤ 3

State before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
⊢ (A.prod fun i => Complex.abs (term f d i z)) ≤ 3
Tactic:
refine le_trans (Finset.prod_le_prod (fun _ _ ↦ Complex.abs.nonneg _) fun n _ ↦ tb n) ?_
State after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
⊢ (A.prod fun i => 1 + 1 / 2 * (1 / 2) ^ i) ≤ 3

State before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
⊢ (A.prod fun i => 1 + 1 / 2 * (1 / 2) ^ i) ≤ 3
Tactic:
rw [← Real.exp_log (Finset.prod_pos fun n _ ↦ p n), Real.log_prod _ _ fun n _ ↦ (p n).ne']
State after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
⊢ (A.sum fun i => (1 + 1 / 2 * (1 / 2) ^ i).log).exp ≤ 3

State before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
⊢ (A.sum fun i => (1 + 1 / 2 * (1 / 2) ^ i).log).exp ≤ 3
Tactic:
refine le_trans (Real.exp_le_exp.mpr (Finset.sum_le_sum fun n _ ↦ lb n)) ?_
State after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
⊢ (A.sum fun i => 1 / 2 * (1 / 2) ^ i).exp ≤ 3

State before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
⊢ (A.sum fun i => 1 / 2 * (1 / 2) ^ i).exp ≤ 3
Tactic:
refine le_trans (Real.exp_le_exp.mpr ?_) Real.exp_one_lt_3.le
State after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
⊢ (A.sum fun i => 1 / 2 * (1 / 2) ^ i) ≤ 1

State before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
⊢ (A.sum fun i => 1 / 2 * (1 / 2) ^ i) ≤ 1
Tactic:
have geom := partial_scaled_geometric_bound (1 / 2) A one_half_pos.le one_half_lt_one
State after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
geom : (A.sum fun n => ↑(1 / 2) * (1 / 2) ^ n) ≤ ↑(1 / 2) * (1 - 1 / 2)⁻¹
⊢ (A.sum fun i => 1 / 2 * (1 / 2) ^ i) ≤ 1

State before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
geom : (A.sum fun n => ↑(1 / 2) * (1 / 2) ^ n) ≤ ↑(1 / 2) * (1 - 1 / 2)⁻¹
⊢ (A.sum fun i => 1 / 2 * (1 / 2) ^ i) ≤ 1
Tactic:
simp only [NNReal.coe_div, NNReal.coe_one, NNReal.coe_two] at geom
State after:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
geom : (A.sum fun x => 1 / 2 * (1 / 2) ^ x) ≤ 1 / 2 * (1 - 1 / 2)⁻¹
⊢ (A.sum fun i => 1 / 2 * (1 / 2) ^ i) ≤ 1

State before:
case intro
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
geom : (A.sum fun x => 1 / 2 * (1 / 2) ^ x) ≤ 1 / 2 * (1 - 1 / 2)⁻¹
⊢ (A.sum fun i => 1 / 2 * (1 / 2) ^ i) ≤ 1
Tactic:
exact le_trans geom (by norm_num)
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
⊢ ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
Tactic:
intro n
State after:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
n : ℕ
⊢ Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
n : ℕ
⊢ Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
Tactic:
calc abs (term f d n z)
  _ = abs (1 + (term f d n z - 1)) := by ring_nf
  _ ≤ Complex.abs 1 + abs (term f d n z - 1) := by bound
  _ = 1 + abs (term f d n z - 1) := by norm_num
  _ ≤ 1 + 1 / 2 * (1 / 2 : ℝ) ^ n := by bound [term_converges s n zt]
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
n : ℕ
⊢ Complex.abs (term f d n z) = Complex.abs (1 + (term f d n z - 1))
Tactic:
ring_nf
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
n : ℕ
⊢ Complex.abs (1 + (term f d n z - 1)) ≤ Complex.abs 1 + Complex.abs (term f d n z - 1)
Tactic:
bound
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
n : ℕ
⊢ Complex.abs 1 + Complex.abs (term f d n z - 1) = 1 + Complex.abs (term f d n z - 1)
Tactic:
norm_num
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
n : ℕ
⊢ 1 + Complex.abs (term f d n z - 1) ≤ 1 + 1 / 2 * (1 / 2) ^ n
Tactic:
bound [term_converges s n zt]
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
x✝ : ℕ
⊢ 0 < 1
Tactic:
bound
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
x✝ : ℕ
⊢ 0 < 1 / 2 * (1 / 2) ^ x✝
Tactic:
bound
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
n : ℕ
⊢ 1 + 1 / 2 * (1 / 2) ^ n - 1 = 1 / 2 * (1 / 2) ^ n
Tactic:
ring
State after:
no goals

State before:
f : ℂ → ℂ
d : ℕ
z : ℂ
t : Set ℂ
s : SuperNear f d t
zt : z ∈ t
p✝ : ℂ
A : Finset ℕ
tb : ∀ (n : ℕ), Complex.abs (term f d n z) ≤ 1 + 1 / 2 * (1 / 2) ^ n
p : ∀ (n : ℕ), 0 < 1 + 1 / 2 * (1 / 2) ^ n
lb : ∀ (n : ℕ), (1 + 1 / 2 * (1 / 2) ^ n).log ≤ 1 / 2 * (1 / 2) ^ n
geom : (A.sum fun x => 1 / 2 * (1 / 2) ^ x) ≤ 1 / 2 * (1 - 1 / 2)⁻¹
⊢ 1 / 2 * (1 - 1 / 2)⁻¹ ≤ 1
Tactic:
norm_num
State after:
no goals