test module

`Tests.StoppingGraphNull`

0 named declarations scanned from Tests/StoppingGraphNull.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.StoppingGraphNull

Imported by

Tests

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

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

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.StoppingGraphNull

namespace AutoSamplingTheory.Tests.StoppingGraphNull

open MeasureTheory
open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses
open StoppingGraphNull
open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.StoppingTime
open scoped NNReal

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

#check stoppingGraph
#check measurableSet_stoppingGraph
#check timeSection_stoppingGraph_zero
#check processTimeMeasure_stoppingGraph_zero
#check ae_notMem_stoppingGraph
#check ae_time_ne_stoppingTime

example (tau : Omega → WithTop ℝ≥0)
    (htau : IsChewiStoppingTime filtration tau) :
    ElementaryItoIntegral.processTimeMeasure mu T (stoppingGraph tau) = 0 :=
  processTimeMeasure_stoppingGraph_zero tau htau T

end AutoSamplingTheory.Tests.StoppingGraphNull