Rightward Convergence of Dyadic Sampling Points

This vendored convergence theorem concerns dyadic sampling of a time point.

Let $T>0$ and let $t\in[0,T]$. For each $n$, let dyadicIndex T t n select the dyadic point at level $n$ lying at or to the right of $t$. Then

as $n\to\infty$, with convergence in the neighborhood filter of $t$ restricted to $[t,\infty)$.

The result supplies the time approximation needed to pass from dyadic samples to right-continuous paths.

Original Lean declaration header

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

theorem tendsto_dyadicTime_dyadicIndex {T t : ℝ} (hT : 0 < T) (ht : 0 ≤ t) (htT : t ≤ T) :
    Filter.Tendsto (fun n => dyadicTime T n (dyadicIndex T t n)) Filter.atTop
      (nhdsWithin t (Set.Ici t))

Module navigation

Module: LevyStochCalc/Probability/DoobContinuous.

Previous: enorm_dyadicRunMax · Next: iSup_enorm_eq_iSup_dyadicRunMax.

Source excerpt, lines 187–189 · Frozen source 408915f.