test module

`Tests.ChewiDefinition1_1_17`

0 named declarations scanned from Tests/ChewiDefinition1_1_17.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ChewiDefinition1_1_17

Imported by

No local reverse import.

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

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

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ChewiDefinition1_1_17

namespace AutoSamplingTheory.Tests.ChewiDefinition1_1_17

open MeasureTheory
open scoped NNReal RealInnerProductSpace

#check TechnicalLemmas.StochasticProcesses.ChewiDefinition1_1_17.stochasticIntegral
#check TechnicalLemmas.StochasticProcesses.ChewiDefinition1_1_17.stochasticIntegral_coordinate
#check TechnicalLemmas.StochasticProcesses.ChewiDefinition1_1_17.drift_integral_coordinate
#check TechnicalLemmas.StochasticProcesses.ChewiDefinition1_1_17.definition_1_1_17_vector_display
#check TechnicalLemmas.StochasticProcesses.ChewiDefinition1_1_17.chewi_definition_1_1_17

end AutoSamplingTheory.Tests.ChewiDefinition1_1_17