test module

`Tests.GlobalStoppedL2Overlap`

0 named declarations scanned from Tests/GlobalStoppedL2Overlap.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalStoppedL2Overlap

Imported by

Tests

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

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

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalStoppedL2Overlap

namespace AutoSamplingTheory.Tests.GlobalStoppedL2Overlap

open MeasureTheory
open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses
open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.DyadicGlobalHorizon
open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalLocalProgressiveL2
open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalStoppedL2Overlap
open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalStoppedProgressiveL2
open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.ProgressiveL2
open scoped NNReal

variable {Omega : Type*} {m : MeasurableSpace Omega}
  {filtration : Filtration ℝ≥0 m} {mu : Measure Omega}

#check dyadicGlobalLocalizingTime_coe_le
#check stopped_globalStoppedIntegrand_eq
#check stop_globalStoppedProgressiveL2_process
#check stop_globalStopped_toLp_eq_extendByZero

example [IsProbabilityMeasure mu]
    (hUsual : SatisfiesUsualConditions filtration mu)
    (eta : GlobalLocalProgressiveL2Integrand filtration mu)
    {k ell : ℕ} (hkell : k ≤ ell) :
    (ProgressiveL2Stopping.stop (globalStoppedProgressiveL2 hUsual eta ell)
      (fun omega =>
        (dyadicGlobalLocalizingTime hUsual eta k omega : WithTop ℝ≥0))
      (dyadicGlobalLocalizingTime_isChewiStoppingTime hUsual eta k)).toLp =
      (ProgressiveL2HorizonExtension.extendByZero
        (globalStoppedProgressiveL2 hUsual eta k)
        (by
          unfold dyadicHorizon
          exact_mod_cast Nat.pow_le_pow_right (by decide : 0 < (2 : ℕ)) hkell)).toLp :=
  stop_globalStopped_toLp_eq_extendByZero hUsual eta hkell

end AutoSamplingTheory.Tests.GlobalStoppedL2Overlap