Theorem: ContinuousAt.potential_of_reaches (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✝
a : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ ContinuousAt (uncurry s.potential) (c, z)
Tactic:
rcases a with ⟨n, a⟩
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)

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]
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)

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']
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)

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 ?_
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)⁻¹

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)
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

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 ↦ ?_)
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

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]
State after:
no goals

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
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)

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
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

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
State after:
no goals

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
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)⁻¹

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
State after:
no goals