test module

`Tests.ElementaryItoEmbedding`

0 named declarations scanned from Tests/ElementaryItoEmbedding.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoEmbedding

Imported by

Tests

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

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

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ElementaryItoEmbedding

namespace AutoSamplingTheory.Tests.ElementaryItoEmbedding

open TechnicalLemmas.StochasticProcesses
open ElementaryItoEmbedding

#check processFunction_stronglyMeasurable
#check value_stronglyProgressive
#check valueBound
#check abs_value_le_valueBound
#check value_memLp_two
#check toProgressiveL2
#check toLp_add
#check toLp_sub
#check toLp_smul

end AutoSamplingTheory.Tests.ElementaryItoEmbedding