test module

`Tests.ProgressiveL2Density`

0 named declarations scanned from Tests/ProgressiveL2Density.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Density

Imported by

Tests

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

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

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Density

open AutoSamplingTheory TechnicalLemmas StochasticProcesses

#check ProgressiveL2Density.fastTolerance
#check ProgressiveL2Density.summable_fastTolerance
#check ProgressiveL2Density.strictSelection
#check ProgressiveL2Density.strictMono_strictSelection
#check ProgressiveL2Density.truncationIndex
#check ProgressiveL2Density.dyadicLevel
#check ProgressiveL2Density.DyadicElementaryProcess
#check ProgressiveL2Density.canonicalElementaryApprox
#check ProgressiveL2Density.progressiveL2_elementary_dense