test module

`Tests.ElementaryItoIsometry`

0 named declarations scanned from Tests/ElementaryItoIsometry.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoIsometry

Imported by

Tests

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

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

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoIsometry

namespace AutoSamplingTheory.Tests.ElementaryItoIsometry

open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses
open ElementaryItoIsometry

#check TimeMeasure.upTo_Ioc
#check brownianIncrement
#check weightedIncrement
#check integral_weightedIncrement_sq
#check integral_weightedIncrement_mul_eq_zero
#check chewi_display_1_1_5
#check processL2Energy_value
#check chewi_display_1_1_6

end AutoSamplingTheory.Tests.ElementaryItoIsometry