Continuous Supremum from Dyadic Running Maxima

This vendored theorem identifies a continuous-time supremum with dyadic running maxima.

Let $T\geq0$, fix an outcome $\omega$, and suppose that the path $s\mapsto M_s(\omega)$ is right-continuous at every time. Then

This is the pathwise bridge from discrete dyadic maximal estimates to a continuous-time supremum estimate.

Formalization Note. The supremum over $[0,T]$ is represented by an iSup over the subtype Set.Icc 0 T.

Original Lean declaration header

Within namespace LevyStochCalc.Probability. Shown in its original module context. Proof omitted.

theorem iSup_enorm_eq_iSup_dyadicRunMax (hT : 0 ≤ T) {ω : Ω}
    (hcad : ∀ t : ℝ, Filter.Tendsto (fun s => M s ω) (nhdsWithin t (Set.Ioi t))
      (nhds (M t ω))) :
    (⨆ t : Set.Icc (0 : ℝ) T, (‖M (t : ℝ) ω‖₊ : ℝ≥0∞))
      = ⨆ n, (‖dyadicRunMax M T n ω‖₊ : ℝ≥0∞)

Module navigation

Module: LevyStochCalc/Probability/DoobContinuous.

Supporting theorems: enorm_dyadicRunMax, tendsto_dyadicTime_dyadicIndex.

Previous: tendsto_dyadicTime_dyadicIndex · Next: lintegral_sq_dyadicRunMax_le.

Source excerpt, lines 208–212 · Frozen source 408915f.