OAI/Probability/SLE/Gauge/RibbonCoordinateCompactness.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Common physical domains and convergence of inverse ribbon coordinates on a fixed compact coordinate patch. The uniform lower Lipschitz bound controls the inverse without requiring derivative convergence.

  1. def OAI.SLEExactGauge.RibbonCoordinates.coordinateInverse line 16
  2. theorem OAI.SLEExactGauge.RibbonCoordinates.coordinateInverse_mem line 18
  3. theorem OAI.SLEExactGauge.RibbonCoordinates.coordinateInverse_right line 22
  4. theorem OAI.SLEExactGauge.RibbonCoordinates.coordinateInverse_left line 26
  5. theorem OAI.SLEExactGauge.RibbonCoordinates.coordinate_image_region_iff line 32

    Source documentation

    Physical coordinate regions agree with inverse-coordinate membership.

    theorem coordinate_image_region_iff {P : ℂ → ℂ} {K A : Set ℂ}
    (hi : InjOn P K) (hA : A ⊆ K) {z : ℂ} :
    z ∈ P '' A ↔ z ∈ P '' K ∧ coordinateInverse P K z ∈ A := by
…

    Mentions: OAI.SLEExactGauge.RibbonCoordinates.coordinateInverse

  6. theorem OAI.SLEExactGauge.RibbonCoordinates.coordinateInverse_lipschitz line 41
  7. theorem OAI.SLEExactGauge.RibbonCoordinates.lower_lipschitz_uniform_limit line 50
  8. theorem OAI.SLEExactGauge.RibbonCoordinates.coordinateInverse_uniform_on line 61

    Source documentation

    Common image containment converts uniform forward convergence into uniform inverse convergence on any retained physical set.

    theorem coordinateInverse_uniform_on
    (Pₙ : ℕ → ℂ → ℂ) (P : ℂ → ℂ) (K S : Set ℂ) (L : ℝ≥0)
    (hconv : TendstoUniformlyOn Pₙ P atTop K)
    (hlower : ∀ n x, x ∈ K → ∀ y, y ∈ K → dist x y ≤ L * dist (Pₙ n x) (Pₙ n y))
    (hSP : S ⊆ P '' K) (hcover : ∀ᶠ n in atTop, S ⊆ Pₙ n '' K) :
    TendstoUniformlyOn (fun n => coordinateInverse (Pₙ n) K) (coordinateInverse P K) atTop S := by
…

    Mentions: OAI.SLEExactGauge.RibbonCoordinates.coordinateInverse

  9. theorem OAI.SLEExactGauge.RibbonCoordinates.lower_lipschitz_injOn line 90

    Source documentation

    The uniform inverse bound makes every coordinate chart injective.

    theorem lower_lipschitz_injOn
    (P : ℂ → ℂ) (K : Set ℂ) (L : ℝ≥0)
    (hlower : ∀ x ∈ K, ∀ y ∈ K, dist x y ≤ L * dist (P x) (P y)) :
    InjOn P K := by
…
  10. theorem OAI.SLEExactGauge.RibbonCoordinates.isOpen_image_interior line 100

    Source documentation

    The limiting coordinate image has an open interior physical domain.

    theorem isOpen_image_interior
    (hpublished : PublishedPlanarDiskOpenness)
    (P : ℂ → ℂ) (K : Set ℂ)
    (hP : ContinuousOn P K) (hi : InjOn P K) :
    IsOpen (P '' interior K) := by
…

    Mentions: OAI.SLEExactGauge.PublishedPlanarDiskOpenness

  11. theorem OAI.SLEExactGauge.RibbonCoordinates.eventual_compact_image_interior line 116

    Source documentation

    Compact physical subsets of the limiting interior image belong to all sufficiently late moving interior images.

    theorem eventual_compact_image_interior
    (hpublished : PublishedPlanarDiskOpenness)
    (Pₙ : ℕ → ℂ → ℂ) (P : ℂ → ℂ) (K S : Set ℂ) (L : ℝ≥0)
    (hL : 0 < L)
    (hPn : ∀ n, ContinuousOn (Pₙ n) K)
    (hconv : TendstoUniformlyOn Pₙ P atTop K)
    (hlower : ∀ n x, x ∈ K → ∀ y, y ∈ K → dist x y ≤ L * dist (Pₙ n x) (Pₙ n y))
    (hS : IsCompact S) (hSP : S ⊆ P '' interior K) :
    ∀ᶠ n in atTop, S ⊆ Pₙ n '' interior K := by
…

    Mentions: OAI.SLEExactGauge.PublishedPlanarDiskOpenness

  12. theorem OAI.SLEExactGauge.RibbonCoordinates.coordinateInverse_locally_uniform line 164

    Source documentation

    The inverse ribbon charts converge locally uniformly on the full limiting interior image. Only compact subsets are eventually common.

    theorem coordinateInverse_locally_uniform
    (hpublished : PublishedPlanarDiskOpenness)
    (Pₙ : ℕ → ℂ → ℂ) (P : ℂ → ℂ) (K : Set ℂ) (L : ℝ≥0)
    (hL : 0 < L) (hP : ContinuousOn P K)
    (hPn : ∀ n, ContinuousOn (Pₙ n) K)
    (hconv : TendstoUniformlyOn Pₙ P atTop K)
    (hlower : ∀ n x, x ∈ K → ∀ y, y ∈ K → dist x y ≤ L * dist (Pₙ n x) (Pₙ n y)) :
    TendstoLocallyUniformlyOn (fun n => coordinateInverse (Pₙ n) K)
      (coordinateInverse P K) atTop (P '' interior K) := by
…

    Mentions: OAI.SLEExactGauge.PublishedPlanarDiskOpenness, OAI.SLEExactGauge.RibbonCoordinates.coordinateInverse

  13. theorem OAI.SLEExactGauge.RibbonCoordinates.common_physical_neighborhood line 185

    Source documentation

    A compact retained physical patch admits one common open neighborhood contained in every sufficiently late coordinate image.

    theorem common_physical_neighborhood
    (hpublished : PublishedPlanarDiskOpenness)
    (Pₙ : ℕ → ℂ → ℂ) (P : ℂ → ℂ) (K A : Set ℂ) (L : ℝ≥0)
    (hL : 0 < L) (hP : ContinuousOn P K)
    (hPn : ∀ n, ContinuousOn (Pₙ n) K)
    (hconv : TendstoUniformlyOn Pₙ P atTop K)
    (hlower : ∀ n x, x ∈ K → ∀ y, y ∈ K → dist x y ≤ L * dist (Pₙ n x) (Pₙ n y))
    (hA : IsCompact A) (hAP : A ⊆ P '' interior K) :
    ∃ U : Set ℂ, IsOpen U ∧ A ⊆ U ∧ IsCompact (closure U) ∧
      closure U ⊆ P '' interior K ∧
      (∀ᶠ n in atTop, closure U ⊆ Pₙ n '' interior K) ∧
      TendstoUniformlyOn (fun n => coordinateInverse (Pₙ n) K)
…

    Mentions: OAI.SLEExactGauge.PublishedPlanarDiskOpenness, OAI.SLEExactGauge.RibbonCoordinates.coordinateInverse

  14. def OAI.SLEExactGauge.RibbonCoordinates.longitudinalCoordinate line 215

    Source documentation

    The source longitudinal coordinate is the real part of the inverse ribbon chart, translated by the current front coordinate.

    def longitudinalCoordinate (P : ℂ → ℂ) (K : Set ℂ) (k : ℝ) (z : ℂ) : ℝ :=
…
  15. theorem OAI.SLEExactGauge.RibbonCoordinates.longitudinalCoordinate_locally_uniform line 218
  16. theorem OAI.SLEExactGauge.RibbonCoordinates.longitudinalCoordinate_continuousOn line 232
  17. theorem OAI.SLEExactGauge.RibbonCoordinates.common_longitudinal_chart line 242

    Source documentation

    A retained compact part of a ribbon has a common open physical chart on which the actual longitudinal coordinates are eventually continuous and converge locally uniformly.

    theorem common_longitudinal_chart
    (hpublished : PublishedPlanarDiskOpenness)
    (Pₙ : ℕ → ℂ → ℂ) (P : ℂ → ℂ) (K A : Set ℂ) (L : ℝ≥0) (k : ℝ)
    (hL : 0 < L) (hP : ContinuousOn P K)
    (hPn : ∀ n, ContinuousOn (Pₙ n) K)
    (hconv : TendstoUniformlyOn Pₙ P atTop K)
    (hlower : ∀ n x, x ∈ K → ∀ y, y ∈ K → dist x y ≤ L * dist (Pₙ n x) (Pₙ n y))
    (hA : IsCompact A) (hAP : A ⊆ P '' interior K) :
    ∃ U : Set ℂ, IsOpen U ∧ A ⊆ U ∧ IsCompact (closure U) ∧
      closure U ⊆ P '' interior K ∧
      (∀ᶠ n in atTop, U ⊆ Pₙ n '' interior K) ∧
      ContinuousOn (longitudinalCoordinate P K k) U ∧
…

    Mentions: OAI.SLEExactGauge.PublishedPlanarDiskOpenness, OAI.SLEExactGauge.RibbonCoordinates.longitudinalCoordinate

  18. theorem OAI.SLEExactGauge.RibbonCoordinates.eventual_compact_coordinate_region line 273

    Source documentation

    A compact set with limiting coordinates in an open coordinate region has its moving coordinates in that same region for all sufficiently late charts. This includes simultaneous longitudinal and transverse margins.

    theorem eventual_compact_coordinate_region
    (Pₙ : ℕ → ℂ → ℂ) (P : ℂ → ℂ) (K S A : Set ℂ) (L : ℝ≥0)
    (hconv : TendstoUniformlyOn Pₙ P atTop K)
    (hlower : ∀ n x, x ∈ K → ∀ y, y ∈ K → dist x y ≤ L * dist (Pₙ n x) (Pₙ n y))
    (hS : IsCompact S) (hSP : S ⊆ P '' K)
    (hcover : ∀ᶠ n in atTop, S ⊆ Pₙ n '' K)
    (hA : IsOpen A) (hSA : coordinateInverse P K '' S ⊆ A) :
    ∀ᶠ n in atTop, S ⊆ Pₙ n '' (K ∩ A) := by
…

    Mentions: OAI.SLEExactGauge.RibbonCoordinates.coordinateInverse

  19. theorem OAI.SLEExactGauge.RibbonCoordinates.exists_bilip_uniform_subsequence line 296

    Source documentation

    The admissible two-point patch bounds and a bounded marked point give an actual uniformly convergent subsequence of the coordinate maps. Both Lipschitz bounds pass to the limit, retaining an embedded limiting patch.

    theorem exists_bilip_uniform_subsequence
    (Pₙ : ℕ → ℂ → ℂ) (K : Set ℂ) (hK : IsCompact K)
    (x₀ : ℂ) (hx₀ : x₀ ∈ K) (C L : ℝ≥0) (R : ℝ)
    (hupper : ∀ n, LipschitzOnWith C (Pₙ n) K)
    (hlower : ∀ n x, x ∈ K → ∀ y, y ∈ K → dist x y ≤ L * dist (Pₙ n x) (Pₙ n y))
    (htip : ∀ n, ‖Pₙ n x₀‖ ≤ R) :
    ∃ P : ℂ → ℂ, ∃ φ : ℕ → ℕ, StrictMono φ ∧
      TendstoUniformlyOn (fun n => Pₙ (φ n)) P atTop K ∧
      LipschitzOnWith C P K ∧
      (∀ x ∈ K, ∀ y ∈ K, dist x y ≤ L * dist (P x) (P y)) ∧
      InjOn P K := by
…