test module

`Tests.SampledElementaryApproximation`

0 named declarations scanned from Tests/SampledElementaryApproximation.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.SampledElementaryApproximation

Imported by

Tests

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

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

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.SampledElementaryApproximation

namespace AutoSamplingTheory.Tests.SampledElementaryApproximation

open TechnicalLemmas.StochasticProcesses.SampledElementaryApproximation

#check regularGridTimes
#check regularGridTimes_strictMono
#check sampledClipped
#check sampledClipped_coeff_abs_le
#check dyadicMesh
#check dyadicMesh_pos
#check sampledClippedDyadic
#check sampledClippedDyadic_last_time

end AutoSamplingTheory.Tests.SampledElementaryApproximation