ConditionalRibbonStep.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The actual uniform ribbon step integrates against the measurable stopped restart law. The estimate holds on every event in the past where an actual admissible ribbon history has been certified.

lemma OAI.SLEExactGauge.ribbon_section_restart_lower_bound line 22

theorem OAI.SLEExactGauge.uniform_conditional_actual_ribbon_step line 66

Source documentation

The genuine Brownian restart and the actual uniform passage estimate give the adapted lower bound needed by concatenation. Histories are required only on the event where the preceding steps succeeded.

theorem uniform_conditional_actual_ribbon_step
    {Ω : Type} [mΩ : MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (B : ℝ≥0 → Ω → ℝ) (hB : IsBrownianReal B P)
    (hm : ∀ t, Measurable (B t)) (hc : ∀ ω, 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