OAI/Probability/SLE/Mass/CanonicalMassImageRestart.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SLEExactGauge.Multipoint.CanonicalMass.exists_raw_all_image_restart line 24

   Source documentation

   Every fixed conformal image inherits the pathwise restart identity, with the same raw functional and one event for all image maps and later times.

   theorem CanonicalMass.exists_raw_all_image_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 ω) ∧
         ∀ (S : Ω → WithTop ℝ≥0)
           (_hS : IsStoppingTime (Filtration.natural B (fun s =>
             (hBm.comp (measurable_const.prodMk measurable_id) : Measurable (B s)).stronglyMeasurable)) S),
   …

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