Theorem: UpperSemicontinuous.potential (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
⊢ UpperSemicontinuous (uncurry s.potential)
Tactic:
intro ⟨c, z⟩
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
⊢ UpperSemicontinuousAt (uncurry s.potential) (c, z)

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
⊢ UpperSemicontinuousAt (uncurry s.potential) (c, z)
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
c : ℂ
z : S
r : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ UpperSemicontinuousAt (uncurry 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
c : ℂ
z : S
r : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ UpperSemicontinuousAt (uncurry s.potential) (c, z)

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
r : ∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ UpperSemicontinuousAt (uncurry s.potential) (c, z)
Tactic:
exact (ContinuousAt.potential_of_reaches s r).upperSemicontinuousAt
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
r : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ UpperSemicontinuousAt (uncurry s.potential) (c, z)
Tactic:
simp only [uncurry, UpperSemicontinuousAt, s.potential_eq_one (not_exists.mp 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
c : ℂ
z : S
r : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ ∀ (y : ℝ), 1 < y → ∀ᶠ (x' : ℂ × S) in 𝓝 (c, z), s.potential x'.1 x'.2 < y

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
r : ¬∃ n, (c, (f c)^[n] z) ∈ s.near
⊢ ∀ (y : ℝ), 1 < y → ∀ᶠ (x' : ℂ × S) in 𝓝 (c, z), s.potential x'.1 x'.2 < y
Tactic:
exact fun y y1 ↦ eventually_of_forall fun p ↦ lt_of_le_of_lt s.potential_le_one y1
State after:
no goals