test module

`Tests.BrownianQuadraticVariationL2`

0 named declarations scanned from Tests/BrownianQuadraticVariationL2.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BrownianQuadraticVariationL2

Imported by

Tests

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

Tests/BrownianQuadraticVariationL2.lean — full module with imports and context

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BrownianQuadraticVariationL2

/-! Focused ABI checks for the Brownian quadratic-variation `L²` packet. -/

#check AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BrownianQuadraticVariationL2.integral_quadraticVariationError_sq
#check AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BrownianQuadraticVariationL2.tendsto_integral_dyadic_quadraticVariationError_sq