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

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
⊢ Continuous (potential d)
Tactic:
set s := superF d
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ Continuous (potential d)

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ Continuous (potential d)
Tactic:
rw [continuous_iff_continuousAt]
State after:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ ∀ (x : 𝕊), ContinuousAt (potential d) x

State before:
c : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
⊢ ∀ (x : 𝕊), ContinuousAt (potential d) x
Tactic:
intro c
State after:
c✝ : ℂ
d : ℕ
inst✝ : Fact (2 ≤ d)
s : Super (f d) d ∞ := superF d
c : 𝕊
⊢ ContinuousAt (potential d) c

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

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

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

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

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 ↦ ?_
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

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

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