RibbonStepTranslation.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The recentered passage uses precisely the original ribbon coordinate and original middle strip after translating back by the actual tip.

def OAI.SLEExactGauge.RibbonHistory.stepChart line 17
lemma OAI.SLEExactGauge.RibbonHistory.stepCompact_maps line 20
lemma OAI.SLEExactGauge.RibbonHistory.recenteredChart_injOn line 27
lemma OAI.SLEExactGauge.RibbonHistory.step_progress_agrees line 34
lemma OAI.SLEExactGauge.RibbonHistory.affine_recentered line 50
lemma OAI.SLEExactGauge.RibbonHistory.passage_translate line 58
lemma OAI.SLEExactGauge.RibbonHistory.middle_translate line 67

theorem OAI.SLEExactGauge.RibbonHistory.frontMass_probability_translate line 95

Source documentation

Translating the actual finite boundary image back to its original tip preserves the full probability, including the original middle-strip mass.

theorem RibbonHistory.frontMass_probability_translate
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    {C L : ℝ≥0} {ε : ℝ} (d : RibbonHistory C L ε) (hε : ε ≤ 1 / 8)
    (η : Ω → ℝ≥0 → ℂ) (κ v c : ℝ) (hv : 0 < v) :
    P {ω | (fun t => affine (d.trace d.time) 1 (η ω t)) ∈
        {f : ℝ≥0 → ℂ | f ∈ PassageSuccess.FrontSuccess
          (fun _ (f : ℝ≥0 → ℂ) => f)
          (fun _ => longitudinalCoordinate d.chart closedRibbon d.front) (fun _ => 0)
          (fun _ => physicalPassageRegion d.stepChart ribbonStepCompact C ε (ε / L))
          (fun _ => d.chart ((d.front : ℂ) + 1)) (ε / L) 0 ∧
          ENNReal.ofReal c ≤ segmentSausageCharge κ f 0
            (FirstFrontPassage.frontTime
…

Mentions: OAI.SLEExactGauge.RibbonHistory, OAI.SLEExactGauge.PassageSuccess.FrontSuccess, OAI.SLEExactGauge.segmentSausageCharge, OAI.SLEExactGauge.FirstFrontPassage.frontTime