OAI/Probability/SLE/Gauge/RibbonHistoryAdvance.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

An actual successful passage gives another admissible stopped ribbon history. Inverse coordinates are used only on the compact physical patch where the successful path is contained.

  1. lemma OAI.SLEExactGauge.strict_before_attained_front line 16
  2. def OAI.SLEExactGauge.RibbonHistory.futureCoordinates line 32
  3. def OAI.SLEExactGauge.RibbonHistory.advanceCoordinates line 36
  4. def OAI.SLEExactGauge.RibbonHistory.futureTrace line 40
  5. lemma OAI.SLEExactGauge.RibbonHistory.tip_in_stepCompact line 45
  6. lemma OAI.SLEExactGauge.RibbonHistory.futureCoordinates_zero line 55
  7. theorem OAI.SLEExactGauge.RibbonHistory.successful_continuation line 68

    Source documentation

    The completed actual trace retains continuous ribbon coordinates, the narrow core, and the strict first-front property required for the next application of the uniform step theorem.

    theorem RibbonHistory.successful_continuation
    {C L : ℝ≥0} {ε : ℝ} (d : RibbonHistory C L ε)
    (hε : ε ≤ 1 / 8) (hL : 0 < L)
    (S : ℝ≥0)
    (hfirst : firstFrontTime
      (fun t => longitudinalCoordinate d.chart closedRibbon d.front
        (d.trace (d.time + t))) 1 = (S : WithTop ℝ≥0))
    (hhit : longitudinalCoordinate d.chart closedRibbon d.front
      (d.trace (d.time + S)) = 1)
    (hS : 0 < S)
    (hpath : MapsTo (fun t => d.trace (d.time + t)) (Icc 0 S)
      (physicalPassageRegion d.stepChart ribbonStepCompact C ε (ε / L)))
…

    Mentions: OAI.SLEExactGauge.RibbonHistory

  8. theorem OAI.SLEExactGauge.RibbonHistory.next_history_of_stepEvent line 210

    Source documentation

    A successful full step produces the actual history at the next integer front, with the same driver, trace, and Loewner maps. The only new geometric data are the deterministic bounds on the next patch.

    theorem RibbonHistory.next_history_of_stepEvent
    {C L : ℝ≥0} {ε : ℝ} (d : RibbonHistory C L ε)
    (hε : ε ≤ 1 / 8) (hL : 0 < L) (κ v c : ℝ)
    (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)) :
    ∃ d' : RibbonHistory C L ε,
      d'.front = d.front + 1 ∧
      d'.time = d.time + frontTime
        (fun t => longitudinalCoordinate d.chart closedRibbon d.front (d.futureTrace t)) 1 ∧
      d'.chart = d.chart ∧ d'.U = d.U ∧ d'.trace = d.trace ∧
…

    Mentions: OAI.SLEExactGauge.RibbonHistory