OAI/Probability/SLE/Geometry/PhysicalRouteProbability.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A uniform positive tube probability for any fixed-speed physical route on the finite exit window. It is a consequence of the cited planar Wiener support input and compactness of based Lipschitz routes.

  1. def OAI.SLEExactGauge.RibbonCoordinates.basedPhysicalRoute line 16
  2. lemma OAI.SLEExactGauge.RibbonCoordinates.basedPhysicalRoute_zero line 20
  3. lemma OAI.SLEExactGauge.RibbonCoordinates.basedPhysicalRoute_lipschitz line 25
  4. theorem OAI.SLEExactGauge.RibbonCoordinates.uniform_physical_route_tube_probability line 40