internlm/Lean-Github huggingface dataset:
Theorem: bottcher_bound
Proof state before:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : s.bottcher c ((f d c)^[n] ↑c) = bottcherNear g d (g^[n] c⁻¹)
e0 : s.bottcher c ((f d c)^[n] ↑c) = bottcher' d c ^ d ^ n
e1 : bottcherNear g d (g^[n] c⁻¹) = bottcherNear g d c⁻¹ ^ d ^ n
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
rw [e0, e1] at eq
Proof state after:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : bottcher' d c ^ d ^ n = bottcherNear g d c⁻¹ ^ d ^ n
e0 : s.bottcher c ((f d c)^[n] ↑c) = bottcher' d c ^ d ^ n
e1 : bottcherNear g d (g^[n] c⁻¹) = bottcherNear g d c⁻¹ ^ d ^ n
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Theorem: bottcher_bound
Proof state before:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : bottcher' d c ^ d ^ n = bottcherNear g d c⁻¹ ^ d ^ n
e0 : s.bottcher c ((f d c)^[n] ↑c) = bottcher' d c ^ d ^ n
e1 : bottcherNear g d (g^[n] c⁻¹) = bottcherNear g d c⁻¹ ^ d ^ n
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
clear e0 e1 iter
Proof state after:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : bottcher' d c ^ d ^ n = bottcherNear g d c⁻¹ ^ d ^ n
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Theorem: bottcher_bound
Proof state before:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : bottcher' d c ^ d ^ n = bottcherNear g d c⁻¹ ^ d ^ n
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
have ae : abs (bottcher' d c) = abs (bottcherNear g d c⁻¹) := by
  apply (pow_left_inj (Complex.abs.nonneg _) (Complex.abs.nonneg _)
    (pow_ne_zero n (d_ne_zero d))).mp
  simp only [← Complex.abs.map_pow, eq]
Proof state after:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : bottcher' d c ^ d ^ n = bottcherNear g d c⁻¹ ^ d ^ n
ae : Complex.abs (bottcher' d c) = Complex.abs (bottcherNear g d c⁻¹)
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Theorem: bottcher_bound
Proof state before:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : bottcher' d c ^ d ^ n = bottcherNear g d c⁻¹ ^ d ^ n
ae : Complex.abs (bottcher' d c) = Complex.abs (bottcherNear g d c⁻¹)
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
rw [ae, ← hg]
Proof state after:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : bottcher' d c ^ d ^ n = bottcherNear g d c⁻¹ ^ d ^ n
ae : Complex.abs (bottcher' d c) = Complex.abs (bottcherNear g d c⁻¹)
⊢ Complex.abs (bottcherNear (fl (f d) ∞ c) d c⁻¹) ≤ 3 * Complex.abs c⁻¹
Theorem: bottcher_bound
Proof state before:
case intro.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : bottcher' d c ^ d ^ n = bottcherNear g d c⁻¹ ^ d ^ n
ae : Complex.abs (bottcher' d c) = Complex.abs (bottcherNear g d c⁻¹)
⊢ Complex.abs (bottcherNear (fl (f d) ∞ c) d c⁻¹) ≤ 3 * Complex.abs c⁻¹
Tactic:
exact bottcherNear_le (superNearF d c) ct
Proof state after:
no goals
Theorem: bottcher_bound
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
⊢ c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
Tactic:
simp only [mem_setOf, map_inv₀]
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
⊢ (Complex.abs c)⁻¹ < (max 16 (Complex.abs c / 2))⁻¹
Theorem: bottcher_bound
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
⊢ (Complex.abs c)⁻¹ < (max 16 (Complex.abs c / 2))⁻¹
Tactic:
apply inv_lt_inv_of_lt
Proof state after:
case hb
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
⊢ 0 < max 16 (Complex.abs c / 2)

case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
⊢ max 16 (Complex.abs c / 2) < Complex.abs c
Theorem: bottcher_bound
Proof state before:
case hb
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
⊢ 0 < max 16 (Complex.abs c / 2)

case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
⊢ max 16 (Complex.abs c / 2) < Complex.abs c
Tactic:
bound
Proof state after:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
⊢ max 16 (Complex.abs c / 2) < Complex.abs c
Theorem: bottcher_bound
Proof state before:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
⊢ max 16 (Complex.abs c / 2) < Complex.abs c
Tactic:
refine max_lt lo (half_lt_self (lt_trans (by norm_num) lo))
Proof state after:
no goals
Theorem: bottcher_bound
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
⊢ 0 < 16
Tactic:
norm_num
Proof state after:
no goals
Theorem: bottcher_bound
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
⊢ 2 < 16
Tactic:
norm_num
Proof state after:
no goals
Theorem: bottcher_bound
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
⊢ ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
Tactic:
intro n
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
n : ℕ
⊢ (f d c)^[n] ↑c ≠ 0
Theorem: bottcher_bound
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
n : ℕ
⊢ (f d c)^[n] ↑c ≠ 0
Tactic:
contrapose mem
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
n : ℕ
mem : ¬(f d c)^[n] ↑c ≠ 0
⊢ ¬c ∉ multibrot d
Theorem: bottcher_bound
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
n : ℕ
mem : ¬(f d c)^[n] ↑c ≠ 0
⊢ ¬c ∉ multibrot d
Tactic:
simp only [not_not] at mem ⊢
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
n : ℕ
mem : (f d c)^[n] ↑c = 0
⊢ c ∈ multibrot d
Theorem: bottcher_bound
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
n : ℕ
mem : (f d c)^[n] ↑c = 0
⊢ c ∈ multibrot d
Tactic:
exact multibrot_of_zero mem
Proof state after:
no goals
Theorem: bottcher_bound
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
⊢ ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
Tactic:
intro n
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
⊢ ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
Theorem: bottcher_bound
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
⊢ ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
Tactic:
induction' n with n h
Proof state after:
case zero
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
⊢ ((f d c)^[0] ↑c)⁻¹ = ↑(g^[0] c⁻¹)

case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
⊢ ((f d c)^[n + 1] ↑c)⁻¹ = ↑(g^[n + 1] c⁻¹)
Theorem: bottcher_bound
Proof state before:
case zero
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
⊢ ((f d c)^[0] ↑c)⁻¹ = ↑(g^[0] c⁻¹)

case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
⊢ ((f d c)^[n + 1] ↑c)⁻¹ = ↑(g^[n + 1] c⁻¹)
Tactic:
have cp : c ≠ 0 := Complex.abs.ne_zero_iff.mp (lt_trans (by norm_num) lo).ne'
Proof state after:
case zero
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
cp : c ≠ 0
⊢ ((f d c)^[0] ↑c)⁻¹ = ↑(g^[0] c⁻¹)

case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
⊢ ((f d c)^[n + 1] ↑c)⁻¹ = ↑(g^[n + 1] c⁻¹)
Theorem: bottcher_bound
Proof state before:
case zero
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
cp : c ≠ 0
⊢ ((f d c)^[0] ↑c)⁻¹ = ↑(g^[0] c⁻¹)

case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
⊢ ((f d c)^[n + 1] ↑c)⁻¹ = ↑(g^[n + 1] c⁻¹)
Tactic:
simp only [Function.iterate_zero_apply, inv_coe cp, toComplex_coe]
Proof state after:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
⊢ ((f d c)^[n + 1] ↑c)⁻¹ = ↑(g^[n + 1] c⁻¹)
Theorem: bottcher_bound
Proof state before:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
⊢ ((f d c)^[n + 1] ↑c)⁻¹ = ↑(g^[n + 1] c⁻¹)
Tactic:
have e : (f d c)^[n] ↑c = ((g^[n] c⁻¹ : ℂ) : 𝕊)⁻¹ := by rw [← h, inv_inv]
Proof state after:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
e : (f d c)^[n] ↑c = (↑(g^[n] c⁻¹))⁻¹
⊢ ((f d c)^[n + 1] ↑c)⁻¹ = ↑(g^[n + 1] c⁻¹)
Theorem: bottcher_bound
Proof state before:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
e : (f d c)^[n] ↑c = (↑(g^[n] c⁻¹))⁻¹
⊢ ((f d c)^[n + 1] ↑c)⁻¹ = ↑(g^[n + 1] c⁻¹)
Tactic:
simp only [Function.iterate_succ_apply', e]
Proof state after:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
e : (f d c)^[n] ↑c = (↑(g^[n] c⁻¹))⁻¹
⊢ (f d c (↑(g^[n] c⁻¹))⁻¹)⁻¹ = ↑(g (g^[n] c⁻¹))
Theorem: bottcher_bound
Proof state before:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
e : (f d c)^[n] ↑c = (↑(g^[n] c⁻¹))⁻¹
⊢ (f d c (↑(g^[n] c⁻¹))⁻¹)⁻¹ = ↑(g (g^[n] c⁻¹))
Tactic:
generalize hz : g^[n] c⁻¹ = z
Proof state after:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
e : (f d c)^[n] ↑c = (↑(g^[n] c⁻¹))⁻¹
z : ℂ
hz : g^[n] c⁻¹ = z
⊢ (f d c (↑z)⁻¹)⁻¹ = ↑(g z)
Theorem: bottcher_bound
Proof state before:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
e : (f d c)^[n] ↑c = (↑(g^[n] c⁻¹))⁻¹
z : ℂ
hz : g^[n] c⁻¹ = z
⊢ (f d c (↑z)⁻¹)⁻¹ = ↑(g z)
Tactic:
simp only [← hg, fl, extChartAt_inf, PartialEquiv.trans_apply, Equiv.toPartialEquiv_apply,
  invEquiv_apply, RiemannSphere.inv_inf, coePartialEquiv_symm_apply, toComplex_zero, sub_zero,
  Function.comp, add_zero, PartialEquiv.coe_trans_symm, PartialEquiv.symm_symm,
  coePartialEquiv_apply, Equiv.toPartialEquiv_symm_apply, invEquiv_symm]
Proof state after:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
e : (f d c)^[n] ↑c = (↑(g^[n] c⁻¹))⁻¹
z : ℂ
hz : g^[n] c⁻¹ = z
⊢ (f d c (↑z)⁻¹)⁻¹ = ↑(f d c (↑z)⁻¹)⁻¹.toComplex
Theorem: bottcher_bound
Proof state before:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
e : (f d c)^[n] ↑c = (↑(g^[n] c⁻¹))⁻¹
z : ℂ
hz : g^[n] c⁻¹ = z
⊢ (f d c (↑z)⁻¹)⁻¹ = ↑(f d c (↑z)⁻¹)⁻¹.toComplex
Tactic:
rw [coe_toComplex]
Proof state after:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
e : (f d c)^[n] ↑c = (↑(g^[n] c⁻¹))⁻¹
z : ℂ
hz : g^[n] c⁻¹ = z
⊢ (f d c (↑z)⁻¹)⁻¹ ≠ ∞
Theorem: bottcher_bound
Proof state before:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
e : (f d c)^[n] ↑c = (↑(g^[n] c⁻¹))⁻¹
z : ℂ
hz : g^[n] c⁻¹ = z
⊢ (f d c (↑z)⁻¹)⁻¹ ≠ ∞
Tactic:
simp only [Ne, inv_eq_inf, ← hz, ← h, inv_inv, ← Function.iterate_succ_apply' (f d c)]
Proof state after:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
e : (f d c)^[n] ↑c = (↑(g^[n] c⁻¹))⁻¹
z : ℂ
hz : g^[n] c⁻¹ = z
⊢ ¬(f d c)^[n.succ] ↑c = 0
Theorem: bottcher_bound
Proof state before:
case succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
e : (f d c)^[n] ↑c = (↑(g^[n] c⁻¹))⁻¹
z : ℂ
hz : g^[n] c⁻¹ = z
⊢ ¬(f d c)^[n.succ] ↑c = 0
Tactic:
apply nz
Proof state after:
no goals
Theorem: bottcher_bound
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
⊢ 0 < 16
Tactic:
norm_num
Proof state after:
no goals
Theorem: bottcher_bound
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
h : ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
⊢ (f d c)^[n] ↑c = (↑(g^[n] c⁻¹))⁻¹
Tactic:
rw [← h, inv_inv]
Proof state after:
no goals
Theorem: bottcher_bound
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : s.bottcher c ((f d c)^[n] ↑c) = bottcherNear g d (g^[n] c⁻¹)
e0 : s.bottcher c ((f d c)^[n] ↑c) = bottcher' d c ^ d ^ n
⊢ bottcherNear g d (g^[n] c⁻¹) = bottcherNear g d c⁻¹ ^ d ^ n
Tactic:
rw [← hg]
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : s.bottcher c ((f d c)^[n] ↑c) = bottcherNear g d (g^[n] c⁻¹)
e0 : s.bottcher c ((f d c)^[n] ↑c) = bottcher' d c ^ d ^ n
⊢ bottcherNear (fl (f d) ∞ c) d ((fl (f d) ∞ c)^[n] c⁻¹) = bottcherNear (fl (f d) ∞ c) d c⁻¹ ^ d ^ n
Theorem: bottcher_bound
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : s.bottcher c ((f d c)^[n] ↑c) = bottcherNear g d (g^[n] c⁻¹)
e0 : s.bottcher c ((f d c)^[n] ↑c) = bottcher' d c ^ d ^ n
⊢ bottcherNear (fl (f d) ∞ c) d ((fl (f d) ∞ c)^[n] c⁻¹) = bottcherNear (fl (f d) ∞ c) d c⁻¹ ^ d ^ n
Tactic:
exact bottcherNear_eqn_iter (superNearF d c) ct n
Proof state after:
no goals
Theorem: bottcher_bound
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : bottcher' d c ^ d ^ n = bottcherNear g d c⁻¹ ^ d ^ n
⊢ Complex.abs (bottcher' d c) = Complex.abs (bottcherNear g d c⁻¹)
Tactic:
apply (pow_left_inj (Complex.abs.nonneg _) (Complex.abs.nonneg _)
  (pow_ne_zero n (d_ne_zero d))).mp
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
g : ℂ → ℂ
hg : fl (f d) ∞ c = g
ct : c⁻¹ ∈ {z | Complex.abs z < (max 16 (Complex.abs c / 2))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
n : ℕ
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
eq : bottcher' d c ^ d ^ n = bottcherNear g d c⁻¹ ^ d ^ n
⊢ Complex.abs (bottcher' d c) ^ d ^ n = Complex.abs (bottcherNear g d c⁻¹) ^ d ^ n