GuideLimitIdentification.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Identification of parameter-guide limits. Compact containment and injectivity give a uniform inverse modulus for the limiting conformal map, so the whole sequence converges once the physical guides do.

theorem OAI.SLEExactGauge.GuideLimitIdentification.compact_inverse_modulus line 20

Source documentation

An injective continuous map on a compact set has a uniform inverse modulus, stated directly in the ambient complex plane.

theorem compact_inverse_modulus
    {F : ℂ → ℂ} {Q : Set ℂ} (hQ : IsCompact Q)
    (hF : ContinuousOn F Q) (hi : InjOn F Q) :
    ∀ ε : ℝ, 0 < ε → ∃ η : ℝ, 0 < η ∧
      ∀ x ∈ Q, ∀ y ∈ Q, dist (F x) (F y) < η → dist x y < ε := by
…

theorem OAI.SLEExactGauge.GuideLimitIdentification.limiting_map_composition_tendsto line 56

Source documentation

Uniform convergence of the physical curves and of the conformal maps on the common compact set gives uniform convergence after applying the limiting map to the parameter curves.

theorem limiting_map_composition_tendsto
    (Fₙ : ℕ → ℂ → ℂ) (F : ℂ → ℂ) (βₙ αₙ : ℕ → ℝ → ℂ) (α : ℝ → ℂ)
    {Q : Set ℂ} {I : Set ℝ}
    (hF : TendstoUniformlyOn Fₙ F atTop Q)
    (hα : TendstoUniformlyOn αₙ α atTop I)
    (hQ : ∀ n, MapsTo (βₙ n) I Q)
    (hrelation : ∀ n t, t ∈ I → Fₙ n (βₙ n t) = αₙ n t) :
    TendstoUniformlyOn (fun n t => F (βₙ n t)) α atTop I := by
…

theorem OAI.SLEExactGauge.GuideLimitIdentification.exists_unique_uniform_guide_limit line 80

Source documentation

The unique inverse guide is the uniform limit on a fixed interval. The compact set can be supplied by inverse_guide_family_compactness.

theorem exists_unique_uniform_guide_limit
    (Fₙ : ℕ → ℂ → ℂ) (F : ℂ → ℂ) (βₙ αₙ : ℕ → ℝ → ℂ) (α : ℝ → ℂ)
    {Q : Set ℂ} {I : Set ℝ} (hQ : IsCompact Q)
    (hFcont : ContinuousOn F Q) (hi : InjOn F Q)
    (hF : TendstoUniformlyOn Fₙ F atTop Q)
    (hα : TendstoUniformlyOn αₙ α atTop I)
    (hβQ : ∀ n, MapsTo (βₙ n) I Q)
    (hβcont : ∀ n, ContinuousOn (βₙ n) I)
    (hrelation : ∀ n t, t ∈ I → Fₙ n (βₙ n t) = αₙ n t) :
    ∃ β : ℝ → ℂ, MapsTo β I Q ∧ EqOn (F ∘ β) α I ∧ ContinuousOn β I ∧
      TendstoUniformlyOn βₙ β atTop I ∧
      ∀ β' : ℝ → ℂ, MapsTo β' I Q → EqOn (F ∘ β') α I → EqOn β' β I := by
…

theorem OAI.SLEExactGauge.GuideLimitIdentification.inverse_guide_injective line 124
theorem OAI.SLEExactGauge.GuideLimitIdentification.inverse_guide_injective_with_tip line 134
Source documentation
The upper-half-plane condition separates every positive-time point from the starting point; injectivity of the physical guide separates the rest.
```
theorem inverse_guide_injective_with_tip
    {β α : ℝ → ℂ} {F : ℂ → ℂ} {T : ℝ}
    (hzero : β 0 = 0) (hH : MapsTo β (Ioc 0 T) upperHalfPlane)
    (hrelation : EqOn (F ∘ β) α (Ioc 0 T)) (hα : InjOn α (Ioc 0 T)) :
    InjOn β (Icc 0 T) := by
…
```
Mentions: OAI.SLEExactGauge.upperHalfPlane

theorem OAI.SLEExactGauge.GuideLimitIdentification.normalized_guide_limit line 159

Source documentation

The fixed-interval inverse limit supplied by the actual normalized hyperbolic-speed estimates.

theorem normalized_guide_limit
    (Fₙ : ℕ → ℂ → ℂ) (F : ℂ → ℂ) (βₙ αₙ : ℕ → ℝ → ℂ) (α : ℝ → ℂ)
    {δ T tw K s : ℝ} (hK : 0 ≤ K) (hs : 0 < s) (htw : tw ∈ Icc δ T)
    (hD : ∀ n t, t ∈ Icc δ T → DifferentiableAt ℝ (βₙ n) t)
    (hH : ∀ n t, t ∈ Icc δ T → 0 < (βₙ n t).im)
    (hv : ∀ n t, t ∈ Icc δ T → ‖deriv (βₙ n) t‖ ≤ K * (βₙ n t).im)
    (hway : ∀ n, ‖βₙ n tw‖ = 1) (hangle : ∀ n, s ≤ (βₙ n tw).im)
    (hFcont : ContinuousOn F upperHalfPlane) (hi : InjOn F upperHalfPlane)
    (hF : TendstoLocallyUniformlyOn Fₙ F atTop upperHalfPlane)
    (hα : TendstoUniformlyOn αₙ α atTop (Icc δ T))
    (hrelation : ∀ n t, t ∈ Icc δ T → Fₙ n (βₙ n t) = αₙ n t) :
    ∃ β : ℝ → ℂ, MapsTo β (Icc δ T) upperHalfPlane ∧
…

Mentions: OAI.SLEExactGauge.upperHalfPlane

theorem OAI.SLEExactGauge.GuideLimitIdentification.uniform_limit_of_away_and_common_tip_modulus line 185

Source documentation

A common tip modulus upgrades uniform convergence away from the tip to uniform convergence on the closed time interval, including continuity at zero.

theorem uniform_limit_of_away_and_common_tip_modulus
    (βₙ : ℕ → ℝ → ℂ) (β : ℝ → ℂ) {T : ℝ}
    (hcont : ∀ n, ContinuousOn (βₙ n) (Icc 0 T)) (hzero : β 0 = 0)
    (haway : ∀ δ : ℝ, 0 < δ → δ ≤ T →
      TendstoUniformlyOn βₙ β atTop (Icc δ T))
    (htip : ∀ ε : ℝ, 0 < ε → ∃ h : ℝ, 0 < h ∧ h ≤ T ∧
      ∀ n t, t ∈ Icc 0 h → ‖βₙ n t‖ < ε) :
    TendstoUniformlyOn βₙ β atTop (Icc 0 T) ∧ ContinuousOn β (Icc 0 T) := by
…

theorem OAI.SLEExactGauge.GuideLimitIdentification.exists_continuous_guide_limit line 218

Source documentation

Compatible inverse limits on all positive compact time intervals give one continuous guide starting at zero. The compact sets are the actual confinement sets proved by HyperbolicGuideCompactness.

theorem exists_continuous_guide_limit
    (Fₙ : ℕ → ℂ → ℂ) (F : ℂ → ℂ) (βₙ αₙ : ℕ → ℝ → ℂ) (α : ℝ → ℂ)
    {T : ℝ}
    (hFcont : ContinuousOn F upperHalfPlane) (hi : InjOn F upperHalfPlane)
    (hF : TendstoLocallyUniformlyOn Fₙ F atTop upperHalfPlane)
    (hα : TendstoUniformlyOn αₙ α atTop (Icc 0 T))
    (hcont : ∀ n, ContinuousOn (βₙ n) (Icc 0 T))
    (hcompact : ∀ δ : ℝ, 0 < δ → δ ≤ T →
      ∃ Q : Set ℂ, IsCompact Q ∧ Q ⊆ upperHalfPlane ∧
        ∀ n, MapsTo (βₙ n) (Icc δ T) Q)
    (hrelation : ∀ n t, t ∈ Ioc 0 T → Fₙ n (βₙ n t) = αₙ n t)
    (htip : ∀ ε : ℝ, 0 < ε → ∃ h : ℝ, 0 < h ∧ h ≤ T ∧
…

Mentions: OAI.SLEExactGauge.upperHalfPlane