OAI/Probability/SLE/Gauge/UniformRibbonStep.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Uniform one-step probability in the original physical ribbon, for any actual continuous boundary realization of the stopped inverse map.

  1. def OAI.SLEExactGauge.translateFiniteBoundary line 18
  2. lemma OAI.SLEExactGauge.finiteBoundaryPath_translate line 21
  3. def OAI.SLEExactGauge.RibbonHistory.stepEvent line 28
  4. lemma OAI.SLEExactGauge.RibbonHistory.finiteBoundary_step_probability line 35
  5. lemma OAI.SLEExactGauge.RibbonHistory.step_lower line 57
  6. lemma OAI.SLEExactGauge.RibbonHistory.stepChart_continuousOn line 64
  7. lemma OAI.SLEExactGauge.RibbonHistory.global_progress_eq_step line 68
  8. lemma OAI.SLEExactGauge.RibbonHistory.stepEvent_measurable line 80
  9. theorem OAI.SLEExactGauge.uniform_actual_ribbon_step line 106

    Source documentation

    This is the uniform one-step estimate for an actual stopped history. The boundary chart can be the already past-measurable chart used in its restart law; no measurable selection of compactness outputs is required.

    theorem uniform_actual_ribbon_step
    {Ω : Type} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (B : ℝ≥0 → Ω → ℝ) (hB : IsBrownianReal B P)
    (hm : ∀ t, Measurable (B t)) (hcont : ∀ ω, Continuous (fun t => B t ω))
    (γ : Ω → ℝ≥0 → ℂ) (G F : Ω → ℝ≥0 → ℂ → ℂ)
    (hw : ∀ ω, IsCapacityTwoWitness (fun t => Real.sqrt κ * B t ω)
      (γ ω) (G ω) (F ω))
    (hcompact : PublishedHalfPlaneUnivalentCompactness)
    (hboundary : PublishedFiniteLoewnerBoundaryExtension)
    (hsupport : PublishedGeometricTubeSupport P γ)
    (hplanar : PublishedPlanarDiskOpenness)
…

    Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.PublishedHalfPlaneUnivalentCompactness, OAI.SLEExactGauge.PublishedFiniteLoewnerBoundaryExtension, OAI.SLEExactGauge.PublishedGeometricTubeSupport, OAI.SLEExactGauge.PublishedPlanarDiskOpenness