Theorem: Super.potential_eq' (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
c : ℂ
z : S
n0 n1 : ℕ
n0s : (c, (f c)^[n0] z) ∈ s.near
n1s : (c, (f c)^[n1] z) ∈ s.near
⊢ ∀ {n0 n1 : ℕ},
    n0 ≤ n1 → (c, (f c)^[n0] z) ∈ s.near → (c, (f c)^[n1] z) ∈ s.near → s.potential' c z n0 = s.potential' c z n1
Tactic:
clear n0s n1s n0 n1
State after:
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
c : ℂ
z : S
⊢ ∀ {n0 n1 : ℕ},
    n0 ≤ n1 → (c, (f c)^[n0] z) ∈ s.near → (c, (f c)^[n1] z) ∈ s.near → s.potential' c z n0 = s.potential' c z n1

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
c : ℂ
z : S
⊢ ∀ {n0 n1 : ℕ},
    n0 ≤ n1 → (c, (f c)^[n0] z) ∈ s.near → (c, (f c)^[n1] z) ∈ s.near → s.potential' c z n0 = s.potential' c z n1
Tactic:
intro n0 n1 n01 n0s _
State after:
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
⊢ s.potential' c z n0 = s.potential' c z n1

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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
⊢ s.potential' c z n0 = s.potential' c z n1
Tactic:
rw [← Nat.sub_add_cancel n01]
State after:
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
⊢ s.potential' c z n0 = s.potential' c z (n1 - n0 + n0)

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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
⊢ s.potential' c z n0 = s.potential' c z (n1 - n0 + n0)
Tactic:
have m : ∀ k, (c, (f c)^[n0 + k] z) ∈ s.near := by
  intro k; rw [Nat.add_comm]
  simp only [Function.iterate_add, s.iter_stays_near n0s k, Function.comp]
State after:
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
⊢ s.potential' c z n0 = s.potential' c z (n1 - n0 + n0)

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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
⊢ s.potential' c z n0 = s.potential' c z (n1 - n0 + n0)
Tactic:
generalize hk : n1 - n0 = k
State after:
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
hk : n1 - n0 = k
⊢ s.potential' c z n0 = s.potential' c z (k + n0)

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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
hk : n1 - n0 = k
⊢ s.potential' c z n0 = s.potential' c z (k + n0)
Tactic:
rw [Nat.add_comm]
State after:
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
hk : n1 - n0 = k
⊢ s.potential' c z n0 = s.potential' c z (n0 + k)

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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
hk : n1 - n0 = k
⊢ s.potential' c z n0 = s.potential' c z (n0 + k)
Tactic:
clear hk
State after:
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
⊢ s.potential' c z n0 = s.potential' c z (n0 + k)

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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
⊢ s.potential' c z n0 = s.potential' c z (n0 + k)
Tactic:
induction' k with k h
State after:
case zero
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
⊢ s.potential' c z n0 = s.potential' c z (n0 + 0)

case succ
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ s.potential' c z n0 = s.potential' c z (n0 + (k + 1))

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
c : ℂ
z : S
n0 n1 : ℕ
n0s : (c, (f c)^[n0] z) ∈ s.near
n1s : (c, (f c)^[n1] z) ∈ s.near
h :
  ∀ {n0 n1 : ℕ},
    n0 ≤ n1 → (c, (f c)^[n0] z) ∈ s.near → (c, (f c)^[n1] z) ∈ s.near → s.potential' c z n0 = s.potential' c z n1
⊢ s.potential' c z n0 = s.potential' c z n1
Tactic:
by_cases n01 : n0 ≤ n1
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
c : ℂ
z : S
n0 n1 : ℕ
n0s : (c, (f c)^[n0] z) ∈ s.near
n1s : (c, (f c)^[n1] z) ∈ s.near
h :
  ∀ {n0 n1 : ℕ},
    n0 ≤ n1 → (c, (f c)^[n0] z) ∈ s.near → (c, (f c)^[n1] z) ∈ s.near → s.potential' c z n0 = s.potential' c z n1
n01 : n0 ≤ n1
⊢ s.potential' c z n0 = s.potential' c z n1

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
c : ℂ
z : S
n0 n1 : ℕ
n0s : (c, (f c)^[n0] z) ∈ s.near
n1s : (c, (f c)^[n1] z) ∈ s.near
h :
  ∀ {n0 n1 : ℕ},
    n0 ≤ n1 → (c, (f c)^[n0] z) ∈ s.near → (c, (f c)^[n1] z) ∈ s.near → s.potential' c z n0 = s.potential' c z n1
n01 : ¬n0 ≤ n1
⊢ s.potential' c z n0 = s.potential' c z n1

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
c : ℂ
z : S
n0 n1 : ℕ
n0s : (c, (f c)^[n0] z) ∈ s.near
n1s : (c, (f c)^[n1] z) ∈ s.near
h :
  ∀ {n0 n1 : ℕ},
    n0 ≤ n1 → (c, (f c)^[n0] z) ∈ s.near → (c, (f c)^[n1] z) ∈ s.near → s.potential' c z n0 = s.potential' c z n1
n01 : n0 ≤ n1
⊢ s.potential' c z n0 = s.potential' c z n1
Tactic:
exact h n01 n0s n1s
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
c : ℂ
z : S
n0 n1 : ℕ
n0s : (c, (f c)^[n0] z) ∈ s.near
n1s : (c, (f c)^[n1] z) ∈ s.near
h :
  ∀ {n0 n1 : ℕ},
    n0 ≤ n1 → (c, (f c)^[n0] z) ∈ s.near → (c, (f c)^[n1] z) ∈ s.near → s.potential' c z n0 = s.potential' c z n1
n01 : ¬n0 ≤ n1
⊢ s.potential' c z n0 = s.potential' c z n1
Tactic:
exact (h (not_le.mp n01).le n1s n0s).symm
State after:
no goals

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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
⊢ ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
Tactic:
intro k
State after:
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
k : ℕ
⊢ (c, (f c)^[n0 + k] z) ∈ s.near

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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
k : ℕ
⊢ (c, (f c)^[n0 + k] z) ∈ s.near
Tactic:
rw [Nat.add_comm]
State after:
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
k : ℕ
⊢ (c, (f c)^[k + n0] z) ∈ s.near

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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
k : ℕ
⊢ (c, (f c)^[k + n0] z) ∈ s.near
Tactic:
simp only [Function.iterate_add, s.iter_stays_near n0s k, Function.comp]
State after:
no goals

State before:
case zero
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
⊢ s.potential' c z n0 = s.potential' c z (n0 + 0)
Tactic:
simp only [Nat.zero_eq, add_zero]
State after:
no goals

State before:
case succ
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ s.potential' c z n0 = s.potential' c z (n0 + (k + 1))
Tactic:
simp only [Nat.add_succ, Function.iterate_succ', Super.potential', Function.comp]
State after:
case succ
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ Complex.abs (s.bottcherNear c ((f c)^[n0] z)) ^ (↑d ^ n0)⁻¹ =
    Complex.abs (s.bottcherNear c (f c ((f c)^[n0 + k] z))) ^ (↑d ^ (n0 + k).succ)⁻¹

State before:
case succ
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ Complex.abs (s.bottcherNear c ((f c)^[n0] z)) ^ (↑d ^ n0)⁻¹ =
    Complex.abs (s.bottcherNear c (f c ((f c)^[n0 + k] z))) ^ (↑d ^ (n0 + k).succ)⁻¹
Tactic:
rw [s.bottcherNear_eqn (m k)]
State after:
case succ
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ Complex.abs (s.bottcherNear c ((f c)^[n0] z)) ^ (↑d ^ n0)⁻¹ =
    Complex.abs (s.bottcherNear c ((f c)^[n0 + k] z) ^ d) ^ (↑d ^ (n0 + k).succ)⁻¹

State before:
case succ
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ Complex.abs (s.bottcherNear c ((f c)^[n0] z)) ^ (↑d ^ n0)⁻¹ =
    Complex.abs (s.bottcherNear c ((f c)^[n0 + k] z) ^ d) ^ (↑d ^ (n0 + k).succ)⁻¹
Tactic:
rw [pow_succ' _ (n0 + k), mul_inv, Complex.abs.map_pow, Real.rpow_mul, ← Real.rpow_natCast _ d]
State after:
case succ
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ Complex.abs (s.bottcherNear c ((f c)^[n0] z)) ^ (↑d ^ n0)⁻¹ =
    ((Complex.abs (s.bottcherNear c ((f c)^[n0 + k] z)) ^ ↑d) ^ (↑d)⁻¹) ^ (↑d ^ (n0 + k))⁻¹

case succ.hx
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ 0 ≤ Complex.abs (s.bottcherNear c ((f c)^[n0 + k] z)) ^ d

State before:
case succ
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ Complex.abs (s.bottcherNear c ((f c)^[n0] z)) ^ (↑d ^ n0)⁻¹ =
    ((Complex.abs (s.bottcherNear c ((f c)^[n0 + k] z)) ^ ↑d) ^ (↑d)⁻¹) ^ (↑d ^ (n0 + k))⁻¹

case succ.hx
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ 0 ≤ Complex.abs (s.bottcherNear c ((f c)^[n0 + k] z)) ^ d
Tactic:
rw [← Real.rpow_mul (Complex.abs.nonneg _) _ d⁻¹,
  mul_inv_cancel (s.superAtC.s (Set.mem_univ c)).drz, Real.rpow_one]
State after:
case succ
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ Complex.abs (s.bottcherNear c ((f c)^[n0] z)) ^ (↑d ^ n0)⁻¹ =
    Complex.abs (s.bottcherNear c ((f c)^[n0 + k] z)) ^ (↑d ^ (n0 + k))⁻¹

case succ.hx
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ 0 ≤ Complex.abs (s.bottcherNear c ((f c)^[n0 + k] z)) ^ d

State before:
case succ
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ Complex.abs (s.bottcherNear c ((f c)^[n0] z)) ^ (↑d ^ n0)⁻¹ =
    Complex.abs (s.bottcherNear c ((f c)^[n0 + k] z)) ^ (↑d ^ (n0 + k))⁻¹

case succ.hx
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ 0 ≤ Complex.abs (s.bottcherNear c ((f c)^[n0 + k] z)) ^ d
Tactic:
exact h
State after:
case succ.hx
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ 0 ≤ Complex.abs (s.bottcherNear c ((f c)^[n0 + k] z)) ^ d

State before:
case succ.hx
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
c : ℂ
z : S
n0 n1 : ℕ
n01 : n0 ≤ n1
n0s : (c, (f c)^[n0] z) ∈ s.near
a✝ : (c, (f c)^[n1] z) ∈ s.near
m : ∀ (k : ℕ), (c, (f c)^[n0 + k] z) ∈ s.near
k : ℕ
h : s.potential' c z n0 = s.potential' c z (n0 + k)
⊢ 0 ≤ Complex.abs (s.bottcherNear c ((f c)^[n0 + k] z)) ^ d
Tactic:
bound
State after:
no goals