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