Theorem: Super.potential_eq_zero (Ray/Dynamics/Potential.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 : ℂ
a z : S
d n : ℕ
s : Super f d a
⊢ s.potential c z = 0 ↔ ∃ n, (f c)^[n] z = a
Tactic:
constructor
State after:
case mp
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
⊢ s.potential c z = 0 → ∃ n, (f c)^[n] z = a

case mpr
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
⊢ (∃ n, (f c)^[n] z = a) → s.potential c z = 0

State before:
case mp
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
⊢ s.potential c z = 0 → ∃ n, (f c)^[n] z = a
Tactic:
intro h
State after:
case mp
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
h : s.potential c z = 0
⊢ ∃ n, (f c)^[n] z = a

State before:
case mp
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
h : s.potential c z = 0
⊢ ∃ n, (f c)^[n] z = a
Tactic:
by_cases r : ∃ n, (c, (f c)^[n] z) ∈ s.near
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
h : s.potential c z = 0
r : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ ∃ n, (f c)^[n] z = a

case neg
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
h : s.potential c z = 0
r : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ ∃ n, (f c)^[n] z = a

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 : ℂ
a z : S
d n : ℕ
s : Super f d a
h : s.potential c z = 0
r : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ ∃ n, (f c)^[n] z = a
Tactic:
rcases r with ⟨n, r⟩
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 : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
h : s.potential c z = 0
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
⊢ ∃ n, (f c)^[n] z = a

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 : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
h : s.potential c z = 0
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
⊢ ∃ n, (f c)^[n] z = a
Tactic:
simp only [s.potential_eq r, Super.potential',
  Real.rpow_eq_zero_iff_of_nonneg (Complex.abs.nonneg _), Complex.abs.eq_zero,
  s.bottcherNear_eq_zero r] at h
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 : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
h : (f c)^[n] z = a ∧ (↑d ^ n)⁻¹ ≠ 0
⊢ ∃ n, (f c)^[n] z = a

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 : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
h : (f c)^[n] z = a ∧ (↑d ^ n)⁻¹ ≠ 0
⊢ ∃ n, (f c)^[n] z = a
Tactic:
use n, h.1
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
h : s.potential c z = 0
r : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ ∃ n, (f c)^[n] z = a
Tactic:
rw [not_exists] at r
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 : ℂ
a z : S
d n : ℕ
s : Super f d a
h : s.potential c z = 0
r : ∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
⊢ ∃ n, (f c)^[n] z = a

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 : ℂ
a z : S
d n : ℕ
s : Super f d a
h : s.potential c z = 0
r : ∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
⊢ ∃ n, (f c)^[n] z = a
Tactic:
simp only [s.potential_eq_one r, one_ne_zero] at h
State after:
no goals

State before:
case mpr
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
⊢ (∃ n, (f c)^[n] z = a) → s.potential c z = 0
Tactic:
intro p
State after:
case mpr
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ∃ n, (f c)^[n] z = a
⊢ s.potential c z = 0

State before:
case mpr
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n : ℕ
s : Super f d a
p : ∃ n, (f c)^[n] z = a
⊢ s.potential c z = 0
Tactic:
rcases p with ⟨n, p⟩
State after:
case mpr.intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
p : (f c)^[n] z = a
⊢ s.potential c z = 0

State before:
case mpr.intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
p : (f c)^[n] z = a
⊢ s.potential c z = 0
Tactic:
have nz : d^n > 0 := pow_pos s.dp _
State after:
case mpr.intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
p : (f c)^[n] z = a
nz : d ^ n > 0
⊢ s.potential c z = 0

State before:
case mpr.intro
S : Type
inst✝⁴ : TopologicalSpace S
inst✝³ : CompactSpace S
inst✝² : T3Space S
inst✝¹ : ChartedSpace ℂ S
inst✝ : AnalyticManifold I S
f : ℂ → S → S
c : ℂ
a z : S
d n✝ : ℕ
s : Super f d a
n : ℕ
p : (f c)^[n] z = a
nz : d ^ n > 0
⊢ s.potential c z = 0
Tactic:
rw [← pow_eq_zero_iff nz.ne', ← s.potential_eqn_iter n, p, s.potential_a]
State after:
no goals