internlm/Lean-Github huggingface dataset:
Theorem: Super.potential_eq'
Proof 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
Proof 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
Theorem: Super.potential_eq'
Proof 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
Proof state after:
no goals
Theorem: Super.potential_eq
Proof 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
k : ℕ
ks : (c, (f c)^[k] z) ∈ s.near
⊢ s.potential c z = s.potential' c z k
Tactic:
have h : ∃ k, (c, (f c)^[k] z) ∈ s.near := ⟨k,ks⟩
Proof 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
k : ℕ
ks : (c, (f c)^[k] z) ∈ s.near
h : ∃ k, (c, (f c)^[k] z) ∈ s.near
⊢ s.potential c z = s.potential' c z k
Theorem: Super.potential_eq
Proof 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
k : ℕ
ks : (c, (f c)^[k] z) ∈ s.near
h : ∃ k, (c, (f c)^[k] z) ∈ s.near
⊢ s.potential c z = s.potential' c z k
Tactic:
simp only [Super.potential, h, dif_pos]
Proof 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
k : ℕ
ks : (c, (f c)^[k] z) ∈ s.near
h : ∃ k, (c, (f c)^[k] z) ∈ s.near
⊢ s.potential' c z (Nat.find ⋯) = s.potential' c z k
Theorem: Super.potential_eq
Proof 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
k : ℕ
ks : (c, (f c)^[k] z) ∈ s.near
h : ∃ k, (c, (f c)^[k] z) ∈ s.near
⊢ s.potential' c z (Nat.find ⋯) = s.potential' c z k
Tactic:
exact s.potential_eq' (Nat.find_spec h) ks
Proof state after:
no goals
Theorem: Super.abs_bottcherNear
Proof 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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
⊢ Complex.abs (s.bottcherNear c ((f c)^[n] z)) = s.potential c z ^ d ^ n
Tactic:
simp only [s.potential_eq r, Super.potential']
Proof 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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
⊢ Complex.abs (s.bottcherNear c ((f c)^[n] z)) = (Complex.abs (s.bottcherNear c ((f c)^[n] z)) ^ (↑d ^ n)⁻¹) ^ d ^ n
Theorem: Super.abs_bottcherNear
Proof 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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
⊢ Complex.abs (s.bottcherNear c ((f c)^[n] z)) = (Complex.abs (s.bottcherNear c ((f c)^[n] z)) ^ (↑d ^ n)⁻¹) ^ d ^ n
Tactic:
rw [← Real.rpow_natCast, ← Real.rpow_mul (Complex.abs.nonneg _), Nat.cast_pow, inv_mul_cancel,
  Real.rpow_one]
Proof 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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
⊢ ↑d ^ n ≠ 0
Theorem: Super.abs_bottcherNear
Proof 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
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
⊢ ↑d ^ n ≠ 0
Tactic:
exact pow_ne_zero _ (Nat.cast_ne_zero.mpr s.d0)
Proof state after:
no goals
Theorem: Super.potential_a
Proof 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 a = 0
Tactic:
have r : (c, (f c)^[0] a) ∈ s.near := by simp only [Function.iterate_zero, s.mem_near, id]
Proof 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
r : (c, (f c)^[0] a) ∈ s.near
⊢ s.potential c a = 0
Theorem: Super.potential_a
Proof 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
r : (c, (f c)^[0] a) ∈ s.near
⊢ s.potential c a = 0
Tactic:
simp only [s.potential_eq r, Super.potential', Function.iterate_zero, id, s.bottcherNear_a,
  Complex.abs.map_zero, pow_zero, inv_one, Real.rpow_one]
Proof state after:
no goals
Theorem: Super.potential_a
Proof 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, (f c)^[0] a) ∈ s.near
Tactic:
simp only [Function.iterate_zero, s.mem_near, id]
Proof state after:
no goals
Theorem: Super.potential_eq_one
Proof 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✝
a : ∀ (n : ℕ), (c, (f c)^[n] z) ∉ s.near
⊢ s.potential c z = 1
Tactic:
simp only [Super.potential, not_exists.mpr a, not_false_iff, dif_neg, and_false_iff]
Proof state after:
no goals
Theorem: Super.potential_lt_one
Proof 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✝
a : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ s.potential c z < 1
Tactic:
simp only [Super.potential, a, dif_pos, Super.potential']
Proof 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✝
a : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ Complex.abs (s.bottcherNear c ((f c)^[Nat.find ⋯] z)) ^ (↑d ^ Nat.find ⋯)⁻¹ < 1
Theorem: Super.potential_lt_one
Proof 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✝
a : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ Complex.abs (s.bottcherNear c ((f c)^[Nat.find ⋯] z)) ^ (↑d ^ Nat.find ⋯)⁻¹ < 1
Tactic:
refine Real.rpow_lt_one (Complex.abs.nonneg _) ?_ (by bound)
Proof 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✝
a : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ Complex.abs (s.bottcherNear c ((f c)^[Nat.find ⋯] z)) < 1
Theorem: Super.potential_lt_one
Proof 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✝
a : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ Complex.abs (s.bottcherNear c ((f c)^[Nat.find ⋯] z)) < 1
Tactic:
exact s.bottcherNear_lt_one (Nat.find_spec a)
Proof state after:
no goals
Theorem: Super.potential_lt_one
Proof 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✝
a : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ 0 < (↑d ^ Nat.find ⋯)⁻¹
Tactic:
bound
Proof state after:
no goals
Theorem: Super.potential_lt_one_iff
Proof 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 < 1 ↔ ∃ n, (c, (f c)^[n] z) ∈ s.near
Tactic:
refine ⟨?_, s.potential_lt_one⟩
Proof 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
⊢ s.potential c z < 1 → ∃ n, (c, (f c)^[n] z) ∈ s.near
Theorem: Super.potential_lt_one_iff
Proof 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 < 1 → ∃ n, (c, (f c)^[n] z) ∈ s.near
Tactic:
intro h
Proof 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
h : s.potential c z < 1
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.near
Theorem: Super.potential_lt_one_iff
Proof 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
h : s.potential c z < 1
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.near
Tactic:
contrapose h
Proof 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
h : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ ¬s.potential c z < 1
Theorem: Super.potential_lt_one_iff
Proof 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
h : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ ¬s.potential c z < 1
Tactic:
simp only [not_exists] at h
Proof 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
h : ∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
⊢ ¬s.potential c z < 1
Theorem: Super.potential_lt_one_iff
Proof 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
h : ∀ (x : ℕ), (c, (f c)^[x] z) ∉ s.near
⊢ ¬s.potential c z < 1
Tactic:
simp only [s.potential_eq_one h, lt_self_iff_false, not_false_iff]
Proof state after:
no goals
Theorem: Super.potential_le_one
Proof 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 ≤ 1
Tactic:
by_cases a : ∃ n, (c, (f c)^[n] z) ∈ s.near
Proof 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✝
a : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ s.potential c z ≤ 1

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✝
a : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ s.potential c z ≤ 1
Theorem: Super.potential_le_one
Proof 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✝
a : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ s.potential c z ≤ 1

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✝
a : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ s.potential c z ≤ 1
Tactic:
exact (s.potential_lt_one a).le
Proof 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✝
a : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ s.potential c z ≤ 1
Theorem: Super.potential_le_one
Proof 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✝
a : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ s.potential c z ≤ 1
Tactic:
exact le_of_eq (s.potential_eq_one (not_exists.mp a))
Proof state after:
no goals
Theorem: Super.potential_nonneg
Proof 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
⊢ 0 ≤ s.potential c z
Tactic:
by_cases r : ∃ n, (c, (f c)^[n] z) ∈ s.near
Proof 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
r : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ 0 ≤ 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 : ℂ
a z : S
d n : ℕ
s : Super f d a
r : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ 0 ≤ s.potential c z
Theorem: Super.potential_nonneg
Proof 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
r : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ 0 ≤ 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 : ℂ
a z : S
d n : ℕ
s : Super f d a
r : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ 0 ≤ s.potential c z
Tactic:
rcases r with ⟨n, r⟩
Proof 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
⊢ 0 ≤ 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 : ℂ
a z : S
d n : ℕ
s : Super f d a
r : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ 0 ≤ s.potential c z
Theorem: Super.potential_nonneg
Proof 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
⊢ 0 ≤ 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 : ℂ
a z : S
d n : ℕ
s : Super f d a
r : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ 0 ≤ s.potential c z
Tactic:
simp only [s.potential_eq r, Super.potential']
Proof 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
⊢ 0 ≤ Complex.abs (s.bottcherNear c ((f c)^[n] z)) ^ (↑d ^ n)⁻¹

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
r : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ 0 ≤ s.potential c z
Theorem: Super.potential_nonneg
Proof 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
⊢ 0 ≤ Complex.abs (s.bottcherNear c ((f c)^[n] z)) ^ (↑d ^ n)⁻¹

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
r : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ 0 ≤ s.potential c z
Tactic:
bound
Proof 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
r : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ 0 ≤ s.potential c z
Theorem: Super.potential_nonneg
Proof 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
r : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ 0 ≤ s.potential c z
Tactic:
simp only [s.potential_eq_one (not_exists.mp r), zero_le_one]
Proof state after:
no goals
Theorem: Super.potential_eqn
Proof 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 (f c z) = s.potential c z ^ d
Tactic:
by_cases a : ∃ n, (c, (f c)^[n] z) ∈ s.near
Proof 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✝
a : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ s.potential c (f c z) = s.potential c z ^ d

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✝
a : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ s.potential c (f c z) = s.potential c z ^ d
Theorem: Super.potential_eqn
Proof 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✝
a : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ s.potential c (f c z) = s.potential c z ^ d
Tactic:
rcases a with ⟨n, a⟩
Proof 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 : ℕ
a : (c, (f c)^[n] z) ∈ s.near
⊢ s.potential c (f c z) = s.potential c z ^ d
Theorem: Super.potential_eqn
Proof 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 : ℕ
a : (c, (f c)^[n] z) ∈ s.near
⊢ s.potential c (f c z) = s.potential c z ^ d
Tactic:
have a' : (c, (f c)^[n] (f c z)) ∈ s.near := by
  simp only [← Function.iterate_succ_apply, Function.iterate_succ', s.stays_near a,
    Function.comp]
Proof 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 : ℕ
a : (c, (f c)^[n] z) ∈ s.near
a' : (c, (f c)^[n] (f c z)) ∈ s.near
⊢ s.potential c (f c z) = s.potential c z ^ d
Theorem: Super.potential_eqn
Proof 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 : ℕ
a : (c, (f c)^[n] z) ∈ s.near
a' : (c, (f c)^[n] (f c z)) ∈ s.near
⊢ s.potential c (f c z) = s.potential c z ^ d
Tactic:
simp only [s.potential_eq a, s.potential_eq a', Super.potential', ← Function.iterate_succ_apply,
  Function.iterate_succ', s.bottcherNear_eqn a, Complex.abs.map_pow, ← Real.rpow_natCast, ←
  Real.rpow_mul (Complex.abs.nonneg _), mul_comm, Function.comp]
Proof state after:
no goals
Theorem: Super.potential_eqn
Proof 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✝
n : ℕ
a : (c, (f c)^[n] z) ∈ s.near
⊢ (c, (f c)^[n] (f c z)) ∈ s.near
Tactic:
simp only [← Function.iterate_succ_apply, Function.iterate_succ', s.stays_near a,
  Function.comp]
Proof state after:
no goals
Theorem: Super.potential_eqn
Proof 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✝
a : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ s.potential c (f c z) = s.potential c z ^ d
Tactic:
have a' : ∀ n, (c, (f c)^[n] (f c z)) ∉ s.near := by
  contrapose a; simp only [not_forall, not_not, ← Function.iterate_succ_apply] at a ⊢
  rcases a with ⟨n, a⟩; exact ⟨n + 1, a⟩
Proof 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✝
a : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
a' : ∀ (n : ℕ), (c, (f c)^[n] (f c z)) ∉ s.near
⊢ s.potential c (f c z) = s.potential c z ^ d
Theorem: Super.potential_eqn
Proof 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✝
a : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
a' : ∀ (n : ℕ), (c, (f c)^[n] (f c z)) ∉ s.near
⊢ s.potential c (f c z) = s.potential c z ^ d
Tactic:
simp only [s.potential_eq_one (not_exists.mp a), s.potential_eq_one a', one_pow]
Proof state after:
no goals