CanonicalMassRestart.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The canonical raw driver functional restarts through the actual inverse Loewner chart. The trace-generation input is precisely the published one already used for ordinary SLE, and strong Markov provides each fresh path.

theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.exists_raw_pathwise_restart line 24

Source documentation

One raw functional realizes the original mass and satisfies the finite and terminal pathwise restart identities at every finite stopping time.

theorem CanonicalMass.exists_raw_pathwise_restart
    (C : CanonicalMass P κ B hBm γ G) (hB : IsBrownianReal B P)
    (hc : ∀ ω, Continuous (fun t => B t ω)) (hκ : 0 < κ)
    (F : Ω → ℝ≥0 → ℂ → ℂ)
    (hw : ∀ ω, IsCapacityTwoWitness (fun t => Real.sqrt κ*B t ω) (γ ω) (G ω) (F ω))
    (hpublished : PublishedTraceGeneration (P.map (sourceDriverPath B hc)) κ (fun t p => p t)) :
    ∃ R : RawCanonicalMass,
      (∀ᵐ ω ∂P, (∀ t, R.process t (sourceDriverPath B hc ω)=C.process t ω) ∧
        R.terminal (sourceDriverPath B hc ω)=C.rational.terminal ω) ∧
      ∀ (τ : Ω → ℝ≥0)
        (_hτ : IsStoppingTime (Filtration.natural B (fun s =>
          (hBm.comp (measurable_const.prodMk measurable_id) : Measurable (B s)).stronglyMeasurable))
…

Mentions: OAI.SLEExactGauge.Multipoint.CanonicalMass, OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.PublishedTraceGeneration, OAI.SLEExactGauge.sourceDriverPath, OAI.SLEExactGauge.Multipoint.RawCanonicalMass