Theorems · Theorem · probability
MeasureTheory.StronglyAdapted.measurable_upcrossings
∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {a b : ℝ} {f : ℕ → Ω → ℝ} {ℱ : MeasureTheory.Filtration ℕ m0},
MeasureTheory.StronglyAdapted ℱ f → a < b → Measurable (MeasureTheory.upcrossings a b f)- Cited by
- 1 results in Mathlib
- Foundations
- Depth 168 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites11
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
- ENNRealstatement · cited by 9,879
- Measurablestatement · cited by 1,499
- MeasureTheory.Filtrationstatement and proof · cited by 425
- Measurable.compproof · cited by 234
- MeasureTheory.StronglyAdaptedstatement and proof · cited by 81
- Measurable.iSupproof · cited by 14
- MeasureTheory.upcrossingsstatement · cited by 9
- measurable_from_topproof · cited by 5
- MeasureTheory.StronglyAdapted.measurable_upcrossingsBeforeproof · cited by 3
Cited by1
Results whose statement or proof uses this declaration.
- MeasureTheory.Submartingale.upcrossings_ae_lt_top'proof · cited by 1