test module

`Tests.ElementaryItoL2`

0 named declarations scanned from Tests/ElementaryItoL2.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoL2

Imported by

Tests

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

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

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoL2

namespace AutoSamplingTheory.Tests.ElementaryItoL2

open TechnicalLemmas.StochasticProcesses
open ElementaryItoL2

#check norm_sq_toLp_eq_integral_sq
#check elementaryItoIntegral_memLp_two
#check elementaryItoTerminalToLp
#check elementaryProcessToLp
#check norm_sq_elementaryItoTerminalToLp
#check norm_elementaryItoTerminalToLp
#check elementaryItoTerminalToLp_add
#check elementaryProcessToLp_add
#check inner_elementaryItoTerminalToLp
#check elementaryItoTerminalToLp_sub
#check elementaryProcessToLp_sub
#check norm_elementaryItoTerminalToLp_sub

end AutoSamplingTheory.Tests.ElementaryItoL2