test module

`Tests.GlobalLocalProgressiveL2`

0 named declarations scanned from Tests/GlobalLocalProgressiveL2.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalLocalProgressiveL2

Imported by

Tests

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

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

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.GlobalLocalProgressiveL2

namespace AutoSamplingTheory.Tests.GlobalLocalProgressiveL2

open MeasureTheory
open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses
open ElementaryItoIntegral GlobalLocalProgressiveL2 LocalProgressiveL2
open scoped NNReal

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

#check GlobalLocalProgressiveL2Integrand
#check GlobalLocalProgressiveL2Integrand.onHorizon
#check GlobalLocalProgressiveL2Integrand.onHorizon_process
#check GlobalLocalProgressiveL2Integrand.chewi_global_condition_1_1_10

example (eta : GlobalLocalProgressiveL2Integrand filtration mu) (T : ℝ≥0) :
    LocalProgressiveL2Integrand filtration mu T :=
  eta.onHorizon T

example (eta : GlobalLocalProgressiveL2Integrand filtration mu) :
    ∀ T : ℝ≥0, IsLocallySquareIntegrableOn eta.process mu T :=
  eta.chewi_global_condition_1_1_10

end AutoSamplingTheory.Tests.GlobalLocalProgressiveL2