test module

`Tests.DyadicGlobalHorizon`

0 named declarations scanned from Tests/DyadicGlobalHorizon.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.DyadicGlobalHorizon

Imported by

Tests

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

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

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.DyadicGlobalHorizon

namespace AutoSamplingTheory.Tests.DyadicGlobalHorizon

open MeasureTheory
open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses
open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.DyadicGlobalHorizon
open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalLocalProgressiveL2
open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2
open scoped NNReal Topology

#check dyadicGlobalIndex
#check dyadicHorizon
#check dyadicGlobalIndex_add_one
#check integerHorizon_dyadicGlobalIndex
#check dyadicGlobalIndex_mono
#check tendsto_dyadicGlobalIndex_atTop
#check dyadicGlobalLocalizingTime
#check dyadicGlobalLocalizingTime_isChewiStoppingTime
#check dyadicGlobalLocalizingTime_mono
#check dyadicGlobalLocalizingTime_le_horizon
#check dyadicGlobalLocalizingTime_tendsto_top_ae

end AutoSamplingTheory.Tests.DyadicGlobalHorizon