OAI/Probability/SLE/Geometry/WaypointRouteProbability.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SLEExactGauge.RibbonCoordinates.basedPhysicalWaypointRoute line 16
2. theorem OAI.SLEExactGauge.RibbonCoordinates.basedPhysicalWaypointRoute_zero line 23
3. theorem OAI.SLEExactGauge.RibbonCoordinates.basedPhysicalWaypointRoute_lipschitz line 30
4. def OAI.SLEExactGauge.RibbonCoordinates.unitClipPoint line 53
5. theorem OAI.SLEExactGauge.RibbonCoordinates.continuous_unitClipPoint line 56
6. def OAI.SLEExactGauge.RibbonCoordinates.physicalUnitBrownianPath line 59
7. theorem OAI.SLEExactGauge.RibbonCoordinates.physicalUnitBrownianPath_continuous line 62
8. theorem OAI.SLEExactGauge.RibbonCoordinates.uniform_physical_waypoint_tube_probability line 69

   Source documentation

   Pointwise Brownian support gives a single positive probability for every physical route with the fixed patch speed bound.

   theorem uniform_physical_waypoint_tube_probability
       (hpublished : PublishedPlanarWienerUnitSupport)
       (W : WienerLaw) (hW : IsWiener W) (C : ℝ≥0) {ε : ℝ} (hε : 0 < ε) :
       ∃ q : ℝ≥0∞, 0 < q ∧ ∀ P : ℂ → ℂ, ∀ k side : ℝ, |side| = 1 →
         LipschitzOnWith C P (crossingPatch k) → q ≤ (W.prod W) {b |
           ∀ t ∈ Icc (0 : ℝ) 3,
             dist (physicalUnitBrownianPath (P ((k + 1 / 2 : ℝ) : ℂ)) b t)
               (P (waypointRoute k side t)) < ε} := by
   …

   Mentions: OAI.SLEExactGauge.PublishedPlanarWienerUnitSupport, OAI.SLEExactGauge.RibbonCoordinates.crossingPatch, OAI.SLEExactGauge.RibbonCoordinates.physicalUnitBrownianPath, OAI.SLEExactGauge.RibbonCoordinates.waypointRoute

9. theorem OAI.SLEExactGauge.RibbonCoordinates.physical_waypoint_tube_hits_past line 100

   Source documentation

   Either orientation of the final physical leg forces a hit of the actual stopped past.

   theorem physical_waypoint_tube_hits_past
       (hpublished : PublishedPlanarDiskOpenness)
       (P : ℂ → ℂ) (hP : ContinuousOn P closedRibbon) (hi : InjOn P closedRibbon)
       (K : ℝ≥0) (hK : 0 < (K : ℝ)) {k ε T side : ℝ}
       (hk : 1 ≤ k) (hε : 0 < ε) (hεsmall : ε ≤ 1 / 8) (hT : 0 < T)
       (hside : side = -1 ∨ side = 1)
       (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| ≤ ε)
   …

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