Extended Norm of the Dyadic Running Maximum

This vendored theorem identifies the extended norm of a sampled running maximum.

For a real-valued process $M_t(\omega)$, a horizon $T$, a level $n\in\mathbb N$, and an outcome $\omega$, the ENNReal norm of dyadicRunMax M T n ω equals the supremum over the $2^n+1$ dyadic partition points:

This provides the discrete supremum representation used in continuous-time maximal estimates.

Formalization Note. The supremum is an ENNReal supremum of the coerced nonnegative norms.

Original Lean declaration header

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

theorem enorm_dyadicRunMax (M : ℝ → Ω → ℝ) (T : ℝ) (n : ℕ) (ω : Ω) :
    (‖dyadicRunMax M T n ω‖₊ : ℝ≥0∞)
      = ⨆ k : Fin (2 ^ n + 1), (‖M (dyadicTime T n (k : ℕ)) ω‖₊ : ℝ≥0∞)

Module navigation

Module: LevyStochCalc/Probability/DoobContinuous.

Next: tendsto_dyadicTime_dyadicIndex.

Source excerpt, lines 111–113 · Frozen source 408915f.