ActualRibbonStep.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

A measurable narrow physical prefix yields the exact actual history. A successful uniform step yields the next such prefix and an actual mass window between successive global first-front times.

def OAI.SLEExactGauge.ribbonPathStep line 19
Source documentation
The path-space step event is deterministic once the chart and integer front are fixed, although the actual Loewner history is random.
```
def ribbonPathStep (P : ℂ → ℂ) (C L : ℝ≥0) (ε k κ v c : ℝ) : Set C(ℝ≥0, ℂ) :=
…
```
lemma OAI.SLEExactGauge.RibbonHistory.stepEvent_eq_ribbonPathStep line 24
lemma OAI.SLEExactGauge.ribbonPathStep_measurable line 28
theorem OAI.SLEExactGauge.actual_history_of_goodRibbonPrefix line 68

theorem OAI.SLEExactGauge.RibbonHistory.actual_step_success line 104

Source documentation

The uniform step's mass is charged to the actual successive global fronts, and its continuation is again a good measurable physical prefix.

theorem RibbonHistory.actual_step_success
    {C L : ℝ≥0} {ε : ℝ} (d : RibbonHistory C L ε)
    (hε : ε ≤ 1 / 8) (hL : 0 < L) (κ v c : ℝ)
    (g : C(ℂ, ℝ)) (hg : ∀ z ∈ closedRibbon, g (d.chart z) = z.re)
    (hstep : d.futureTrace ∈ d.stepEvent κ v c)
    (hupper : LipschitzOnWith C d.chart (ribbonStepPatch (d.front + 1)))
    (hlower : ∀ u ∈ ribbonStepPatch (d.front + 1),
      ∀ v ∈ ribbonStepPatch (d.front + 1), dist u v ≤ L * dist (d.chart u) (d.chart v)) :
    () ∈ RibbonStepSuccess (fun _ : Unit => d.trace)
      (fun _ => firstFrontTime (fun t => g (d.trace t)) d.front)
      (fun _ => firstFrontTime (fun t => g (d.trace t)) (d.front + 1))
      d.chart ε κ v c (physicalMiddleRegion d.chart closedRibbon d.front ε) := by
…

Mentions: OAI.SLEExactGauge.RibbonHistory, OAI.SLEExactGauge.RibbonStepSuccess