Theorem: bottcherHolomorphic (Ray/Dynamics/Multibrot/Basic.lean)

State before:
c : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ HolomorphicOn I I (bottcher d) (multibrotExt d)
Tactic:
intro c m
State after:
c✝ : ℂ
d✝ : ℕ
inst✝¹ : Fact (2 ≤ d✝)
d : ℕ
inst✝ : Fact (2 ≤ d)
c : 𝕊
m : c ∈ multibrotExt d
⊢ HolomorphicAt I I (bottcher d) c

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
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✝

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
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

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]
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

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
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

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]
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

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
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

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
State after:
no goals

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
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✝

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)
State after:
no goals