Dyadic scalar Brownian quadratic variation converges in mean square

The proof rewrites the exact finite-grid second moment as 2T times the dyadic mesh and passes to the known zero-mesh limit.

Braces mark parameters Lean can infer; square brackets request structures such as a measurable space or probability measure. Named hypotheses are mathematical premises, not facts established by this declaration. Section parameters are described in the mathematical hypotheses above; the module link retains their exact source context.

theorem tendsto_integral_dyadic_quadraticVariationError_sq
    (hB : IsPreBrownianReal B mu) (T : ℝ≥0) :
    Tendsto
      (fun level =>
        ∫ omega,
          (quadraticVariationError B
            (regularGridTimes (dyadicMesh T level) (2 ^ level)) omega) ^ 2 ∂mu)
      atTop (nhds 0) := by
  have hexact : ∀ level : ℕ,
      (∫ omega,
          (quadraticVariationError B
            (regularGridTimes (dyadicMesh T level) (2 ^ level)) omega) ^ 2 ∂mu) =
        2 * (T : ℝ) * ((dyadicMesh T level : ℝ≥0) : ℝ) := by
    intro level
    rw [integral_quadraticVariationError_sq hB
      (regularGridTimes_monotone
        (dyadicMesh T level) (2 ^ level))]
    rw [sum_dyadic_cellLengths_sq]
    ring
  have hlimit := (FiniteTimeGrid.dyadicMesh_tendsto_zero T).const_mul (2 * (T : ℝ))
  have hfun :
      (fun level =>
        ∫ omega,
          (quadraticVariationError B
            (regularGridTimes (dyadicMesh T level) (2 ^ level)) omega) ^ 2 ∂mu) =
        fun level => 2 * (T : ℝ) * ((dyadicMesh T level : ℝ≥0) : ℝ) := by
    funext level
    exact hexact level
  rw [hfun]
  simpa using hlimit

end BrownianQuadraticVariationL2
end StochasticProcesses
end TechnicalLemmas
end AutoSamplingTheory

Exact module and namespace context