test module

`Tests.Martingale`

0 named declarations scanned from Tests/Martingale.lean.

Imports

AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Martingale

Imported by

Tests

Placeholder scan

0 declaration(s) flagged

Gate status

Partial

Declarations

This aggregator contains no named declarations.

Complete Lean source

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

Download module (.lean)

import AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Martingale

namespace AutoSamplingTheory.Tests.Martingale

open MeasureTheory
open AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Martingale
open scoped NNReal

#check AutoSamplingTheory.TechnicalLemmas.StochasticProcesses.Martingale.IsChewiMartingale

example {Ω : Type*} {m : MeasurableSpace Ω}
    (filtration : Filtration ℝ≥0 m) (μ : Measure Ω) [IsFiniteMeasure μ]
    (value : ℝ) :
    IsChewiMartingale (fun _ : ℝ≥0 => fun _ : Ω => value) filtration μ :=
  isChewiMartingale_const filtration μ value

end AutoSamplingTheory.Tests.Martingale