RibbonStepSuccess.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Actual passage-and-mass successes are measured in the next global front past, with the earlier global front as the mass window's start.

def OAI.SLEExactGauge.RibbonStepSuccess line 18
lemma OAI.SLEExactGauge.stoppedAtPath_eq_on_prefix line 23
lemma OAI.SLEExactGauge.segmentSausageCharge_shift line 30

theorem OAI.SLEExactGauge.ribbonStepSuccess_measurable line 48

Source documentation

The whole actual step and its sausage lower bound are adapted to the next front. Both global front times may be infinite off success.

theorem ribbonStepSuccess_measurable
    {Ω : Type*} [mΩ : MeasurableSpace Ω] (ℱ : Filtration ℝ≥0 mΩ)
    (γ : Ω → ℝ≥0 → ℂ) (ha : Adapted ℱ (fun t ω => γ ω t))
    (hc : ∀ ω, Continuous (γ ω))
    (σ τ : Ω → WithTop ℝ≥0) (hσ : IsStoppingTime ℱ σ) (hτ : IsStoppingTime ℱ τ)
    (hστ : σ ≤ τ) (P : ℂ → ℂ)
    (he : Topology.IsClosedEmbedding (fun z : closedRibbon => P z))
    (ε κ v c : ℝ) (R : Set ℂ) :
    MeasurableSet[hτ.measurableSpace] (RibbonStepSuccess γ σ τ P ε κ v c R) := by
…

Mentions: OAI.SLEExactGauge.RibbonStepSuccess