Theorem: Super.abs_bottcher (Ray/Dynamics/Bottcher.lean)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
⊢ Complex.abs (s.bottcher c z) = s.potential c z
Tactic:
have base : ∀ {c z}, (c, z) ∈ s.post → abs (s.bottcher c z) = s.potential c z := by
  intro c z m; rcases s.ray_surj m with ⟨x, m, e⟩; rw [← e, s.bottcher_ray m, s.ray_potential m]
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
base : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → Complex.abs (s.bottcher c z) = s.potential c z
⊢ Complex.abs (s.bottcher c z) = s.potential c z

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
base : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → Complex.abs (s.bottcher c z) = s.potential c z
⊢ Complex.abs (s.bottcher c z) = s.potential c z
Tactic:
by_cases m : (c, z) ∈ s.basin
State after:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
base : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → Complex.abs (s.bottcher c z) = s.potential c z
m : (c, z) ∈ s.basin
⊢ Complex.abs (s.bottcher c z) = s.potential c z

case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
base : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → Complex.abs (s.bottcher c z) = s.potential c z
m : (c, z) ∉ s.basin
⊢ Complex.abs (s.bottcher c z) = s.potential c z

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
⊢ ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → Complex.abs (s.bottcher c z) = s.potential c z
Tactic:
intro c z m
State after:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
m : (c, z) ∈ s.post
⊢ Complex.abs (s.bottcher c z) = s.potential c z

State before:
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
m : (c, z) ∈ s.post
⊢ Complex.abs (s.bottcher c z) = s.potential c z
Tactic:
rcases s.ray_surj m with ⟨x, m, e⟩
State after:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
m✝ : (c, z) ∈ s.post
x : ℂ
m : (c, x) ∈ s.ext
e : s.ray c x = z
⊢ Complex.abs (s.bottcher c z) = s.potential c z

State before:
case intro.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c✝ x✝ : ℂ
a z✝ : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
c : ℂ
z : S
m✝ : (c, z) ∈ s.post
x : ℂ
m : (c, x) ∈ s.ext
e : s.ray c x = z
⊢ Complex.abs (s.bottcher c z) = s.potential c z
Tactic:
rw [← e, s.bottcher_ray m, s.ray_potential m]
State after:
no goals

State before:
case pos
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
base : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → Complex.abs (s.bottcher c z) = s.potential c z
m : (c, z) ∈ s.basin
⊢ Complex.abs (s.bottcher c z) = s.potential c z
Tactic:
rcases s.basin_post m with ⟨n, p⟩
State after:
case pos.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
base : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → Complex.abs (s.bottcher c z) = s.potential c z
m : (c, z) ∈ s.basin
n : ℕ
p : (c, (f c)^[n] z) ∈ s.post
⊢ Complex.abs (s.bottcher c z) = s.potential c z

State before:
case pos.intro
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n✝ : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
base : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → Complex.abs (s.bottcher c z) = s.potential c z
m : (c, z) ∈ s.basin
n : ℕ
p : (c, (f c)^[n] z) ∈ s.post
⊢ Complex.abs (s.bottcher c z) = s.potential c z
Tactic:
rw [← Real.pow_rpow_inv_natCast (Complex.abs.nonneg _) (pow_ne_zero n s.d0), ←
  Complex.abs.map_pow, ← s.bottcher_eqn_iter n, base p, s.potential_eqn_iter,
  Real.pow_rpow_inv_natCast s.potential_nonneg (pow_ne_zero n s.d0)]
State after:
no goals

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
base : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → Complex.abs (s.bottcher c z) = s.potential c z
m : (c, z) ∉ s.basin
⊢ Complex.abs (s.bottcher c z) = s.potential c z
Tactic:
have m' := m
State after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
base : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → Complex.abs (s.bottcher c z) = s.potential c z
m m' : (c, z) ∉ s.basin
⊢ Complex.abs (s.bottcher c z) = s.potential c z

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
base : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → Complex.abs (s.bottcher c z) = s.potential c z
m m' : (c, z) ∉ s.basin
⊢ Complex.abs (s.bottcher c z) = s.potential c z
Tactic:
simp only [Super.basin, not_exists, mem_setOf] at m'
State after:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
base : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → Complex.abs (s.bottcher c z) = s.potential c z
m : (c, z) ∉ s.basin
m' : ∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
⊢ Complex.abs (s.bottcher c z) = s.potential c z

State before:
case neg
S : Type
inst✝⁵ : TopologicalSpace S
inst✝⁴ : CompactSpace S
inst✝³ : T3Space S
inst✝² : ChartedSpace ℂ S
inst✝¹ : AnalyticManifold I S
f : ℂ → S → S
c x : ℂ
a z : S
d n : ℕ
s✝ : Super f d a
y : ℂ × ℂ
s : Super f d a
inst✝ : OnePreimage s
base : ∀ {c : ℂ} {z : S}, (c, z) ∈ s.post → Complex.abs (s.bottcher c z) = s.potential c z
m : (c, z) ∉ s.basin
m' : ∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
⊢ Complex.abs (s.bottcher c z) = s.potential c z
Tactic:
simp only [s.bottcher_not_basin m, Complex.abs.map_one, s.potential_eq_one m']
State after:
no goals