BrownianQuadraticVariationL2: mathematical reading route

The proof packages the Gaussian fourth-moment calculation into a one-cell variance, transports independence through the centered-square map, and invokes finite-sum variance additivity.

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 integral_quadraticVariationError_sq
    (hB : IsPreBrownianReal B mu)
    {n : ℕ} {times : Fin (n + 1) → ℝ≥0}
    (hmono : Monotone times) :
    ∫ omega, (quadraticVariationError B times omega) ^ 2 ∂mu =
      2 * ∑ i : Fin n,
        (((times i.succ - times i.castSucc : ℝ≥0) : ℝ) ^ 2) := by
  let _ : IsProbabilityMeasure mu := hB.isGaussianProcess.isProbabilityMeasure
  let Y : Fin n → Omega → ℝ := fun i => centeredSquaredIncrement B times i
  have hYmem : ∀ i, MemLp (Y i) 2 mu := fun i => by
    change MemLp
      (fun omega =>
        (B (times i.succ) omega - B (times i.castSucc) omega) ^ 2 -
          ((times i.succ - times i.castSucc : ℝ≥0) : ℝ)) 2 mu
    simpa only using
      centered_increment_sq_memLp_two hB _ _
  have hYind : Set.Pairwise (↑(Finset.univ : Finset (Fin n)) : Set (Fin n))
      (fun i j => Y i ⟂ᵢ[mu] Y j) := by
    intro i _ j _ hij
    exact (iIndepFun_centeredSquaredIncrement hB hmono).indepFun hij
  have hvar := ProbabilityTheory.IndepFun.variance_sum
    (s := Finset.univ) (X := Y) (fun i _ => hYmem i) hYind
  have hsumMem : MemLp (∑ i : Fin n, Y i) 2 mu :=
    memLp_finsetSum' Finset.univ (fun i _ => hYmem i)
  have hmean : ∫ omega, (∑ i : Fin n, Y i) omega ∂mu = 0 := by
    calc
      ∫ omega, (∑ i : Fin n, Y i) omega ∂mu =
          ∫ omega, ∑ i ∈ (Finset.univ : Finset (Fin n)), Y i omega ∂mu := by
            congr 1
            funext omega
            simp only [Finset.sum_apply]
      _ = ∑ i ∈ (Finset.univ : Finset (Fin n)), ∫ omega, Y i omega ∂mu := by
        rw [integral_finsetSum]
        intro i _
        exact (hYmem i).integrable (by norm_num)
      _ = 0 := by
        apply Finset.sum_eq_zero
        intro i _
        simpa [Y, centeredSquaredIncrement] using
          integral_centered_increment_sq_eq_zero hB (grid_cell_le hmono i)
  rw [variance_of_integral_eq_zero hsumMem.aemeasurable hmean] at hvar
  change ∫ omega, (∑ i : Fin n, centeredSquaredIncrement B times i omega) ^ 2 ∂mu = _
  change ∫ omega, (∑ i : Fin n, Y i omega) ^ 2 ∂mu = _
  rw [show (∫ omega, (∑ i : Fin n, Y i omega) ^ 2 ∂mu) =
      ∑ i : Fin n, Var[Y i; mu] by
    simpa only [Finset.sum_apply] using hvar]
  rw [Finset.mul_sum]
  apply Finset.sum_congr rfl
  intro i _
  have hYiMean : ∫ omega, Y i omega ∂mu = 0 := by
    simpa [Y, centeredSquaredIncrement] using
      integral_centered_increment_sq_eq_zero hB (grid_cell_le hmono i)
  rw [variance_of_integral_eq_zero (hYmem i).aemeasurable hYiMean]
  simpa [Y, centeredSquaredIncrement] using
    integral_centered_increment_sq_sq hB (grid_cell_le hmono i)

Exact module and namespace context

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