AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.TimeMeasure

- Lebesgue measure on nonnegative real time, pulled back along the canonical embedding into the real line.

noncomputable def nnrealLebesgue : Measure ℝ≥0 :=
  Measure.comap ((↑) : ℝ≥0 → ℝ)
    (@MeasureSpace.volume ℝ inferInstance)

/-- Finite Lebesgue measure on nonnegative time up to `T`. Defining the
restriction before pulling back supplies Mathlib's finite-measure instance. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/TimeMeasure.lean:21published source at 77184245109a

- Finite Lebesgue measure on nonnegative time up to `T`. Defining the restriction before pulling back supplies Mathlib's finite-measure instance.

noncomputable def upTo (T : ℝ≥0) : Measure ℝ≥0 :=
  Measure.comap ((↑) : ℝ≥0 → ℝ)
    ((@MeasureSpace.volume ℝ inferInstance).restrict (Icc 0 (T : ℝ)))

noncomputable instance (T : ℝ≥0) : IsFiniteMeasure (upTo T) := by
  unfold upTo
  infer_instance

/-- The stopped time measure is literally nonnegative Lebesgue measure
restricted to `[0,T]`.  This bridge lets source statements written with a
restricted Lebesgue integral reuse the finite `upTo T` measure used by the
Itô construction. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/TimeMeasure.lean:27published source at 77184245109a

- The stopped time measure is literally nonnegative Lebesgue measure restricted to `[0,T]`. This bridge lets source statements written with a restricted Lebesgue integral reuse the finite `upTo T` measure used by the Itô construction.

theorem upTo_eq_restrict_nnrealLebesgue (T : ℝ≥0) :
    upTo T = nnrealLebesgue.restrict (Icc 0 T) := by
  unfold upTo nnrealLebesgue
  change
    Measure.comap (Subtype.val : ℝ≥0 → ℝ)
        (volume.restrict (Icc 0 (T : ℝ))) =
      (Measure.comap (Subtype.val : ℝ≥0 → ℝ) volume).restrict (Icc 0 T)
  have hcoe : MeasurableEmbedding (Subtype.val : ℝ≥0 → ℝ) :=
    MeasurableEmbedding.subtype_coe
      (measurableSet_Ici : MeasurableSet (Ici (0 : ℝ)))
  have hpre :
      (Subtype.val : ℝ≥0 → ℝ) ⁻¹' Icc 0 (T : ℝ) = Icc 0 T := by
    ext t
    constructor
    · intro ht
      exact ⟨zero_le, by exact_mod_cast ht.2⟩
    · intro ht
      exact ⟨t.property, by exact_mod_cast ht.2⟩
  calc
    Measure.comap (Subtype.val : ℝ≥0 → ℝ)
        (volume.restrict (Icc 0 (T : ℝ))) =
      (Measure.comap (Subtype.val : ℝ≥0 → ℝ) volume).restrict
        ((Subtype.val : ℝ≥0 → ℝ) ⁻¹' Icc 0 (T : ℝ)) :=
      hcoe.comap_restrict volume (Icc 0 (T : ℝ))
    _ = (Measure.comap (Subtype.val : ℝ≥0 → ℝ) volume).restrict (Icc 0 T) :=
      congrArg
        (fun s : Set ℝ≥0 => (Measure.comap (Subtype.val : ℝ≥0 → ℝ) volume).restrict s)
        hpre

/-- Restricting two larger finite horizons to the same earlier prefix gives
exactly the same time measure.  This is the cross-horizon consistency used by
global localization. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/TimeMeasure.lean:39published source at 77184245109a

- Restricting two larger finite horizons to the same earlier prefix gives exactly the same time measure. This is the cross-horizon consistency used by global localization.

theorem restrict_upTo_Iio_eq_of_le {t T₁ T₂ : ℝ≥0}
    (ht : t ≤ T₁) (hT : T₁ ≤ T₂) :
    (upTo T₁).restrict (Iio t) = (upTo T₂).restrict (Iio t) := by
  rw [upTo_eq_restrict_nnrealLebesgue, upTo_eq_restrict_nnrealLebesgue]
  ext s hs
  rw [Measure.restrict_apply hs, Measure.restrict_apply hs]
  have hsi : MeasurableSet (s ∩ Iio t) := hs.inter measurableSet_Iio
  rw [Measure.restrict_apply hsi, Measure.restrict_apply hsi]
  congr 1
  ext x
  simp only [mem_inter_iff, mem_Iio, mem_Icc]
  constructor
  · rintro ⟨⟨hsx, hxt⟩, hx0, _hxT₁⟩
    exact ⟨⟨hsx, hxt⟩, hx0, hxt.le.trans ht |>.trans hT⟩
  · rintro ⟨⟨hsx, hxt⟩, hx0, _hxT₂⟩
    exact ⟨⟨hsx, hxt⟩, hx0, hxt.le.trans ht⟩

/-- The total mass of nonnegative time stopped at `T` is `T`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/TimeMeasure.lean:71published source at 77184245109a

- The total mass of nonnegative time stopped at `T` is `T`.

theorem upTo_univ (T : ℝ≥0) : upTo T Set.univ = T := by
  have himage : NNReal.toReal '' (Set.univ : Set ℝ≥0) = Ici (0 : ℝ) := by
    ext r
    constructor
    · rintro ⟨s, _, rfl⟩
      exact s.property
    · intro hr
      exact ⟨⟨r, hr⟩, Set.mem_univ _, rfl⟩
  have hinter : Ici (0 : ℝ) ∩ Icc 0 (T : ℝ) = Icc 0 (T : ℝ) := by
    exact inter_eq_right.mpr fun r hr ↦ hr.1
  calc
    upTo T Set.univ =
        (volume.restrict (Icc 0 (T : ℝ)))
          (NNReal.toReal '' (Set.univ : Set ℝ≥0)) := by
      unfold upTo
      exact Measure.comap_apply NNReal.toReal NNReal.coe_injective
        (fun _ hs => (MeasurableEmbedding.subtype_coe
          (measurableSet_Ici : MeasurableSet (Ici (0 : ℝ)))).measurableSet_image' hs)
        _ MeasurableSet.univ
    _ = T := by
      rw [himage, Measure.restrict_apply measurableSet_Ici, hinter, Real.volume_Icc]
      simp

/-- Stopped Lebesgue time has no atoms. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/TimeMeasure.lean:89published source at 77184245109a

- Stopped Lebesgue time has no atoms.

@[simp] theorem upTo_singleton (T t : ℝ≥0) : upTo T {t} = 0 := by
  calc
    upTo T {t} =
        (volume.restrict (Icc 0 (T : ℝ)))
          (NNReal.toReal '' ({t} : Set ℝ≥0)) := by
      unfold upTo
      exact Measure.comap_apply NNReal.toReal NNReal.coe_injective
        (fun _ hs => (MeasurableEmbedding.subtype_coe
          (measurableSet_Ici : MeasurableSet (Ici (0 : ℝ)))).measurableSet_image' hs)
        _ (measurableSet_singleton t)
    _ = 0 := by simp

/-- The mass of `(a, b]` under time measure stopped at `T` is the length of
the clipped interval. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/TimeMeasure.lean:113published source at 77184245109a

- The mass of `(a, b]` under time measure stopped at `T` is the length of the clipped interval.

theorem upTo_Ioc (T a b : ℝ≥0) (hab : a ≤ b) :
    upTo T (Ioc a b) = ↑(min b T - min a T) := by
  calc
    upTo T (Ioc a b) =
        (volume.restrict (Icc 0 (T : ℝ))) (NNReal.toReal '' Ioc a b) := by
      unfold upTo
      exact Measure.comap_apply NNReal.toReal NNReal.coe_injective
        (fun _ hs => (MeasurableEmbedding.subtype_coe
          (measurableSet_Ici : MeasurableSet (Ici (0 : ℝ)))).measurableSet_image' hs)
        _ (measurableSet_Ioc : MeasurableSet (Ioc a b))
    _ = ↑(min b T - min a T) := by
      rw [NNReal.image_coe_Ioc, Measure.restrict_apply measurableSet_Ioc]
      have hinter :
          Ioc (a : ℝ) (b : ℝ) ∩ Icc 0 (T : ℝ) =
            Ioc ((min a T : ℝ≥0) : ℝ) ((min b T : ℝ≥0) : ℝ) := by
        ext x
        simp only [mem_inter_iff, mem_Ioc, mem_Icc, NNReal.coe_min,
          min_lt_iff, le_min_iff]
        constructor
        · rintro ⟨⟨hax, hxb⟩, hx0, hxT⟩
          exact ⟨Or.inl hax, hxb, hxT⟩
        · rintro ⟨hax | hTx, hxb, hxT⟩
          · exact ⟨⟨hax, hxb⟩, le_trans a.property hax.le, hxT⟩
          · exact (not_lt_of_ge hxT hTx).elim
      rw [hinter, Real.volume_Ioc]
      rw [← NNReal.coe_sub (min_le_min hab le_rfl)]
      simp

/-- Stopped nonnegative Lebesgue time lies in `(0,T]` almost everywhere;
the omitted initial endpoint is null. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/TimeMeasure.lean:127published source at 77184245109a

- Stopped nonnegative Lebesgue time lies in `(0,T]` almost everywhere; the omitted initial endpoint is null.

theorem ae_mem_Ioc_zero_upTo (T : ℝ≥0) :
    ∀ᵐ t ∂upTo T, t ∈ Ioc 0 T := by
  apply (ae_mem_iff_measure_eq measurableSet_Ioc.nullMeasurableSet).2
  rw [upTo_Ioc T 0 T (by simp), upTo_univ]
  simp

/-- Restricting stopped time to `(0,T]` leaves the measure unchanged. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/TimeMeasure.lean:157published source at 77184245109a

- Restricting stopped time to `(0,T]` leaves the measure unchanged.

theorem restrict_upTo_Ioc_zero (T : ℝ≥0) :
    (upTo T).restrict (Ioc 0 T) = upTo T :=
  Measure.restrict_eq_self_of_ae_mem (ae_mem_Ioc_zero_upTo T)

/-- The finite time measure is supported on `[0,T]`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/TimeMeasure.lean:164published source at 77184245109a

- The finite time measure is supported on `[0,T]`.

theorem upTo_Ioi_terminal (T : ℝ≥0) : upTo T (Ioi T) = 0 := by
  have himage : NNReal.toReal '' Ioi T = Ioi (T : ℝ) := by
    ext r
    constructor
    · rintro ⟨s, hs, rfl⟩
      exact_mod_cast hs
    · intro hr
      have hr0 : 0 ≤ r := T.property.trans hr.le
      refine ⟨⟨r, hr0⟩, ?_, rfl⟩
      exact_mod_cast hr
  have hinter : Ioi (T : ℝ) ∩ Icc 0 (T : ℝ) = ∅ := by
    apply Set.eq_empty_iff_forall_notMem.mpr
    intro r hr
    exact (not_lt_of_ge hr.2.2) hr.1
  calc
    upTo T (Ioi T) =
        (volume.restrict (Icc 0 (T : ℝ))) (NNReal.toReal '' Ioi T) := by
      unfold upTo
      exact Measure.comap_apply NNReal.toReal NNReal.coe_injective
        (fun _ hs => (MeasurableEmbedding.subtype_coe
          (measurableSet_Ici : MeasurableSet (Ici (0 : ℝ)))).measurableSet_image' hs)
        _ (measurableSet_Ioi : MeasurableSet (Ioi T))
    _ = 0 := by
      rw [himage, Measure.restrict_apply measurableSet_Ioi, hinter, measure_empty]

/-- Almost every time under `upTo T` lies below the terminal horizon. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/TimeMeasure.lean:169published source at 77184245109a

- Almost every time under `upTo T` lies below the terminal horizon.

theorem ae_le_terminal (T : ℝ≥0) : ∀ᵐ s ∂upTo T, s ≤ T := by
  filter_upwards [ae_mem_Ioc_zero_upTo T] with s hs
  exact hs.2

/-- The terminal endpoint itself is null, so almost every stopped time is
strictly before `T`. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/TimeMeasure.lean:195published source at 77184245109a

- The terminal endpoint itself is null, so almost every stopped time is strictly before `T`.

theorem ae_lt_terminal (T : ℝ≥0) : ∀ᵐ s ∂upTo T, s < T := by
  have hne : ∀ᵐ s ∂upTo T, s ∉ ({T} : Set ℝ≥0) :=
    measure_eq_zero_iff_ae_notMem.mp (upTo_singleton T T)
  filter_upwards [ae_le_terminal T, hne] with s hs hsne
  exact lt_of_le_of_ne hs (by simpa only [mem_singleton_iff] using hsne)

/-- Restricting `[0,T]` to the open terminal prefix `[0,T)` changes nothing,
because the omitted endpoint has zero Lebesgue mass. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/TimeMeasure.lean:201published source at 77184245109a

- Restricting `[0,T]` to the open terminal prefix `[0,T)` changes nothing, because the omitted endpoint has zero Lebesgue mass.

theorem restrict_upTo_Iio_terminal (T : ℝ≥0) :
    (upTo T).restrict (Iio T) = upTo T :=
  Measure.restrict_eq_self_of_ae_mem (ae_lt_terminal T)

end TimeMeasure
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/TimeMeasure.lean:209published source at 77184245109a