OAI/Probability/SLE/Gauge/RibbonRouteLifting.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Physical perturbations of a transverse ribbon route admit continuous coordinate lifts. The fixed inverse Lipschitz bound then turns a physical tube event into a forced hit of the actual stopped past.

  1. theorem OAI.SLEExactGauge.RibbonCoordinates.inverse_coordinate_lipschitz line 17
  2. theorem OAI.SLEExactGauge.RibbonCoordinates.physical_tube_has_coordinate_lift line 28

    Source documentation

    Invariance of domain supplies a physical tube; the patch inverse is continuous with exactly the given inverse Lipschitz bound.

    theorem physical_tube_has_coordinate_lift
    (hpublished : PublishedPlanarDiskOpenness)
    (P : ℂ → ℂ) (S : Set ℂ) (hP : ContinuousOn P S) (hi : InjOn P S)
    (K : ℝ≥0) (hK : 0 < (K : ℝ))
    (hlower : ∀ u ∈ S, ∀ v ∈ S, dist u v ≤ K * dist (P u) (P v))
    (ξ ζ : ℝ → ℂ) (I : Set ℝ) {r : ℝ} (hr : 0 < r)
    (hξ : ∀ t ∈ I, closedBall (ξ t) r ⊆ S)
    (hζ : ContinuousOn ζ I)
    (hnear : ∀ t ∈ I, dist (ζ t) (P (ξ t)) < r / K) :
    let q := invFunOn P S ∘ ζ
…

    Mentions: OAI.SLEExactGauge.PublishedPlanarDiskOpenness

  3. def OAI.SLEExactGauge.RibbonCoordinates.crossingPatch line 61
  4. theorem OAI.SLEExactGauge.RibbonCoordinates.crossingPatch_subset_closedRibbon line 64
  5. theorem OAI.SLEExactGauge.RibbonCoordinates.transverse_template_ball_subset_patch line 69
  6. theorem OAI.SLEExactGauge.RibbonCoordinates.physical_transverse_tube_hits_past line 87

    Source documentation

    A single physical tube radius, independent of the past, forces a hit. Every coordinate and continuity condition for the perturbed route is derived from the actual patch embedding rather than assumed.

    theorem physical_transverse_tube_hits_past
    (hpublished : PublishedPlanarDiskOpenness)
    (P : ℂ → ℂ) (hP : ContinuousOn P closedRibbon) (hi : InjOn P closedRibbon)
    (K : ℝ≥0) (hK : 0 < (K : ℝ)) {k ε T : ℝ}
    (hk : 1 ≤ k) (hε : 0 < ε) (hεsmall : ε ≤ 1 / 8) (hT : 0 < T)
    (hlower : ∀ u ∈ crossingPatch k, ∀ v ∈ crossingPatch k,
      dist u v ≤ K * dist (P u) (P v))
    (γ xp ζ : ℝ → ℂ) (hxp : ContinuousOn xp (Icc 0 T))
    (hγ : EqOn γ (P ∘ xp) (Icc 0 T))
    (hxp0 : (xp 0).re = 0) (hxpT : (xp T).re = k)
    (hcore : ∀ t ∈ Icc (0 : ℝ) T, |(xp t).im| ≤ ε)
    (hζ : ContinuousOn ζ (Icc 0 1))
…

    Mentions: OAI.SLEExactGauge.PublishedPlanarDiskOpenness, OAI.SLEExactGauge.RibbonCoordinates.closedRibbon, OAI.SLEExactGauge.RibbonCoordinates.crossingPatch