internlm/Lean-Github huggingface dataset:
Theorem: not_multibrot_of_two_lt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
c2 : Complex.abs c ≤ 2
s : ℝ
h : 2 < s
hs : Complex.abs ((f' d c)^[n] c) = s
s1 : 1 ≤ s
s1' : 1 ≤ s - 1
s0 : 0 ≤ s
b : ∀ (k : ℕ), s * (s - 1) ^ k ≤ Complex.abs ((f' d c)^[k + n] c)
⊢ 0 < s
Tactic:
linarith
Proof state after:
no goals
Theorem: multibrot_eq_le_two
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ multibrot d = ⋂ n, (fun c => (f' d c)^[n] c) ⁻¹' closedBall 0 2
Tactic:
apply Set.ext
Proof state after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ (x : ℂ), x ∈ multibrot d ↔ x ∈ ⋂ n, (fun c => (f' d c)^[n] c) ⁻¹' closedBall 0 2
Theorem: multibrot_eq_le_two
Proof state before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ (x : ℂ), x ∈ multibrot d ↔ x ∈ ⋂ n, (fun c => (f' d c)^[n] c) ⁻¹' closedBall 0 2
Tactic:
intro c
Proof state after:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ c ∈ multibrot d ↔ c ∈ ⋂ n, (fun c => (f' d c)^[n] c) ⁻¹' closedBall 0 2
Theorem: multibrot_eq_le_two
Proof state before:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ c ∈ multibrot d ↔ c ∈ ⋂ n, (fun c => (f' d c)^[n] c) ⁻¹' closedBall 0 2
Tactic:
simp only [mem_iInter, mem_preimage, mem_closedBall, Complex.dist_eq, sub_zero]
Proof state after:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ c ∈ multibrot d ↔ ∀ (i : ℕ), Complex.abs ((f' d c)^[i] c) ≤ 2
Theorem: multibrot_eq_le_two
Proof state before:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ c ∈ multibrot d ↔ ∀ (i : ℕ), Complex.abs ((f' d c)^[i] c) ≤ 2
Tactic:
constructor
Proof state after:
case h.mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ c ∈ multibrot d → ∀ (i : ℕ), Complex.abs ((f' d c)^[i] c) ≤ 2

case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ (∀ (i : ℕ), Complex.abs ((f' d c)^[i] c) ≤ 2) → c ∈ multibrot d
Theorem: multibrot_eq_le_two
Proof state before:
case h.mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ c ∈ multibrot d → ∀ (i : ℕ), Complex.abs ((f' d c)^[i] c) ≤ 2
Tactic:
intro m n
Proof state after:
case h.mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
m : c ∈ multibrot d
n : ℕ
⊢ Complex.abs ((f' d c)^[n] c) ≤ 2
Theorem: multibrot_eq_le_two
Proof state before:
case h.mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
m : c ∈ multibrot d
n : ℕ
⊢ Complex.abs ((f' d c)^[n] c) ≤ 2
Tactic:
contrapose m
Proof state after:
case h.mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
m : ¬Complex.abs ((f' d c)^[n] c) ≤ 2
⊢ c ∉ multibrot d
Theorem: multibrot_eq_le_two
Proof state before:
case h.mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
m : ¬Complex.abs ((f' d c)^[n] c) ≤ 2
⊢ c ∉ multibrot d
Tactic:
simp only [not_le] at m
Proof state after:
case h.mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
m : 2 < Complex.abs ((f' d c)^[n] c)
⊢ c ∉ multibrot d
Theorem: multibrot_eq_le_two
Proof state before:
case h.mp
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
n : ℕ
m : 2 < Complex.abs ((f' d c)^[n] c)
⊢ c ∉ multibrot d
Tactic:
exact not_multibrot_of_two_lt m
Proof state after:
no goals
Theorem: multibrot_eq_le_two
Proof state before:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
⊢ (∀ (i : ℕ), Complex.abs ((f' d c)^[i] c) ≤ 2) → c ∈ multibrot d
Tactic:
intro h
Proof state after:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
h : ∀ (i : ℕ), Complex.abs ((f' d c)^[i] c) ≤ 2
⊢ c ∈ multibrot d
Theorem: multibrot_eq_le_two
Proof state before:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
h : ∀ (i : ℕ), Complex.abs ((f' d c)^[i] c) ≤ 2
⊢ c ∈ multibrot d
Tactic:
contrapose h
Proof state after:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
h : c ∉ multibrot d
⊢ ¬∀ (i : ℕ), Complex.abs ((f' d c)^[i] c) ≤ 2
Theorem: multibrot_eq_le_two
Proof state before:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
h : c ∉ multibrot d
⊢ ¬∀ (i : ℕ), Complex.abs ((f' d c)^[i] c) ≤ 2
Tactic:
simp only [multibrot_coe, tendsto_atInf_iff_norm_tendsto_atTop, Complex.norm_eq_abs,
  not_not, not_forall, not_le, Filter.tendsto_atTop, not_exists] at h ⊢
Proof state after:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
h : ∀ (x : ℝ), ∀ᶠ (a : ℕ) in atTop, x ≤ Complex.abs ((f' d c)^[a] c)
⊢ ∃ x, 2 < Complex.abs ((f' d c)^[x] c)
Theorem: multibrot_eq_le_two
Proof state before:
case h.mpr
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
h : ∀ (x : ℝ), ∀ᶠ (a : ℕ) in atTop, x ≤ Complex.abs ((f' d c)^[a] c)
⊢ ∃ x, 2 < Complex.abs ((f' d c)^[x] c)
Tactic:
rcases(h 3).exists with ⟨n, h⟩
Proof state after:
case h.mpr.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
h✝ : ∀ (x : ℝ), ∀ᶠ (a : ℕ) in atTop, x ≤ Complex.abs ((f' d c)^[a] c)
n : ℕ
h : 3 ≤ Complex.abs ((f' d c)^[n] c)
⊢ ∃ x, 2 < Complex.abs ((f' d c)^[x] c)
Theorem: multibrot_eq_le_two
Proof state before:
case h.mpr.intro
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
h✝ : ∀ (x : ℝ), ∀ᶠ (a : ℕ) in atTop, x ≤ Complex.abs ((f' d c)^[a] c)
n : ℕ
h : 3 ≤ Complex.abs ((f' d c)^[n] c)
⊢ ∃ x, 2 < Complex.abs ((f' d c)^[x] c)
Tactic:
use n
Proof state after:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
h✝ : ∀ (x : ℝ), ∀ᶠ (a : ℕ) in atTop, x ≤ Complex.abs ((f' d c)^[a] c)
n : ℕ
h : 3 ≤ Complex.abs ((f' d c)^[n] c)
⊢ 2 < Complex.abs ((f' d c)^[n] c)
Theorem: multibrot_eq_le_two
Proof state before:
case h
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
h✝ : ∀ (x : ℝ), ∀ᶠ (a : ℕ) in atTop, x ≤ Complex.abs ((f' d c)^[a] c)
n : ℕ
h : 3 ≤ Complex.abs ((f' d c)^[n] c)
⊢ 2 < Complex.abs ((f' d c)^[n] c)
Tactic:
linarith
Proof state after:
no goals
Theorem: isCompact_multibrot
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsCompact (multibrot d)
Tactic:
refine IsCompact.of_isClosed_subset (isCompact_closedBall _ _) ?_ multibrot_subset_closedBall
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsClosed (multibrot d)
Theorem: isCompact_multibrot
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsClosed (multibrot d)
Tactic:
rw [multibrot_eq_le_two]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsClosed (⋂ n, (fun c => (f' d c)^[n] c) ⁻¹' closedBall 0 2)
Theorem: isCompact_multibrot
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsClosed (⋂ n, (fun c => (f' d c)^[n] c) ⁻¹' closedBall 0 2)
Tactic:
apply isClosed_iInter
Proof state after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ (i : ℕ), IsClosed ((fun c => (f' d c)^[i] c) ⁻¹' closedBall 0 2)
Theorem: isCompact_multibrot
Proof state before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ (i : ℕ), IsClosed ((fun c => (f' d c)^[i] c) ⁻¹' closedBall 0 2)
Tactic:
intro n
Proof state after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
⊢ IsClosed ((fun c => (f' d c)^[n] c) ⁻¹' closedBall 0 2)
Theorem: isCompact_multibrot
Proof state before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
⊢ IsClosed ((fun c => (f' d c)^[n] c) ⁻¹' closedBall 0 2)
Tactic:
refine IsClosed.preimage ?_ Metric.isClosed_ball
Proof state after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
⊢ Continuous fun c => (f' d c)^[n] c
Theorem: isCompact_multibrot
Proof state before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
⊢ Continuous fun c => (f' d c)^[n] c
Tactic:
induction' n with n h
Proof state after:
case h.zero
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ Continuous fun c => (f' d c)^[0] c

case h.succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : Continuous fun c => (f' d c)^[n] c
⊢ Continuous fun c => (f' d c)^[n + 1] c
Theorem: isCompact_multibrot
Proof state before:
case h.zero
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ Continuous fun c => (f' d c)^[0] c

case h.succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : Continuous fun c => (f' d c)^[n] c
⊢ Continuous fun c => (f' d c)^[n + 1] c
Tactic:
simp only [Function.iterate_zero_apply]
Proof state after:
case h.zero
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ Continuous fun c => c

case h.succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : Continuous fun c => (f' d c)^[n] c
⊢ Continuous fun c => (f' d c)^[n + 1] c
Theorem: isCompact_multibrot
Proof state before:
case h.zero
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ Continuous fun c => c

case h.succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : Continuous fun c => (f' d c)^[n] c
⊢ Continuous fun c => (f' d c)^[n + 1] c
Tactic:
exact continuous_id
Proof state after:
case h.succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : Continuous fun c => (f' d c)^[n] c
⊢ Continuous fun c => (f' d c)^[n + 1] c
Theorem: isCompact_multibrot
Proof state before:
case h.succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : Continuous fun c => (f' d c)^[n] c
⊢ Continuous fun c => (f' d c)^[n + 1] c
Tactic:
simp only [Function.iterate_succ_apply']
Proof state after:
case h.succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : Continuous fun c => (f' d c)^[n] c
⊢ Continuous fun c => f' d c ((f' d c)^[n] c)
Theorem: isCompact_multibrot
Proof state before:
case h.succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : Continuous fun c => (f' d c)^[n] c
⊢ Continuous fun c => f' d c ((f' d c)^[n] c)
Tactic:
rw [continuous_iff_continuousAt]
Proof state after:
case h.succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : Continuous fun c => (f' d c)^[n] c
⊢ ∀ (x : ℂ), ContinuousAt (fun c => f' d c ((f' d c)^[n] c)) x
Theorem: isCompact_multibrot
Proof state before:
case h.succ
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : Continuous fun c => (f' d c)^[n] c
⊢ ∀ (x : ℂ), ContinuousAt (fun c => f' d c ((f' d c)^[n] c)) x
Tactic:
intro c
Proof state after:
case h.succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : Continuous fun c => (f' d c)^[n] c
c : ℂ
⊢ ContinuousAt (fun c => f' d c ((f' d c)^[n] c)) c
Theorem: isCompact_multibrot
Proof state before:
case h.succ
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
n : ℕ
h : Continuous fun c => (f' d c)^[n] c
c : ℂ
⊢ ContinuousAt (fun c => f' d c ((f' d c)^[n] c)) c
Tactic:
exact (analytic_f' _ (mem_univ _)).continuousAt.comp₂ continuousAt_id h.continuousAt
Proof state after:
no goals
Theorem: isOpen_multibrotExt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsOpen (multibrotExt d)
Tactic:
rw [OnePoint.isOpen_iff_of_mem']
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsCompact (OnePoint.some ⁻¹' multibrotExt d)ᶜ ∧ IsOpen (OnePoint.some ⁻¹' multibrotExt d)

c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∞ ∈ multibrotExt d
Theorem: isOpen_multibrotExt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsCompact (OnePoint.some ⁻¹' multibrotExt d)ᶜ ∧ IsOpen (OnePoint.some ⁻¹' multibrotExt d)

c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∞ ∈ multibrotExt d
Tactic:
simp only [coe_preimage_multibrotExt, compl_compl]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsCompact (multibrot d) ∧ IsOpen (multibrot d)ᶜ

c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∞ ∈ multibrotExt d
Theorem: isOpen_multibrotExt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ IsCompact (multibrot d) ∧ IsOpen (multibrot d)ᶜ

c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∞ ∈ multibrotExt d
Tactic:
use isCompact_multibrot, isCompact_multibrot.isClosed.isOpen_compl
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∞ ∈ multibrotExt d
Theorem: isOpen_multibrotExt
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∞ ∈ multibrotExt d
Tactic:
exact multibrotExt_inf
Proof state after:
no goals
Theorem: bottcher_bound
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
set s := superF d
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : ℂ
lo : 16 < Complex.abs c
s : Super (f d) d ∞ := superF d
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs 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
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
generalize hg : fl (f d) ∞ c = g
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 (bottcher' d c) ≤ 3 * Complex.abs 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
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
have ct : c⁻¹ ∈ {z : ℂ | abs z < (max 16 (abs c / 2))⁻¹} := by
  simp only [mem_setOf, map_inv₀]
  apply inv_lt_inv_of_lt; bound; refine max_lt lo (half_lt_self (lt_trans (by norm_num) lo))
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))⁻¹}
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs 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))⁻¹}
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
have mem : c ∉ multibrot d := multibrot_two_lt (lt_trans (by norm_num) lo)
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
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs 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
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
have nz : ∀ n, (f d c)^[n] c ≠ 0 := by
  intro n; contrapose mem; simp only [not_not] at mem ⊢; exact multibrot_of_zero 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))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs 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
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
have iter : ∀ n, ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹) := by
  intro n; induction' n with n h
  have cp : c ≠ 0 := Complex.abs.ne_zero_iff.mp (lt_trans (by norm_num) lo).ne'
  simp only [Function.iterate_zero_apply, inv_coe cp, toComplex_coe]
  have e : (f d c)^[n] ↑c = ((g^[n] c⁻¹ : ℂ) : 𝕊)⁻¹ := by rw [← h, inv_inv]
  simp only [Function.iterate_succ_apply', e]
  generalize hz : g^[n] c⁻¹ = z
  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]
  rw [coe_toComplex]
  simp only [Ne, inv_eq_inf, ← hz, ← h, inv_inv, ← Function.iterate_succ_apply' (f d c)]
  apply nz
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⁻¹)
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs 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
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
have b := 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))⁻¹}
mem : c ∉ multibrot d
nz : ∀ (n : ℕ), (f d c)^[n] ↑c ≠ 0
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
b : c ∉ multibrot d
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs 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
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
b : c ∉ multibrot d
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
simp only [multibrot_basin', not_not] at b
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⁻¹)
b : (c, ↑c) ∈ ⋯.basin
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs 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
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
b : (c, ↑c) ∈ ⋯.basin
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
have attracts := (s.basin_attracts b).eventually (s.bottcher_eq_bottcherNear c)
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⁻¹)
b : (c, ↑c) ∈ ⋯.basin
attracts : ∀ᶠ (x : ℕ) in atTop, s.bottcher c ((f d c)^[x] ↑c) = s.bottcherNear c ((f d c)^[x] ↑c)
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs 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
iter : ∀ (n : ℕ), ((f d c)^[n] ↑c)⁻¹ = ↑(g^[n] c⁻¹)
b : (c, ↑c) ∈ ⋯.basin
attracts : ∀ᶠ (x : ℕ) in atTop, s.bottcher c ((f d c)^[x] ↑c) = s.bottcherNear c ((f d c)^[x] ↑c)
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
rcases (attracts.and (s.basin_stays b)).exists with ⟨n, 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⁻¹)
b : (c, ↑c) ∈ ⋯.basin
attracts : ∀ᶠ (x : ℕ) in atTop, s.bottcher c ((f d c)^[x] ↑c) = s.bottcherNear c ((f d c)^[x] ↑c)
n : ℕ
eq : s.bottcher c ((f d c)^[n] ↑c) = s.bottcherNear c ((f d c)^[n] ↑c)
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
⊢ 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⁻¹)
b : (c, ↑c) ∈ ⋯.basin
attracts : ∀ᶠ (x : ℕ) in atTop, s.bottcher c ((f d c)^[x] ↑c) = s.bottcherNear c ((f d c)^[x] ↑c)
n : ℕ
eq : s.bottcher c ((f d c)^[n] ↑c) = s.bottcherNear c ((f d c)^[n] ↑c)
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
clear attracts b
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 : ℕ
eq : s.bottcher c ((f d c)^[n] ↑c) = s.bottcherNear c ((f d c)^[n] ↑c)
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
⊢ 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 : ℕ
eq : s.bottcher c ((f d c)^[n] ↑c) = s.bottcherNear c ((f d c)^[n] ↑c)
right✝ : (c, (f d c)^[n] ↑c) ∈ s.near
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
simp only [Super.bottcherNear, extChartAt_inf, PartialEquiv.trans_apply,
  coePartialEquiv_symm_apply, Equiv.toPartialEquiv_apply, invEquiv_apply, RiemannSphere.inv_inf,
  toComplex_zero, sub_zero, Super.fl, hg, iter, toComplex_coe] 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 : s.bottcher c ((f d c)^[n] ↑c) = bottcherNear g d (g^[n] 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
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⁻¹)
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
have e0 : s.bottcher c ((f d c)^[n] ↑c) = bottcher' d c ^ d ^ n := s.bottcher_eqn_iter n
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 : 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
⊢ 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 : 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
⊢ Complex.abs (bottcher' d c) ≤ 3 * Complex.abs c⁻¹
Tactic:
have e1 : bottcherNear g d (g^[n] c⁻¹) = bottcherNear g d c⁻¹ ^ d ^ n := by
  rw [← hg]; exact bottcherNear_eqn_iter (superNearF d c) ct n
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 : 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⁻¹