test module

`Tests.BrownianMotion`

0 named declarations scanned from Tests/BrownianMotion.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BrownianMotion

Imported by

Tests

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

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

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BrownianMotion

namespace AutoSamplingTheory.Tests.BrownianMotion

#check AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BrownianMotion.projectedIncrementVariance
#check AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BrownianMotion.IsStandardBrownianMotion
#check AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BrownianMotion.IsBrownianMotionWithFiltration
#check AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BrownianMotion.IsBrownianMotionWithFiltration.indepFun_increment_of_stronglyMeasurable
#check AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BrownianMotion.IsBrownianMotionWithFiltration.condExp_increment_eq_zero
#check AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BrownianMotion.IsBrownianMotionWithFiltration.integral_increment_sq
#check AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.BrownianMotion.IsBrownianMotionWithFiltration.condExp_increment_sq

end AutoSamplingTheory.Tests.BrownianMotion