internlm/Lean-Github huggingface dataset:
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) ^ d ^ n = Complex.abs (bottcherNear g d c⁻¹) ^ d ^ n
Tactic:
simp only [← Complex.abs.map_pow, eq]
Proof state after:
no goals
Theorem: bottcher_tendsto_zero
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ Tendsto (bottcher' d) atInf (𝓝 0)
Tactic:
rw [Metric.tendsto_nhds]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ ε > 0, ∀ᶠ (x : ℂ) in atInf, dist (bottcher' d x) 0 < ε
Theorem: bottcher_tendsto_zero
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ ∀ ε > 0, ∀ᶠ (x : ℂ) in atInf, dist (bottcher' d x) 0 < ε
Tactic:
intro r rp
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
⊢ ∀ᶠ (x : ℂ) in atInf, dist (bottcher' d x) 0 < r
Theorem: bottcher_tendsto_zero
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
⊢ ∀ᶠ (x : ℂ) in atInf, dist (bottcher' d x) 0 < r
Tactic:
rw [atInf_basis.eventually_iff]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
⊢ ∃ i, True ∧ ∀ ⦃x : ℂ⦄, x ∈ {x | i < ‖x‖} → dist (bottcher' d x) 0 < r
Theorem: bottcher_tendsto_zero
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
⊢ ∃ i, True ∧ ∀ ⦃x : ℂ⦄, x ∈ {x | i < ‖x‖} → dist (bottcher' d x) 0 < r
Tactic:
use max 16 (3 / r)
Proof state after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
⊢ True ∧ ∀ ⦃x : ℂ⦄, x ∈ {x | max 16 (3 / r) < ‖x‖} → dist (bottcher' d x) 0 < r
Theorem: bottcher_tendsto_zero
Proof state before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
⊢ True ∧ ∀ ⦃x : ℂ⦄, x ∈ {x | max 16 (3 / r) < ‖x‖} → dist (bottcher' d x) 0 < r
Tactic:
simp only [true_and_iff, mem_setOf, Complex.dist_eq, sub_zero, Complex.norm_eq_abs, max_lt_iff]
Proof state after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
⊢ ∀ ⦃x : ℂ⦄, 16 < Complex.abs x ∧ 3 / r < Complex.abs x → Complex.abs (bottcher' d x) < r
Theorem: bottcher_tendsto_zero
Proof state before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
⊢ ∀ ⦃x : ℂ⦄, 16 < Complex.abs x ∧ 3 / r < Complex.abs x → Complex.abs (bottcher' d x) < r
Tactic:
intro z ⟨lo, rz⟩
Proof state after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
z : ℂ
lo : 16 < Complex.abs z
rz : 3 / r < Complex.abs z
⊢ Complex.abs (bottcher' d z) < r
Theorem: bottcher_tendsto_zero
Proof state before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
z : ℂ
lo : 16 < Complex.abs z
rz : 3 / r < Complex.abs z
⊢ Complex.abs (bottcher' d z) < r
Tactic:
apply lt_of_le_of_lt (bottcher_bound lo)
Proof state after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
z : ℂ
lo : 16 < Complex.abs z
rz : 3 / r < Complex.abs z
⊢ 3 * Complex.abs z⁻¹ < r
Theorem: bottcher_tendsto_zero
Proof state before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
z : ℂ
lo : 16 < Complex.abs z
rz : 3 / r < Complex.abs z
⊢ 3 * Complex.abs z⁻¹ < r
Tactic:
rw [div_lt_iff rp] at rz
Proof state after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
z : ℂ
lo : 16 < Complex.abs z
rz : 3 < Complex.abs z * r
⊢ 3 * Complex.abs z⁻¹ < r
Theorem: bottcher_tendsto_zero
Proof state before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
z : ℂ
lo : 16 < Complex.abs z
rz : 3 < Complex.abs z * r
⊢ 3 * Complex.abs z⁻¹ < r
Tactic:
rw [map_inv₀, mul_inv_lt_iff (lt_trans (by norm_num) lo)]
Proof state after:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
z : ℂ
lo : 16 < Complex.abs z
rz : 3 < Complex.abs z * r
⊢ 3 < Complex.abs z * r
Theorem: bottcher_tendsto_zero
Proof state before:
case h
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
z : ℂ
lo : 16 < Complex.abs z
rz : 3 < Complex.abs z * r
⊢ 3 < Complex.abs z * r
Tactic:
exact rz
Proof state after:
no goals
Theorem: bottcher_tendsto_zero
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
r : ℝ
rp : r > 0
z : ℂ
lo : 16 < Complex.abs z
rz : 3 < Complex.abs z * r
⊢ 0 < 16
Tactic:
norm_num
Proof state after:
no goals
Theorem: bottcher_analytic
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ AnalyticOn ℂ (bottcher' d) (multibrot d)ᶜ
Tactic:
set s := superF d
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ AnalyticOn ℂ (bottcher' d) (multibrot d)ᶜ
Theorem: bottcher_analytic
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ AnalyticOn ℂ (bottcher' d) (multibrot d)ᶜ
Tactic:
intro c m
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
c : ℂ
m : c ∈ (multibrot d)ᶜ
⊢ AnalyticAt ℂ (bottcher' d) c
Theorem: bottcher_analytic
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
c : ℂ
m : c ∈ (multibrot d)ᶜ
⊢ AnalyticAt ℂ (bottcher' d) c
Tactic:
apply HolomorphicAt.analyticAt I I
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
c : ℂ
m : c ∈ (multibrot d)ᶜ
⊢ HolomorphicAt I I (bottcher' d) c
Theorem: bottcher_analytic
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
c : ℂ
m : c ∈ (multibrot d)ᶜ
⊢ HolomorphicAt I I (bottcher' d) c
Tactic:
exact (s.bottcher_holomorphicOn (c, c) (multibrotPost m)).comp₂_of_eq holomorphicAt_id
  (holomorphic_coe _) rfl
Proof state after:
no goals
Theorem: bottcherHolomorphic
Proof state before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ HolomorphicOn I I (bottcher d) (multibrotExt d)
Tactic:
intro c m
Proof state after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
⊢ HolomorphicAt I I (bottcher d) c
Theorem: bottcherHolomorphic
Proof state before:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
⊢ HolomorphicAt I I (bottcher d) c
Tactic:
induction c using OnePoint.rec
Proof state after:
case h₁
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
m : ∞ ∈ multibrotExt d
⊢ HolomorphicAt I I (bottcher d) ∞

case h₂
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
x✝ : ℂ
m : ↑x✝ ∈ multibrotExt d
⊢ HolomorphicAt I I (bottcher d) ↑x✝
Theorem: bottcherHolomorphic
Proof state before:
case h₁
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
m : ∞ ∈ multibrotExt d
⊢ HolomorphicAt I I (bottcher d) ∞
Tactic:
refine holomorphicAt_fill_inf ?_ bottcher_tendsto_zero
Proof state after:
case h₁
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
m : ∞ ∈ multibrotExt d
⊢ ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I (bottcher' d) z
Theorem: bottcherHolomorphic
Proof state before:
case h₁
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
m : ∞ ∈ multibrotExt d
⊢ ∀ᶠ (z : ℂ) in atInf, HolomorphicAt I I (bottcher' d) z
Tactic:
rw [atInf_basis.eventually_iff]
Proof state after:
case h₁
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
m : ∞ ∈ multibrotExt d
⊢ ∃ i, True ∧ ∀ ⦃x : ℂ⦄, x ∈ {x | i < ‖x‖} → HolomorphicAt I I (bottcher' d) x
Theorem: bottcherHolomorphic
Proof state before:
case h₁
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
m : ∞ ∈ multibrotExt d
⊢ ∃ i, True ∧ ∀ ⦃x : ℂ⦄, x ∈ {x | i < ‖x‖} → HolomorphicAt I I (bottcher' d) x
Tactic:
use 2
Proof state after:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
m : ∞ ∈ multibrotExt d
⊢ True ∧ ∀ ⦃x : ℂ⦄, x ∈ {x | 2 < ‖x‖} → HolomorphicAt I I (bottcher' d) x
Theorem: bottcherHolomorphic
Proof state before:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
m : ∞ ∈ multibrotExt d
⊢ True ∧ ∀ ⦃x : ℂ⦄, x ∈ {x | 2 < ‖x‖} → HolomorphicAt I I (bottcher' d) x
Tactic:
simp only [true_and_iff, mem_setOf, Complex.norm_eq_abs]
Proof state after:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
m : ∞ ∈ multibrotExt d
⊢ ∀ ⦃x : ℂ⦄, 2 < Complex.abs x → HolomorphicAt I I (bottcher' d) x
Theorem: bottcherHolomorphic
Proof state before:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
m : ∞ ∈ multibrotExt d
⊢ ∀ ⦃x : ℂ⦄, 2 < Complex.abs x → HolomorphicAt I I (bottcher' d) x
Tactic:
intro z a
Proof state after:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
m : ∞ ∈ multibrotExt d
z : ℂ
a : 2 < Complex.abs z
⊢ HolomorphicAt I I (bottcher' d) z
Theorem: bottcherHolomorphic
Proof state before:
case h
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
m : ∞ ∈ multibrotExt d
z : ℂ
a : 2 < Complex.abs z
⊢ HolomorphicAt I I (bottcher' d) z
Tactic:
exact (bottcher_analytic _ (multibrot_two_lt a)).holomorphicAt I I
Proof state after:
no goals
Theorem: bottcherHolomorphic
Proof state before:
case h₂
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
x✝ : ℂ
m : ↑x✝ ∈ multibrotExt d
⊢ HolomorphicAt I I (bottcher d) ↑x✝
Tactic:
simp only [multibrotExt_coe] at m
Proof state after:
case h₂
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
x✝ : ℂ
m : x✝ ∉ multibrot d
⊢ HolomorphicAt I I (bottcher d) ↑x✝
Theorem: bottcherHolomorphic
Proof state before:
case h₂
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
x✝ : ℂ
m : x✝ ∉ multibrot d
⊢ HolomorphicAt I I (bottcher d) ↑x✝
Tactic:
exact holomorphicAt_fill_coe ((bottcher_analytic (d := d) _ m).holomorphicAt I I)
Proof state after:
no goals
Theorem: abs_bottcher
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
⊢ Complex.abs (bottcher d c) = potential d c
Tactic:
set s := superF d
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
s : Super (f d) d ∞ := superF d
⊢ Complex.abs (bottcher d c) = potential d c
Theorem: abs_bottcher
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
s : Super (f d) d ∞ := superF d
⊢ Complex.abs (bottcher d c) = potential d c
Tactic:
induction c using OnePoint.rec
Proof state after:
case h₁
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ Complex.abs (bottcher d ∞) = potential d ∞

case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
⊢ Complex.abs (bottcher d ↑x✝) = potential d ↑x✝
Theorem: abs_bottcher
Proof state before:
case h₁
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ Complex.abs (bottcher d ∞) = potential d ∞
Tactic:
simp only [bottcher, potential, fill_inf, Complex.abs.map_zero]
Proof state after:
no goals
Theorem: abs_bottcher
Proof state before:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
⊢ Complex.abs (bottcher d ↑x✝) = potential d ↑x✝
Tactic:
simp only [bottcher, potential, fill_coe]
Proof state after:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
⊢ Complex.abs (bottcher' d x✝) = ⋯.potential x✝ ↑x✝
Theorem: abs_bottcher
Proof state before:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
⊢ Complex.abs (bottcher' d x✝) = ⋯.potential x✝ ↑x✝
Tactic:
exact s.abs_bottcher
Proof state after:
no goals
Theorem: potential_continuous
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ Continuous (potential d)
Tactic:
set s := superF d
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ Continuous (potential d)
Theorem: potential_continuous
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ Continuous (potential d)
Tactic:
rw [continuous_iff_continuousAt]
Proof state after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ ∀ (x : 𝕊), ContinuousAt (potential d) x
Theorem: potential_continuous
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ ∀ (x : 𝕊), ContinuousAt (potential d) x
Tactic:
intro c
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
c : 𝕊
⊢ ContinuousAt (potential d) c
Theorem: potential_continuous
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
c : 𝕊
⊢ ContinuousAt (potential d) c
Tactic:
induction c using OnePoint.rec
Proof state after:
case h₁
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ ContinuousAt (potential d) ∞

case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
⊢ ContinuousAt (potential d) ↑x✝
Theorem: potential_continuous
Proof state before:
case h₁
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ ContinuousAt (potential d) ∞
Tactic:
have e : potential d =ᶠ[𝓝 ∞] fun c ↦ abs (bottcher d c) := by
  refine eventually_of_forall fun c ↦ ?_; rw [← abs_bottcher]
Proof state after:
case h₁
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : (𝓝 ∞).EventuallyEq (potential d) fun c => Complex.abs (bottcher d c)
⊢ ContinuousAt (potential d) ∞
Theorem: potential_continuous
Proof state before:
case h₁
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : (𝓝 ∞).EventuallyEq (potential d) fun c => Complex.abs (bottcher d c)
⊢ ContinuousAt (potential d) ∞
Tactic:
rw [continuousAt_congr e]
Proof state after:
case h₁
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : (𝓝 ∞).EventuallyEq (potential d) fun c => Complex.abs (bottcher d c)
⊢ ContinuousAt (fun c => Complex.abs (bottcher d c)) ∞
Theorem: potential_continuous
Proof state before:
case h₁
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
e : (𝓝 ∞).EventuallyEq (potential d) fun c => Complex.abs (bottcher d c)
⊢ ContinuousAt (fun c => Complex.abs (bottcher d c)) ∞
Tactic:
exact Complex.continuous_abs.continuousAt.comp
  (bottcherHolomorphic d _ multibrotExt_inf).continuousAt
Proof state after:
no goals
Theorem: potential_continuous
Proof state before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ (𝓝 ∞).EventuallyEq (potential d) fun c => Complex.abs (bottcher d c)
Tactic:
refine eventually_of_forall fun c ↦ ?_
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
c : 𝕊
⊢ potential d c = (fun c => Complex.abs (bottcher d c)) c
Theorem: potential_continuous
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
c : 𝕊
⊢ potential d c = (fun c => Complex.abs (bottcher d c)) c
Tactic:
rw [← abs_bottcher]
Proof state after:
no goals
Theorem: potential_continuous
Proof state before:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
⊢ ContinuousAt (potential d) ↑x✝
Tactic:
exact continuousAt_fill_coe ((Continuous.potential s).comp₂
  continuous_id continuous_coe).continuousAt
Proof state after:
no goals
Theorem: potential_lt_one
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
⊢ potential d c < 1 ↔ c ∈ multibrotExt d
Tactic:
set s := superF d
Proof state after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
s : Super (f d) d ∞ := superF d
⊢ potential d c < 1 ↔ c ∈ multibrotExt d
Theorem: potential_lt_one
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
s : Super (f d) d ∞ := superF d
⊢ potential d c < 1 ↔ c ∈ multibrotExt d
Tactic:
induction c using OnePoint.rec
Proof state after:
case h₁
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ potential d ∞ < 1 ↔ ∞ ∈ multibrotExt d

case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
⊢ potential d ↑x✝ < 1 ↔ ↑x✝ ∈ multibrotExt d
Theorem: potential_lt_one
Proof state before:
case h₁
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ potential d ∞ < 1 ↔ ∞ ∈ multibrotExt d
Tactic:
simp only [potential, bottcher, fill_inf, zero_lt_one, multibrotExt_inf]
Proof state after:
no goals
Theorem: potential_lt_one
Proof state before:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
⊢ potential d ↑x✝ < 1 ↔ ↑x✝ ∈ multibrotExt d
Tactic:
constructor
Proof state after:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
⊢ potential d ↑x✝ < 1 → ↑x✝ ∈ multibrotExt d

case h₂.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
⊢ ↑x✝ ∈ multibrotExt d → potential d ↑x✝ < 1
Theorem: potential_lt_one
Proof state before:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
⊢ potential d ↑x✝ < 1 → ↑x✝ ∈ multibrotExt d
Tactic:
intro h
Proof state after:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
h : potential d ↑x✝ < 1
⊢ ↑x✝ ∈ multibrotExt d
Theorem: potential_lt_one
Proof state before:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
h : potential d ↑x✝ < 1
⊢ ↑x✝ ∈ multibrotExt d
Tactic:
contrapose h
Proof state after:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
h : ↑x✝ ∉ multibrotExt d
⊢ ¬potential d ↑x✝ < 1
Theorem: potential_lt_one
Proof state before:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
h : ↑x✝ ∉ multibrotExt d
⊢ ¬potential d ↑x✝ < 1
Tactic:
simp only [not_not, not_lt, multibrot_basin', potential, fill_coe, Super.basin,
  mem_setOf, not_exists, multibrotExt_coe] at h ⊢
Proof state after:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
h : ∀ (x : ℕ), (x✝, (f d x✝)^[x] ↑x✝) ∉ ⋯.near
⊢ 1 ≤ ⋯.potential x✝ ↑x✝
Theorem: potential_lt_one
Proof state before:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
h : ∀ (x : ℕ), (x✝, (f d x✝)^[x] ↑x✝) ∉ ⋯.near
⊢ 1 ≤ ⋯.potential x✝ ↑x✝
Tactic:
rw [s.potential_eq_one]
Proof state after:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
h : ∀ (x : ℕ), (x✝, (f d x✝)^[x] ↑x✝) ∉ ⋯.near
⊢ ∀ (n : ℕ), (x✝, (f d x✝)^[n] ↑x✝) ∉ s.near
Theorem: potential_lt_one
Proof state before:
case h₂.mp
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
h : ∀ (x : ℕ), (x✝, (f d x✝)^[x] ↑x✝) ∉ ⋯.near
⊢ ∀ (n : ℕ), (x✝, (f d x✝)^[n] ↑x✝) ∉ s.near
Tactic:
exact h
Proof state after:
no goals
Theorem: potential_lt_one
Proof state before:
case h₂.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
⊢ ↑x✝ ∈ multibrotExt d → potential d ↑x✝ < 1
Tactic:
intro m
Proof state after:
case h₂.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
m : ↑x✝ ∈ multibrotExt d
⊢ potential d ↑x✝ < 1
Theorem: potential_lt_one
Proof state before:
case h₂.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
m : ↑x✝ ∈ multibrotExt d
⊢ potential d ↑x✝ < 1
Tactic:
rw [← abs_bottcher]
Proof state after:
case h₂.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
m : ↑x✝ ∈ multibrotExt d
⊢ Complex.abs (bottcher d ↑x✝) < 1
Theorem: potential_lt_one
Proof state before:
case h₂.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
m : ↑x✝ ∈ multibrotExt d
⊢ Complex.abs (bottcher d ↑x✝) < 1
Tactic:
simp only [bottcher, fill_coe]
Proof state after:
case h₂.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
m : ↑x✝ ∈ multibrotExt d
⊢ Complex.abs (bottcher' d x✝) < 1
Theorem: potential_lt_one
Proof state before:
case h₂.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
m : ↑x✝ ∈ multibrotExt d
⊢ Complex.abs (bottcher' d x✝) < 1
Tactic:
simp only [multibrotExt_coe] at m
Proof state after:
case h₂.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
m : x✝ ∉ multibrot d
⊢ Complex.abs (bottcher' d x✝) < 1
Theorem: potential_lt_one
Proof state before:
case h₂.mpr
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
x✝ : ℂ
m : x✝ ∉ multibrot d
⊢ Complex.abs (bottcher' d x✝) < 1
Tactic:
exact s.bottcher_lt_one (multibrotPost m)
Proof state after:
no goals
Theorem: potential_nonneg
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
⊢ 0 ≤ potential d c
Tactic:
induction c using OnePoint.rec
Proof state after:
case h₁
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 0 ≤ potential d ∞

case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x✝ : ℂ
⊢ 0 ≤ potential d ↑x✝
Theorem: potential_nonneg
Proof state before:
case h₁
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ 0 ≤ potential d ∞
Tactic:
simp only [potential, fill_inf, le_refl]
Proof state after:
no goals
Theorem: potential_nonneg
Proof state before:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x✝ : ℂ
⊢ 0 ≤ potential d ↑x✝
Tactic:
simp only [potential, fill_coe]
Proof state after:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x✝ : ℂ
⊢ 0 ≤ ⋯.potential x✝ ↑x✝
Theorem: potential_nonneg
Proof state before:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x✝ : ℂ
⊢ 0 ≤ ⋯.potential x✝ ↑x✝
Tactic:
exact (superF d).potential_nonneg
Proof state after:
no goals
Theorem: potential_eq_zero
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
⊢ potential d c = 0 ↔ c = ∞
Tactic:
induction c using OnePoint.rec
Proof state after:
case h₁
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ potential d ∞ = 0 ↔ ∞ = ∞

case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x✝ : ℂ
⊢ potential d ↑x✝ = 0 ↔ ↑x✝ = ∞
Theorem: potential_eq_zero
Proof state before:
case h₁
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ potential d ∞ = 0 ↔ ∞ = ∞
Tactic:
simp only [potential, fill_inf, eq_self_iff_true]
Proof state after:
no goals
Theorem: potential_eq_zero
Proof state before:
case h₂
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
x✝ : ℂ
⊢ potential d ↑x✝ = 0 ↔ ↑x✝ = ∞
Tactic:
simp only [potential, fill_coe, (superF d).potential_eq_zero_of_onePreimage]
Proof state after:
no goals
Theorem: bottcherNontrivial
Proof state before:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
⊢ NontrivialHolomorphicAt (bottcher d) c
Tactic:
by_cases h : ∃ᶠ e in 𝓝 c, bottcher d e ≠ bottcher d c
Proof state after:
case pos
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
h : ∃ᶠ (e : 𝕊) in 𝓝 c, bottcher d e ≠ bottcher d c
⊢ NontrivialHolomorphicAt (bottcher d) c

case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
h : ¬∃ᶠ (e : 𝕊) in 𝓝 c, bottcher d e ≠ bottcher d c
⊢ NontrivialHolomorphicAt (bottcher d) c
Theorem: bottcherNontrivial
Proof state before:
case pos
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
h : ∃ᶠ (e : 𝕊) in 𝓝 c, bottcher d e ≠ bottcher d c
⊢ NontrivialHolomorphicAt (bottcher d) c

case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
h : ¬∃ᶠ (e : 𝕊) in 𝓝 c, bottcher d e ≠ bottcher d c
⊢ NontrivialHolomorphicAt (bottcher d) c
Tactic:
exact
  { holomorphicAt := bottcherHolomorphic d _ m
    nonconst := h }
Proof state after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
h : ¬∃ᶠ (e : 𝕊) in 𝓝 c, bottcher d e ≠ bottcher d c
⊢ NontrivialHolomorphicAt (bottcher d) c
Theorem: bottcherNontrivial
Proof state before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
h : ¬∃ᶠ (e : 𝕊) in 𝓝 c, bottcher d e ≠ bottcher d c
⊢ NontrivialHolomorphicAt (bottcher d) c
Tactic:
exfalso
Proof state after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
h : ¬∃ᶠ (e : 𝕊) in 𝓝 c, bottcher d e ≠ bottcher d c
⊢ False
Theorem: bottcherNontrivial
Proof state before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
h : ¬∃ᶠ (e : 𝕊) in 𝓝 c, bottcher d e ≠ bottcher d c
⊢ False
Tactic:
simp only [Filter.not_frequently, not_not] at h
Proof state after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
h : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = bottcher d c
⊢ False
Theorem: bottcherNontrivial
Proof state before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
h : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = bottcher d c
⊢ False
Tactic:
set b := bottcher d c
Proof state after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
⊢ False
Theorem: bottcherNontrivial
Proof state before:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
⊢ False
Tactic:
have b1 : abs b < 1 := by simp only [abs_bottcher, potential_lt_one, m, b]
Proof state after:
case neg
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
b : ℂ := bottcher d c
h : ∀ᶠ (x : 𝕊) in 𝓝 c, bottcher d x = b
b1 : Complex.abs b < 1
⊢ False