OAI/Probability/SLE/Stochastic/ProgressiveStoppedTime.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Stopped-value measurability for a progressive process with a merely measurable target, in particular a measure-valued canonical mass.

  1. lemma OAI.MeasureTheory.IsProgressive.bounded_stopped_measurable line 19
  2. lemma OAI.MeasureTheory.IsProgressive.truncated_stopped_measurable line 35
  3. theorem OAI.MeasureTheory.IsProgressive.stopped_time_measurable line 44

    Source documentation

    This requires no topology on the target.

    theorem stopped_time_measurable (hN : _root_.MeasureTheory.IsProgressive ℱ N)
    (τ : Ω → ℝ≥0)
    (hτ : _root_.MeasureTheory.IsStoppingTime ℱ (fun ω => (τ ω : WithTop ℝ≥0))) :
    Measurable[hτ.measurableSpace] (fun ω => N (τ ω) ω) := by
…
  4. theorem OAI.MeasureTheory.IsProgressive.shifted_adapted line 76

    Source documentation

    The original measure-valued process evaluated after a finite stopping time is adapted to the full shifted stopped-past filtration.

    theorem shifted_adapted (hN : _root_.MeasureTheory.IsProgressive ℱ N)
    (τ : Ω → ℝ≥0)
    (hτ : _root_.MeasureTheory.IsStoppingTime ℱ (fun ω => (τ ω : WithTop ℝ≥0))) :
    _root_.MeasureTheory.Adapted (SLEExactGauge.shiftedStoppingFiltration hτ)
      (fun t ω => N (τ ω+t) ω) := by
…

    Mentions: OAI.SLEExactGauge.shiftedStoppingFiltration