OAI/Probability/SLE/Loewner/RestartDriverScaling.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SLEExactGauge.scaleDriverPath line 18
2. lemma OAI.SLEExactGauge.measurable_scaleDriverPath line 22
3. lemma OAI.SLEExactGauge.brownian_scaled_driver_path_law line 32
4. theorem OAI.SLEExactGauge.restart_random_transform_law line 54

   Source documentation

   A measurable transformation of the fresh path may depend on the stopped past if each of its sections preserves the fresh path law.

   theorem restart_random_transform_law
       {Ω X : Type*} [mΩ : MeasurableSpace Ω] [mX : MeasurableSpace X]
       (P : Measure Ω) [IsFiniteMeasure P] (ν : Measure X) [IsFiniteMeasure ν]
       (m : MeasurableSpace Ω) (hm : m ≤ mΩ)
       (Y : Ω → X) (hY : Measurable[mΩ] Y)
       (hlaw : ∀ A : Set Ω, MeasurableSet[m] A →
         @Measure.map Ω X mΩ mX Y (P.restrict A) = P A • ν)
       (H : Ω × X → X) (hH : @Measurable (Ω × X) X (m.prod mX) mX H)
       (hsections : ∀ ω, ν.map (fun x => H (ω, x)) = ν)
       (A : Set Ω) (hA : MeasurableSet[m] A) :
       @Measure.map Ω X mΩ mX (fun ω => H (ω, Y ω)) (P.restrict A) = P A • ν := by
   …

5. theorem OAI.SLEExactGauge.source_restart_random_scale_driver_law line 103

   Source documentation

   The normalized fresh driver has the original continuous Brownian law on every event in the stopped past, even with a random past-measurable scale.

   theorem source_restart_random_scale_driver_law
       {Ω : Type*} [mΩ : MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P]
       (B : ℝ≥0 → Ω → ℝ) (hB : IsBrownianReal B P)
       (hm : ∀ t, Measurable (B t)) (hc : ∀ ω, Continuous (fun t => B t ω))
       (τ : Ω → ℝ≥0)
       (hτ : IsStoppingTime (Filtration.natural B (fun t => (hm t).stronglyMeasurable))
         (fun ω => (τ ω : WithTop ℝ≥0)))
       (c : Ω → ℝ≥0) (hcm : Measurable[hτ.measurableSpace] c) (hcpos : ∀ ω, 0 < c ω)
       (A : Set Ω) (hA : MeasurableSet[hτ.measurableSpace] A) :
       (P.restrict A).map (fun ω => scaleDriverPath (c ω) (sourceRestartDriverPath B hc τ ω)) =
         P A • P.map (sourceDriverPath B hc) := by
   …

   Mentions: OAI.SLEExactGauge.scaleDriverPath, OAI.SLEExactGauge.sourceRestartDriverPath, OAI.SLEExactGauge.sourceDriverPath