Theorem: bottcher_approx_z (Ray/Dynamics/Multibrot/Bottcher.lean)

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
⊢ Complex.abs (⋯.bottcher c ↑z - z⁻¹) ≤ 16 * (Complex.abs z)⁻¹ ^ 2
Tactic:
set s := superF d
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
⊢ Complex.abs (s.bottcher c ↑z - z⁻¹) ≤ 16 * (Complex.abs z)⁻¹ ^ 2

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
⊢ Complex.abs (s.bottcher c ↑z - z⁻¹) ≤ 16 * (Complex.abs z)⁻¹ ^ 2
Tactic:
have i8 : (abs z)⁻¹ ≤ 1 / 8 := by
  rw [one_div]; apply inv_le_inv_of_le; norm_num
  exact le_trans (by norm_num) (le_trans c16.le cz)
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
⊢ Complex.abs (s.bottcher c ↑z - z⁻¹) ≤ 16 * (Complex.abs z)⁻¹ ^ 2

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
⊢ Complex.abs (s.bottcher c ↑z - z⁻¹) ≤ 16 * (Complex.abs z)⁻¹ ^ 2
Tactic:
simp only [bottcher_eq_bottcherNear_z c16 cz, bottcherNear, Complex.abs.map_mul, ← mul_sub_one,
  pow_two, ← mul_assoc, map_inv₀, mul_comm (abs z)⁻¹]
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
⊢ Complex.abs (∏' (n : ℕ), term (fl (f d) ∞ c) d n z⁻¹ - 1) * (Complex.abs z)⁻¹ ≤
    16 * (Complex.abs z)⁻¹ * (Complex.abs z)⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
⊢ Complex.abs (∏' (n : ℕ), term (fl (f d) ∞ c) d n z⁻¹ - 1) * (Complex.abs z)⁻¹ ≤
    16 * (Complex.abs z)⁻¹ * (Complex.abs z)⁻¹
Tactic:
refine mul_le_mul_of_nonneg_right ?_ (inv_nonneg.mpr (Complex.abs.nonneg _))
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
⊢ Complex.abs (∏' (n : ℕ), term (fl (f d) ∞ c) d n z⁻¹ - 1) ≤ 16 * (Complex.abs z)⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
⊢ Complex.abs (∏' (n : ℕ), term (fl (f d) ∞ c) d n z⁻¹ - 1) ≤ 16 * (Complex.abs z)⁻¹
Tactic:
rcases term_prod_exists (superNearF d c) _ (inv_mem_t c16 cz) with ⟨p, h⟩
State after:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
h : HasProd (fun n => term (fl (f d) ∞ c) d n z⁻¹) p
⊢ Complex.abs (∏' (n : ℕ), term (fl (f d) ∞ c) d n z⁻¹ - 1) ≤ 16 * (Complex.abs z)⁻¹

State before:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
h : HasProd (fun n => term (fl (f d) ∞ c) d n z⁻¹) p
⊢ Complex.abs (∏' (n : ℕ), term (fl (f d) ∞ c) d n z⁻¹ - 1) ≤ 16 * (Complex.abs z)⁻¹
Tactic:
rw [h.tprod_eq]
State after:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
h : HasProd (fun n => term (fl (f d) ∞ c) d n z⁻¹) p
⊢ Complex.abs (p - 1) ≤ 16 * (Complex.abs z)⁻¹

State before:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
h : HasProd (fun n => term (fl (f d) ∞ c) d n z⁻¹) p
⊢ Complex.abs (p - 1) ≤ 16 * (Complex.abs z)⁻¹
Tactic:
simp only [HasProd] at h
State after:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
h : Tendsto (fun s => s.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) Filter.atTop (𝓝 p)
⊢ Complex.abs (p - 1) ≤ 16 * (Complex.abs z)⁻¹

State before:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
h : Tendsto (fun s => s.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) Filter.atTop (𝓝 p)
⊢ Complex.abs (p - 1) ≤ 16 * (Complex.abs z)⁻¹
Tactic:
apply le_of_tendsto' (Filter.Tendsto.comp Complex.continuous_abs.continuousAt (h.sub_const 1))
State after:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
h : Tendsto (fun s => s.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) Filter.atTop (𝓝 p)
⊢ ∀ (c_1 : Finset ℕ),
    (⇑Complex.abs ∘ fun x => (x.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) - 1) c_1 ≤ 16 * (Complex.abs z)⁻¹

State before:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
h : Tendsto (fun s => s.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) Filter.atTop (𝓝 p)
⊢ ∀ (c_1 : Finset ℕ),
    (⇑Complex.abs ∘ fun x => (x.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) - 1) c_1 ≤ 16 * (Complex.abs z)⁻¹
Tactic:
clear h
State after:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
⊢ ∀ (c_1 : Finset ℕ),
    (⇑Complex.abs ∘ fun x => (x.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) - 1) c_1 ≤ 16 * (Complex.abs z)⁻¹

State before:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
⊢ ∀ (c_1 : Finset ℕ),
    (⇑Complex.abs ∘ fun x => (x.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) - 1) c_1 ≤ 16 * (Complex.abs z)⁻¹
Tactic:
intro A
State after:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ (⇑Complex.abs ∘ fun x => (x.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) - 1) A ≤ 16 * (Complex.abs z)⁻¹

State before:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ (⇑Complex.abs ∘ fun x => (x.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) - 1) A ≤ 16 * (Complex.abs z)⁻¹
Tactic:
simp only [Function.comp]
State after:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ Complex.abs ((A.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) - 1) ≤ 16 * (Complex.abs z)⁻¹

State before:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ Complex.abs ((A.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) - 1) ≤ 16 * (Complex.abs z)⁻¹
Tactic:
rw [(by norm_num : (16 : ℝ) = 4 * 4), mul_assoc]
State after:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ Complex.abs ((A.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) - 1) ≤ 4 * (4 * (Complex.abs z)⁻¹)

State before:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ Complex.abs ((A.prod fun x => term (fl (f d) ∞ c) d x z⁻¹) - 1) ≤ 4 * (4 * (Complex.abs z)⁻¹)
Tactic:
refine dist_prod_one_le_abs_sum ?_ (by linarith)
State after:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ (A.sum fun n => Complex.abs (term (fl (f d) ∞ c) d n z⁻¹ - 1)) ≤ 4 * (Complex.abs z)⁻¹

State before:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ (A.sum fun n => Complex.abs (term (fl (f d) ∞ c) d n z⁻¹ - 1)) ≤ 4 * (Complex.abs z)⁻¹
Tactic:
refine le_trans (Finset.sum_le_sum fun n _ ↦ term_approx d (by linarith) cz n) ?_
State after:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ (A.sum fun i => 2 * (1 / 2) ^ i * (Complex.abs z)⁻¹) ≤ 4 * (Complex.abs z)⁻¹

State before:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ (A.sum fun i => 2 * (1 / 2) ^ i * (Complex.abs z)⁻¹) ≤ 4 * (Complex.abs z)⁻¹
Tactic:
simp only [mul_comm _ _⁻¹, ← mul_assoc, ← Finset.mul_sum]
State after:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ ((Complex.abs z)⁻¹ * 2 * A.sum fun i => (1 / 2) ^ i) ≤ (Complex.abs z)⁻¹ * 4

State before:
case intro
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ ((Complex.abs z)⁻¹ * 2 * A.sum fun i => (1 / 2) ^ i) ≤ (Complex.abs z)⁻¹ * 4
Tactic:
calc (abs z)⁻¹ * 2 * A.sum (fun n ↦ (1/2:ℝ)^n)
  _ ≤ (abs z)⁻¹ * 2 * (1 - 1 / 2)⁻¹ := by gcongr; apply partial_geometric_bound; repeat norm_num
  _ = (abs z)⁻¹ * 4 := by ring
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
⊢ (Complex.abs z)⁻¹ ≤ 1 / 8
Tactic:
rw [one_div]
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
⊢ (Complex.abs z)⁻¹ ≤ 8⁻¹

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
⊢ (Complex.abs z)⁻¹ ≤ 8⁻¹
Tactic:
apply inv_le_inv_of_le
State after:
case ha
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
⊢ 0 < 8

case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
⊢ 8 ≤ Complex.abs z

State before:
case ha
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
⊢ 0 < 8

case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
⊢ 8 ≤ Complex.abs z
Tactic:
norm_num
State after:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
⊢ 8 ≤ Complex.abs z

State before:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
⊢ 8 ≤ Complex.abs z
Tactic:
exact le_trans (by norm_num) (le_trans c16.le cz)
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
⊢ 8 ≤ 16
Tactic:
norm_num
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ 16 = 4 * 4
Tactic:
norm_num
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ 4 * (Complex.abs z)⁻¹ ≤ 1 / 2
Tactic:
linarith
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
n : ℕ
x✝ : n ∈ A
⊢ 16 < Complex.abs c
Tactic:
linarith
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ ((Complex.abs z)⁻¹ * 2 * A.sum fun n => (1 / 2) ^ n) ≤ (Complex.abs z)⁻¹ * 2 * (1 - 1 / 2)⁻¹
Tactic:
gcongr
State after:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ (A.sum fun n => (1 / 2) ^ n) ≤ (1 - 1 / 2)⁻¹

State before:
case h
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ (A.sum fun n => (1 / 2) ^ n) ≤ (1 - 1 / 2)⁻¹
Tactic:
apply partial_geometric_bound
State after:
case h.a0
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ 0 ≤ 1 / 2

case h.a1
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ 1 / 2 < 1

State before:
case h.a0
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ 0 ≤ 1 / 2

case h.a1
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ 1 / 2 < 1
Tactic:
repeat norm_num
State after:
no goals

State before:
case h.a1
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ 1 / 2 < 1
Tactic:
norm_num
State after:
no goals

State before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c z : ℂ
c16 : 16 < Complex.abs c
cz : Complex.abs c ≤ Complex.abs z
s : Super (f d) d ∞ := superF d
i8 : (Complex.abs z)⁻¹ ≤ 1 / 8
p : ℂ
A : Finset ℕ
⊢ (Complex.abs z)⁻¹ * 2 * (1 - 1 / 2)⁻¹ = (Complex.abs z)⁻¹ * 4
Tactic:
ring
State after:
no goals