ActualRibbonStoppedMass.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The retained mass is present at successful completion and is observable at that stopping time. It supplies the adapted cover tests and the successful-completion change of measure.

lemma OAI.SLEExactGauge.untopD_le_of_le_finite line 16

theorem OAI.SLEExactGauge.actual_successes_force_stopped_mass line 27

Source documentation

All selected mass is measurable by the successful completion time; no later portion of the trace is used to create a dense candidate.

theorem actual_successes_force_stopped_mass
    {Ω : Type*} (γ : Ω → ℝ≥0 → ℂ) (hc : ∀ ω, Continuous (γ ω))
    (g : C(ℂ, ℝ)) (hg0 : ∀ ω, g (γ ω 0) = 0) (P : ℂ → ℂ)
    (hplanar : PublishedPlanarDiskOpenness) (hP : ContinuousOn P closedRibbon)
    (hi : InjOn P closedRibbon) (ε κ v c : ℝ) (hε : ε ≤ 1)
    (N : ℕ) (I : Finset ℕ) (hI : ∀ i ∈ I, 0 < i ∧ i ≤ N) (D : Set ℂ)
    (hregions : ∀ i ∈ I, physicalMiddleRegion P closedRibbon i ε ⊆ D)
    (ω : Ω) (hω : ω ∈ GoodRibbonPrefix γ (ribbonIntegerFront g γ 0) P ε ∩
      ⋂ n ∈ Finset.range N, actualRibbonSuccess γ g P ε κ v c n) :
    ω ∈ GoodRibbonPrefix γ (ribbonIntegerFront g γ N) P ε ∧
      (I.card : ℝ≥0∞) * ENNReal.ofReal c ≤ segmentSausageCharge κ (γ ω) 0
        ((ribbonIntegerFront g γ N ω).untopD 0) v D := by
…

Mentions: OAI.SLEExactGauge.PublishedPlanarDiskOpenness, OAI.SLEExactGauge.GoodRibbonPrefix, OAI.SLEExactGauge.ribbonIntegerFront, OAI.SLEExactGauge.actualRibbonSuccess, OAI.SLEExactGauge.segmentSausageCharge