Theorems · Theorem · probability

MeasureTheory.martingale_const_fun

∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : OrderBot ι] (ℱ : MeasureTheory.Filtration ι m0)
  (μ : MeasureTheory.Measure Ω) [MeasureTheory.SigmaFiniteFiltration μ ℱ] {f : Ω → E},
  MeasureTheory.StronglyMeasurable f → MeasureTheory.Integrable f μ → MeasureTheory.Martingale (fun x => f) ℱ μ

Defined in: Mathlib.Probability.Martingale.Basic
Cited by: 1 results in Mathlib
Foundations: Depth 297 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Preorder NormedAddCommGroup NormedSpace OrderBot MeasureTheory.SigmaFiniteFiltration

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites22

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
NormedAddCommGroupstatement and proof · cited by 15,752
MeasurableSpacestatement and proof · cited by 13,106
NormedSpacestatement and proof · cited by 12,499
MeasureTheory.Measurestatement and proof · cited by 10,939
Preorderstatement and proof · cited by 7,952
Bot.botstatement · cited by 4,720
MeasureTheory.aeproof · cited by 2,352
Filter.EventuallyEqproof · cited by 1,912
MeasureTheory.Integrablestatement and proof · cited by 1,367
OrderBotstatement and proof · cited by 1,055
MeasureTheory.Filtrationstatement and proof · cited by 425

Cited by1

Results whose statement or proof uses this declaration.

MeasureTheory.Submartingale.bddAbove_iff_exists_tendstoproof · cited by 1