AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Stopping

- The product-space closed stopping event is measurable.

theorem measurableSet_stoppingSet
    (tau : Omega → WithTop ℝ≥0)
    (htau : IsChewiStoppingTime filtration tau) :
    MeasurableSet (stoppingSet tau) := by
  have ht : Measurable (fun z : Omega × ℝ≥0 => (z.2 : WithTop ℝ≥0)) :=
    (measurable_snd : Measurable (fun z : Omega × ℝ≥0 => z.2)).withTop_coe
  have htau' : MeasureTheory.IsStoppingTime filtration tau := htau
  have hτ : Measurable (fun z : Omega × ℝ≥0 => tau z.1) :=
    htau'.measurable'.comp measurable_fst
  simpa only [stoppingSet] using measurableSet_le ht hτ

/-- Chewi's closed stopping convention preserves strong progressiveness. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Stopping.lean:34published source at 7bcd37294df1

- Chewi's closed stopping convention preserves strong progressiveness.

theorem stoppedIntegrand_stronglyProgressive
    (eta : ProgressiveL2Integrand filtration mu T)
    (tau : Omega → WithTop ℝ≥0)
    (htau : IsChewiStoppingTime filtration tau) :
    IsStronglyProgressive filtration (stoppedIntegrand eta.process tau) := by
  have htau' : MeasureTheory.IsStoppingTime filtration tau := htau
  intro i
  have hτmin : Measurable[filtration i]
      (fun omega => min (tau omega) (i : WithTop ℝ≥0)) :=
    (htau'.min_const i).measurable_of_le (fun omega => min_le_right _ _)
  have htime : Measurable[Subtype.instMeasurableSpace.prod (filtration i)]
      (fun p : Set.Iic i × Omega => ((p.1 : ℝ≥0) : WithTop ℝ≥0)) :=
    (measurable_subtype_coe.comp measurable_fst).withTop_coe
  have hτprod : Measurable[Subtype.instMeasurableSpace.prod (filtration i)]
      (fun p : Set.Iic i × Omega => min (tau p.2) (i : WithTop ℝ≥0)) :=
    hτmin.comp measurable_snd
  have hsetMin : @MeasurableSet (Set.Iic i × Omega)
      (Subtype.instMeasurableSpace.prod (filtration i))
      {p | ((p.1 : ℝ≥0) : WithTop ℝ≥0) ≤
        min (tau p.2) (i : WithTop ℝ≥0)} :=
    measurableSet_le htime hτprod
  have heq :
      {p : Set.Iic i × Omega |
        ((p.1 : ℝ≥0) : WithTop ℝ≥0) ≤ tau p.2} =
      {p : Set.Iic i × Omega |
        ((p.1 : ℝ≥0) : WithTop ℝ≥0) ≤
          min (tau p.2) (i : WithTop ℝ≥0)} := by
    ext p
    change
      (((p.1 : ℝ≥0) : WithTop ℝ≥0) ≤ tau p.2) ↔
        ((p.1 : ℝ≥0) : WithTop ℝ≥0) ≤
          min (tau p.2) (i : WithTop ℝ≥0)
    constructor
    · intro hptau
      apply le_min hptau
      exact_mod_cast p.1.property
    · intro hpmin
      exact hpmin.trans (min_le_left _ _)
  have hset : @MeasurableSet (Set.Iic i × Omega)
      (Subtype.instMeasurableSpace.prod (filtration i))
      {p | ((p.1 : ℝ≥0) : WithTop ℝ≥0) ≤ tau p.2} := by
    rw [heq]
    exact hsetMin
  exact StronglyMeasurable.ite hset (eta.progressive i) stronglyMeasurable_const
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Stopping.lean:46published source at 7bcd37294df1

Excerpt truncated; the exact source link is authoritative.

- The closed stopped integrand remains in product-space `L²`.

theorem stoppedIntegrand_memLp
    (eta : ProgressiveL2Integrand filtration mu T)
    (tau : Omega → WithTop ℝ≥0)
    (htau : IsChewiStoppingTime filtration tau) :
    MemLp (processFunction (stoppedIntegrand eta.process tau)) 2
      (processTimeMeasure mu T) := by
  rw [processFunction_stoppedIntegrand_eq_indicator]
  exact eta.memLp.indicator (measurableSet_stoppingSet tau htau)

/-- Generic closed stopping operator on completed progressive `L²` integrands. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Stopping.lean:92published source at 7bcd37294df1

- Generic closed stopping operator on completed progressive `L²` integrands.

noncomputable def stop
    (eta : ProgressiveL2Integrand filtration mu T)
    (tau : Omega → WithTop ℝ≥0)
    (htau : IsChewiStoppingTime filtration tau) :
    ProgressiveL2Integrand filtration mu T where
  process := stoppedIntegrand eta.process tau
  progressive := stoppedIntegrand_stronglyProgressive eta tau htau
  memLp := stoppedIntegrand_memLp eta tau htau

@[simp]

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Stopping.lean:102published source at 7bcd37294df1

No declaration docstring.

theorem stop_process
    (eta : ProgressiveL2Integrand filtration mu T)
    (tau : Omega → WithTop ℝ≥0)
    (htau : IsChewiStoppingTime filtration tau) :
    (stop eta tau htau).process = stoppedIntegrand eta.process tau := rfl

/-- Closed stopping is a contraction on the completed progressive `L²` space. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Stopping.lean:112published source at 7bcd37294df1

- Closed stopping is a contraction on the completed progressive `L²` space.

theorem norm_stop_sub_stop_le
    (eta xi : ProgressiveL2Integrand filtration mu T)
    (tau : Omega → WithTop ℝ≥0)
    (htau : IsChewiStoppingTime filtration tau) :
    ‖(stop eta tau htau).toLp - (stop xi tau htau).toLp‖ ≤
      ‖eta.toLp - xi.toLp‖ := by
  apply norm_stopped_sub_le eta xi (stop eta tau htau) (stop xi tau htau) tau
  · exact Filter.Eventually.of_forall fun _ => rfl
  · exact Filter.Eventually.of_forall fun _ => rfl

/-- Stopping preserves convergence in the completed progressive `L²` space. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Stopping.lean:119published source at 7bcd37294df1

- Stopping preserves convergence in the completed progressive `L²` space.

theorem tendsto_stop_toLp_of_tendsto
    (eta : ProgressiveL2Integrand filtration mu T)
    (approx : ℕ → ProgressiveL2Integrand filtration mu T)
    (tau : Omega → WithTop ℝ≥0)
    (htau : IsChewiStoppingTime filtration tau)
    (happrox : Tendsto (fun n => (approx n).toLp) atTop (𝓝 eta.toLp)) :
    Tendsto (fun n => (stop (approx n) tau htau).toLp) atTop
      (𝓝 (stop eta tau htau).toLp) := by
  apply tendsto_iff_norm_sub_tendsto_zero.mpr
  apply squeeze_zero
    (fun n => norm_nonneg ((stop (approx n) tau htau).toLp - (stop eta tau htau).toLp))
    (fun n => norm_stop_sub_stop_le (approx n) eta tau htau)
  exact tendsto_iff_norm_sub_tendsto_zero.mp happrox

end ProgressiveL2Stopping
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/ProgressiveL2Stopping.lean:130published source at 7bcd37294df1