internlm/Lean-Github huggingface dataset:
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✝
a : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ ∀ (n : ℕ), (c, (f c)^[n] (f c z)) ∉ s.near
Tactic:
contrapose a
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] (f c z)) ∉ s.near
⊢ ¬¬∃ n, (c, (f c)^[n] z) ∈ s.near
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✝
a : ¬∀ (n : ℕ), (c, (f c)^[n] (f c z)) ∉ s.near
⊢ ¬¬∃ n, (c, (f c)^[n] z) ∈ s.near
Tactic:
simp only [not_forall, not_not, ← Function.iterate_succ_apply] at a ⊢
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 : ∃ x, (c, (f c)^[x.succ] z) ∈ s.near
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.near
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✝
a : ∃ x, (c, (f c)^[x.succ] z) ∈ s.near
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.near
Tactic:
rcases a with ⟨n, a⟩
Proof state after:
case 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.succ] z) ∈ s.near
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.near
Theorem: Super.potential_eqn
Proof state before:
case 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.succ] z) ∈ s.near
⊢ ∃ n, (c, (f c)^[n] z) ∈ s.near
Tactic:
exact ⟨n + 1, a⟩
Proof state after:
no goals
Theorem: Super.potential_eqn_iter
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 : ℕ
⊢ s.potential c ((f c)^[n] z) = s.potential c z ^ d ^ n
Tactic:
induction' n with n h
Proof 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
⊢ s.potential c ((f c)^[0] z) = s.potential c z ^ d ^ 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
n : ℕ
h : s.potential c ((f c)^[n] z) = s.potential c z ^ d ^ n
⊢ s.potential c ((f c)^[n + 1] z) = s.potential c z ^ d ^ (n + 1)
Theorem: Super.potential_eqn_iter
Proof 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
⊢ s.potential c ((f c)^[0] z) = s.potential c z ^ d ^ 0
Tactic:
simp only [Function.iterate_zero, id, pow_zero, pow_one]
Proof state after:
no goals
Theorem: Super.potential_eqn_iter
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
n : ℕ
h : s.potential c ((f c)^[n] z) = s.potential c z ^ d ^ n
⊢ s.potential c ((f c)^[n + 1] z) = s.potential c z ^ d ^ (n + 1)
Tactic:
simp only [Function.iterate_succ', Super.potential_eqn, h, ← pow_mul, ← pow_succ,
  Function.comp]
Proof state after:
no goals
Theorem: Super.iter_holomorphic'
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 : ℕ
⊢ Holomorphic (I.prod I) I fun p => (f p.1)^[n] p.2
Tactic:
intro p
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 : ℕ
p : ℂ × S
⊢ HolomorphicAt (I.prod I) I (fun p => (f p.1)^[n] p.2) p
Theorem: Super.iter_holomorphic'
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 : ℕ
p : ℂ × S
⊢ HolomorphicAt (I.prod I) I (fun p => (f p.1)^[n] p.2) p
Tactic:
induction' n with n h
Proof 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
p : ℂ × S
⊢ HolomorphicAt (I.prod I) I (fun p => (f p.1)^[0] p.2) p

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
p : ℂ × S
n : ℕ
h : HolomorphicAt (I.prod I) I (fun p => (f p.1)^[n] p.2) p
⊢ HolomorphicAt (I.prod I) I (fun p => (f p.1)^[n + 1] p.2) p
Theorem: Super.iter_holomorphic'
Proof 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
p : ℂ × S
⊢ HolomorphicAt (I.prod I) I (fun p => (f p.1)^[0] p.2) p

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
p : ℂ × S
n : ℕ
h : HolomorphicAt (I.prod I) I (fun p => (f p.1)^[n] p.2) p
⊢ HolomorphicAt (I.prod I) I (fun p => (f p.1)^[n + 1] p.2) p
Tactic:
simp [Function.iterate_zero, holomorphicAt_snd]
Proof 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
p : ℂ × S
n : ℕ
h : HolomorphicAt (I.prod I) I (fun p => (f p.1)^[n] p.2) p
⊢ HolomorphicAt (I.prod I) I (fun p => (f p.1)^[n + 1] p.2) p
Theorem: Super.iter_holomorphic'
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
p : ℂ × S
n : ℕ
h : HolomorphicAt (I.prod I) I (fun p => (f p.1)^[n] p.2) p
⊢ HolomorphicAt (I.prod I) I (fun p => (f p.1)^[n + 1] p.2) p
Tactic:
simp only [Function.iterate_succ', Function.comp]
Proof 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
p : ℂ × S
n : ℕ
h : HolomorphicAt (I.prod I) I (fun p => (f p.1)^[n] p.2) p
⊢ HolomorphicAt (I.prod I) I (fun p => f p.1 ((f p.1)^[n] p.2)) p
Theorem: Super.iter_holomorphic'
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
p : ℂ × S
n : ℕ
h : HolomorphicAt (I.prod I) I (fun p => (f p.1)^[n] p.2) p
⊢ HolomorphicAt (I.prod I) I (fun p => f p.1 ((f p.1)^[n] p.2)) p
Tactic:
exact (s.fa _).comp₂ holomorphicAt_fst h
Proof state after:
no goals
Theorem: Super.iter_holomorphic
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 : ℕ
⊢ Holomorphic (I.prod I) (I.prod I) fun p => (p.1, (f p.1)^[n] p.2)
Tactic:
intro p
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 : ℕ
p : ℂ × S
⊢ HolomorphicAt (I.prod I) (I.prod I) (fun p => (p.1, (f p.1)^[n] p.2)) p
Theorem: Super.iter_holomorphic
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 : ℕ
p : ℂ × S
⊢ HolomorphicAt (I.prod I) (I.prod I) (fun p => (p.1, (f p.1)^[n] p.2)) p
Tactic:
apply holomorphicAt_fst.prod
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 : ℕ
p : ℂ × S
⊢ HolomorphicAt (I.prod I) I (fun x => (f x.1)^[n] x.2) p
Theorem: Super.iter_holomorphic
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 : ℕ
p : ℂ × S
⊢ HolomorphicAt (I.prod I) I (fun x => (f x.1)^[n] x.2) p
Tactic:
apply s.iter_holomorphic'
Proof state after:
no goals
Theorem: ContinuousAt.potential_of_reaches
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
⊢ ContinuousAt (uncurry s.potential) (c, z)
Tactic:
rcases a with ⟨n, a⟩
Proof state after:
case 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
⊢ ContinuousAt (uncurry s.potential) (c, z)
Theorem: ContinuousAt.potential_of_reaches
Proof state before:
case 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
⊢ ContinuousAt (uncurry s.potential) (c, z)
Tactic:
have e : uncurry s.potential =ᶠ[𝓝 (c, z)] fun p : ℂ × S ↦ s.potential' p.1 p.2 n := by
  have a' : ∀ᶠ p : ℂ × S in 𝓝 (c, z), (p.1, (f p.1)^[n] p.2) ∈ s.near :=
    (s.iter_holomorphic n _).continuousAt.eventually_mem (s.isOpen_near.mem_nhds a)
  refine a'.mp (eventually_of_forall fun p h ↦ ?_)
  simp only [uncurry, s.potential_eq h]
Proof state after:
case 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
e : (𝓝 (c, z)).EventuallyEq (uncurry s.potential) fun p => s.potential' p.1 p.2 n
⊢ ContinuousAt (uncurry s.potential) (c, z)
Theorem: ContinuousAt.potential_of_reaches
Proof state before:
case 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
e : (𝓝 (c, z)).EventuallyEq (uncurry s.potential) fun p => s.potential' p.1 p.2 n
⊢ ContinuousAt (uncurry s.potential) (c, z)
Tactic:
simp only [continuousAt_congr e, Super.potential']
Proof state after:
case 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
e : (𝓝 (c, z)).EventuallyEq (uncurry s.potential) fun p => s.potential' p.1 p.2 n
⊢ ContinuousAt (fun p => Complex.abs (s.bottcherNear p.1 ((f p.1)^[n] p.2)) ^ (↑d ^ n)⁻¹) (c, z)
Theorem: ContinuousAt.potential_of_reaches
Proof state before:
case 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
e : (𝓝 (c, z)).EventuallyEq (uncurry s.potential) fun p => s.potential' p.1 p.2 n
⊢ ContinuousAt (fun p => Complex.abs (s.bottcherNear p.1 ((f p.1)^[n] p.2)) ^ (↑d ^ n)⁻¹) (c, z)
Tactic:
refine ContinuousAt.rpow ?_ continuousAt_const ?_
Proof state after:
case intro.refine_1
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
e : (𝓝 (c, z)).EventuallyEq (uncurry s.potential) fun p => s.potential' p.1 p.2 n
⊢ ContinuousAt (fun p => Complex.abs (s.bottcherNear p.1 ((f p.1)^[n] p.2))) (c, z)

case intro.refine_2
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
e : (𝓝 (c, z)).EventuallyEq (uncurry s.potential) fun p => s.potential' p.1 p.2 n
⊢ Complex.abs (s.bottcherNear (c, z).1 ((f (c, z).1)^[n] (c, z).2)) ≠ 0 ∨ 0 < (↑d ^ n)⁻¹
Theorem: ContinuousAt.potential_of_reaches
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, z)).EventuallyEq (uncurry s.potential) fun p => s.potential' p.1 p.2 n
Tactic:
have a' : ∀ᶠ p : ℂ × S in 𝓝 (c, z), (p.1, (f p.1)^[n] p.2) ∈ s.near :=
  (s.iter_holomorphic n _).continuousAt.eventually_mem (s.isOpen_near.mem_nhds a)
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 : ℕ
a : (c, (f c)^[n] z) ∈ s.near
a' : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), (p.1, (f p.1)^[n] p.2) ∈ s.near
⊢ (𝓝 (c, z)).EventuallyEq (uncurry s.potential) fun p => s.potential' p.1 p.2 n
Theorem: ContinuousAt.potential_of_reaches
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
a' : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), (p.1, (f p.1)^[n] p.2) ∈ s.near
⊢ (𝓝 (c, z)).EventuallyEq (uncurry s.potential) fun p => s.potential' p.1 p.2 n
Tactic:
refine a'.mp (eventually_of_forall fun p 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✝
n : ℕ
a : (c, (f c)^[n] z) ∈ s.near
a' : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), (p.1, (f p.1)^[n] p.2) ∈ s.near
p : ℂ × S
h : (p.1, (f p.1)^[n] p.2) ∈ s.near
⊢ uncurry s.potential p = (fun p => s.potential' p.1 p.2 n) p
Theorem: ContinuousAt.potential_of_reaches
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
a' : ∀ᶠ (p : ℂ × S) in 𝓝 (c, z), (p.1, (f p.1)^[n] p.2) ∈ s.near
p : ℂ × S
h : (p.1, (f p.1)^[n] p.2) ∈ s.near
⊢ uncurry s.potential p = (fun p => s.potential' p.1 p.2 n) p
Tactic:
simp only [uncurry, s.potential_eq h]
Proof state after:
no goals
Theorem: ContinuousAt.potential_of_reaches
Proof state before:
case intro.refine_1
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
e : (𝓝 (c, z)).EventuallyEq (uncurry s.potential) fun p => s.potential' p.1 p.2 n
⊢ ContinuousAt (fun p => Complex.abs (s.bottcherNear p.1 ((f p.1)^[n] p.2))) (c, z)
Tactic:
apply Complex.continuous_abs.continuousAt.comp
Proof state after:
case intro.refine_1
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
e : (𝓝 (c, z)).EventuallyEq (uncurry s.potential) fun p => s.potential' p.1 p.2 n
⊢ ContinuousAt (fun p => s.bottcherNear p.1 ((f p.1)^[n] p.2)) (c, z)
Theorem: ContinuousAt.potential_of_reaches
Proof state before:
case intro.refine_1
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
e : (𝓝 (c, z)).EventuallyEq (uncurry s.potential) fun p => s.potential' p.1 p.2 n
⊢ ContinuousAt (fun p => s.bottcherNear p.1 ((f p.1)^[n] p.2)) (c, z)
Tactic:
refine ((s.bottcherNear_holomorphic _ ?_).comp (s.iter_holomorphic n (c, z))).continuousAt
Proof state after:
case intro.refine_1
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
e : (𝓝 (c, z)).EventuallyEq (uncurry s.potential) fun p => s.potential' p.1 p.2 n
⊢ ((c, z).1, (f (c, z).1)^[n] (c, z).2) ∈ s.near
Theorem: ContinuousAt.potential_of_reaches
Proof state before:
case intro.refine_1
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
e : (𝓝 (c, z)).EventuallyEq (uncurry s.potential) fun p => s.potential' p.1 p.2 n
⊢ ((c, z).1, (f (c, z).1)^[n] (c, z).2) ∈ s.near
Tactic:
exact a
Proof state after:
no goals
Theorem: ContinuousAt.potential_of_reaches
Proof state before:
case intro.refine_2
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
e : (𝓝 (c, z)).EventuallyEq (uncurry s.potential) fun p => s.potential' p.1 p.2 n
⊢ Complex.abs (s.bottcherNear (c, z).1 ((f (c, z).1)^[n] (c, z).2)) ≠ 0 ∨ 0 < (↑d ^ n)⁻¹
Tactic:
right
Proof state after:
case intro.refine_2.h
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
e : (𝓝 (c, z)).EventuallyEq (uncurry s.potential) fun p => s.potential' p.1 p.2 n
⊢ 0 < (↑d ^ n)⁻¹
Theorem: ContinuousAt.potential_of_reaches
Proof state before:
case intro.refine_2.h
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
e : (𝓝 (c, z)).EventuallyEq (uncurry s.potential) fun p => s.potential' p.1 p.2 n
⊢ 0 < (↑d ^ n)⁻¹
Tactic:
bound
Proof state after:
no goals
Theorem: Super.potential_eq_zero
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 = 0 ↔ ∃ n, (f c)^[n] z = a
Tactic:
constructor
Proof 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
Theorem: Super.potential_eq_zero
Proof 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
Proof 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
Theorem: Super.potential_eq_zero
Proof 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
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
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
Theorem: Super.potential_eq_zero
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
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⟩
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
h : s.potential c z = 0
n : ℕ
r : (c, (f c)^[n] z) ∈ s.near
⊢ ∃ n, (f c)^[n] z = a
Theorem: Super.potential_eq_zero
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
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
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
h : (f c)^[n] z = a ∧ (↑d ^ n)⁻¹ ≠ 0
⊢ ∃ n, (f c)^[n] z = a
Theorem: Super.potential_eq_zero
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
h : (f c)^[n] z = a ∧ (↑d ^ n)⁻¹ ≠ 0
⊢ ∃ n, (f c)^[n] z = a
Tactic:
use n, h.1
Proof state after:
no goals