Theorems · Theorem · probability

MeasureTheory.StronglyAdapted.integrable_upcrossingsBefore

∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {a b : ℝ} {f : ℕ → Ω → ℝ} {N : ℕ}
  {ℱ : MeasureTheory.Filtration ℕ m0} [MeasureTheory.IsFiniteMeasure μ],
  MeasureTheory.StronglyAdapted ℱ f →
    a < b → MeasureTheory.Integrable (fun ω => ↑(MeasureTheory.upcrossingsBefore a b f N ω)) μ

Defined in: Mathlib.Probability.Martingale.Upcrossing
Cited by: 1 results in Mathlib
Foundations: Depth 203 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: MeasureTheory.IsFiniteMeasure

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites18

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
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
Filter.univ_mem'proof · cited by 1,672
MeasureTheory.Integrablestatement · cited by 1,367
MeasureTheory.IsFiniteMeasurestatement and proof · cited by 1,078
MeasureTheory.Filtrationstatement and proof · cited by 425
Measurable.compproof · cited by 234
Nat.cast_leproof · cited by 159
Real.norm_eq_absproof · cited by 88
MeasureTheory.StronglyAdaptedstatement and proof · cited by 81
Measurable.aestronglyMeasurableproof · cited by 59

Cited by1

Results whose statement or proof uses this declaration.

MeasureTheory.Submartingale.mul_lintegral_upcrossings_le_lintegral_pos_partproof · cited by 1