test module

`Tests.ProgressiveL2Truncation`

0 named declarations scanned from Tests/ProgressiveL2Truncation.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Truncation

Imported by

Tests

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

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

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2Truncation

namespace AutoSamplingTheory.Tests.ProgressiveL2Truncation

open TechnicalLemmas.StochasticProcesses.ProgressiveL2Truncation

#check clipProcess
#check clipProcess_stronglyProgressive
#check clipProcess_memLp
#check clipped
#check clipped_abs_le
#check tendsto_clipped_toLp

end AutoSamplingTheory.Tests.ProgressiveL2Truncation