AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.RandomStoppingL2Convergence

- The deterministic coefficient-sum bound used below is nonnegative.

theorem valueBound_nonneg
    (eta : DyadicElementaryProcess filtration T) :
    0 ≤ valueBound eta.process := by
  unfold valueBound
  exact Finset.sum_nonneg fun i _ => le_max_left 0 _

/-- The pointwise error between a stopped refinement and its stopped target is
bounded by twice the original elementary-process bound. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/RandomStoppingL2Convergence.lean:36published source at 7bcd37294df1

- The pointwise error between a stopped refinement and its stopped target is bounded by twice the original elementary-process bound.

theorem abs_stopRefinedDyadic_sub_stoppedIntegrand_le
    (eta : DyadicElementaryProcess filtration T)
    (tau : Omega → ℝ≥0)
    (htau : IsChewiStoppingTime filtration
      (fun omega => (tau omega : WithTop ℝ≥0)))
    (htauT : ∀ omega, tau omega ≤ T)
    (n : ℕ) (s : ℝ≥0) (omega : Omega) :
    |(stopRefinedDyadic eta tau htau n).process.value s omega -
        Localization.stoppedIntegrand eta.process.value
          (fun w => (tau w : WithTop ℝ≥0)) s omega| ≤
      2 * valueBound eta.process := by
  calc
    |(stopRefinedDyadic eta tau htau n).process.value s omega -
        Localization.stoppedIntegrand eta.process.value
          (fun w => (tau w : WithTop ℝ≥0)) s omega| ≤
      |(stopRefinedDyadic eta tau htau n).process.value s omega| +
        |Localization.stoppedIntegrand eta.process.value
          (fun w => (tau w : WithTop ℝ≥0)) s omega| := abs_sub _ _
    _ ≤ valueBound eta.process + valueBound eta.process :=
      add_le_add
        (abs_stopRefinedDyadic_value_le_valueBound eta tau htau htauT n s omega)
        (abs_stoppedIntegrand_le_valueBound eta tau s omega)
    _ = 2 * valueBound eta.process := by ring

/-- Dominated convergence for the squared product-space error.  This is the
measure-theoretic core of random-stopping convergence. -/

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/RandomStoppingL2Convergence.lean:44published source at 7bcd37294df1

- Dominated convergence for the squared product-space error. This is the measure-theoretic core of random-stopping convergence.

theorem tendsto_integral_sq_stopRefinedDyadic_sub
    [IsFiniteMeasure mu]
    (eta : DyadicElementaryProcess filtration T)
    (tau : Omega → ℝ≥0)
    (htau : IsChewiStoppingTime filtration
      (fun omega => (tau omega : WithTop ℝ≥0)))
    (htauT : ∀ omega, tau omega ≤ T) :
    Tendsto
      (fun n =>
        ∫ z,
          ((stopRefinedDyadic eta tau htau n).process.value z.2 z.1 -
            Localization.stoppedIntegrand eta.process.value
              (fun w => (tau w : WithTop ℝ≥0)) z.2 z.1) ^ 2
          ∂processTimeMeasure mu T)
      atTop (𝓝 0) := by
  let _ : IsFiniteMeasure (processTimeMeasure mu T) := by
    unfold processTimeMeasure
    infer_instance
  let target := stoppedProgressiveL2 (mu := mu) eta tau htau htauT
  let approximation : ℕ → ProgressiveL2Integrand filtration mu T := fun n =>
    toProgressiveL2 (stopRefinedDyadic eta tau htau n).process mu T
  let error : ℕ → Omega × ℝ≥0 → ℝ := fun n z =>
    (approximation n).process z.2 z.1 - target.process z.2 z.1
  have herrorMem : ∀ n, MemLp (error n) 2 (processTimeMeasure mu T) := by
    intro n
    exact (approximation n).memLp.sub target.memLp
  have hmeas : ∀ n,
      AEStronglyMeasurable (fun z => (error n z) ^ 2)
        (processTimeMeasure mu T) := fun n =>
    (herrorMem n).integrable_sq.aestronglyMeasurable
  have hboundIntegrable :
      Integrable (fun _ : Omega × ℝ≥0 =>
        4 * (valueBound eta.process) ^ 2)
        (processTimeMeasure mu T) :=
    MeasureTheory.integrable_const
      (μ := processTimeMeasure mu T) (4 * (valueBound eta.process) ^ 2)
  have hbound : ∀ n, ∀ᵐ z ∂processTimeMeasure mu T,
      ‖(error n z) ^ 2‖ ≤ 4 * (valueBound eta.process) ^ 2 := by
    intro n
    filter_upwards [] with z
    have herr := abs_stopRefinedDyadic_sub_stoppedIntegrand_le
      eta tau htau htauT n z.2 z.1
    change |error n z| ≤ 2 * valueBound eta.process at herr
    calc
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/RandomStoppingL2Convergence.lean:70published source at 7bcd37294df1

Excerpt truncated; the exact source link is authoritative.

- The stopped dyadic refinements converge to the stopped elementary integrand in the actual product-space `L2` object.

theorem tendsto_stopRefinedDyadic_toLp
    [IsFiniteMeasure mu]
    (eta : DyadicElementaryProcess filtration T)
    (tau : Omega → ℝ≥0)
    (htau : IsChewiStoppingTime filtration
      (fun omega => (tau omega : WithTop ℝ≥0)))
    (htauT : ∀ omega, tau omega ≤ T) :
    Tendsto
      (fun n => (stopRefinedDyadic eta tau htau n).toLp mu)
      atTop
      (𝓝 (stoppedProgressiveL2 (mu := mu) eta tau htau htauT).toLp) := by
  let target := stoppedProgressiveL2 (mu := mu) eta tau htau htauT
  let approximation : ℕ → ProgressiveL2Integrand filtration mu T := fun n =>
    toProgressiveL2 (stopRefinedDyadic eta tau htau n).process mu T
  have hnormSq (n : ℕ) :
      ‖(approximation n).toLp - target.toLp‖ ^ 2 =
        ∫ z,
          ((stopRefinedDyadic eta tau htau n).process.value z.2 z.1 -
            Localization.stoppedIntegrand eta.process.value
              (fun w => (tau w : WithTop ℝ≥0)) z.2 z.1) ^ 2
          ∂processTimeMeasure mu T := by
    have h := norm_sq_toLp_eq_integral_sq
      ((approximation n).memLp.sub target.memLp)
    rw [MemLp.toLp_sub] at h
    change
      ‖(approximation n).toLp - target.toLp‖ ^ 2 =
        ∫ z,
          ((approximation n).process z.2 z.1 - target.process z.2 z.1) ^ 2
          ∂processTimeMeasure mu T at h
    simpa only [approximation, target, toProgressiveL2_process,
      stoppedProgressiveL2_process] using h
  have hsquares :
      Tendsto
        (fun n => ‖(approximation n).toLp - target.toLp‖ ^ 2)
        atTop (𝓝 0) := by
    refine Filter.tendsto_congr'
      (Filter.Eventually.of_forall fun n => hnormSq n) |>.mpr ?_
    exact tendsto_integral_sq_stopRefinedDyadic_sub eta tau htau htauT
  have hnorms :
      Tendsto
        (fun n => ‖(approximation n).toLp - target.toLp‖)
        atTop (𝓝 0) := by
    have hsqrt := Real.continuous_sqrt.continuousAt.tendsto.comp hsquares
    change Tendsto
-- Source excerpt truncated; follow the exact source link.

AutoSamplingTheory/TechnicalLemmas/StochasticProcesses/RandomStoppingL2Convergence.lean:143published source at 7bcd37294df1

Excerpt truncated; the exact source link is authoritative.