ActualRibbonMass.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Charge selected actual successive-front windows to a single sausage, retaining the successful terminal prefix for clearance and density transfer.

lemma OAI.SLEExactGauge.actual_successes_terminal_prefix line 15

theorem OAI.SLEExactGauge.actual_successes_force_whole_mass line 28

Source documentation

Only selected middle strips are charged. The trace windows are the original actual fronts, including their exact starting and ending times.

theorem actual_successes_force_whole_mass
    {Ω : Type*} (γ : Ω → ℝ≥0 → ℂ) (g : C(ℂ, ℝ)) (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 ≤ wholeSausageCharge κ (γ ω) v D := by
…

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