test module

`Tests.LaggedDyadicApproximation`

0 named declarations scanned from Tests/LaggedDyadicApproximation.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LaggedDyadicApproximation

Imported by

Tests

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

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

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.LaggedDyadicApproximation

open AutoSamplingTheory TechnicalLemmas StochasticProcesses

#check LaggedDyadicApproximation.clippedExtensionAt
#check LaggedDyadicApproximation.clippedExtensionAt_stronglyMeasurable
#check LaggedDyadicApproximation.clippedExtensionAt_abs_le
#check LaggedDyadicApproximation.laggedCellAverage
#check LaggedDyadicApproximation.laggedCellAverage_stronglyMeasurable
#check LaggedDyadicApproximation.laggedCellAverage_zero
#check LaggedDyadicApproximation.laggedCellAverage_abs_le
#check LaggedDyadicApproximation.dyadicLeftTime
#check LaggedDyadicApproximation.laggedDyadicCoeff
#check LaggedDyadicApproximation.laggedDyadicCoeff_stronglyMeasurable
#check LaggedDyadicApproximation.laggedDyadicCoeff_abs_le
#check LaggedDyadicApproximation.laggedDyadicApprox
#check LaggedDyadicApproximation.laggedDyadicApprox_times
#check LaggedDyadicApproximation.laggedDyadicApprox_coeff
#check LaggedDyadicApproximation.laggedDyadicApprox_last_time
#check LaggedDyadicApproximation.laggedDyadicApprox_isElementaryAdapted