Theorems · Theorem · probability
MeasureTheory.Integrable.uniformIntegrable_condExp_filtration
∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {μ : MeasureTheory.Measure Ω}
[MeasureTheory.IsFiniteMeasure μ] {f : MeasureTheory.Filtration ι m} {g : Ω → ℝ},
MeasureTheory.Integrable g μ → MeasureTheory.UniformIntegrable (fun i => μ[g | ↑f i]) 1 μGiven an integrable function g, the conditional expectations of g with respect to a
filtration is uniformly integrable.
- Defined in
- Mathlib.Probability.Process.Filtration
- Cited by
- 2 results in Mathlib
- Foundations
- Depth 314 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites13
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
- ENNRealstatement · cited by 9,879
- Preorderstatement and proof · cited by 7,952
- MeasureTheory.Integrablestatement and proof · cited by 1,367
- MeasureTheory.IsFiniteMeasurestatement and proof · cited by 1,078
- MeasureTheory.Filtrationstatement and proof · cited by 425
- MeasureTheory.condExpstatement · cited by 234
- MeasureTheory.Filtration.seqstatement · cited by 184
- MeasureTheory.Filtration.leproof · cited by 65
- MeasureTheory.UniformIntegrablestatement · cited by 30
Cited by2
Results whose statement or proof uses this declaration.
- MeasureTheory.Integrable.tendsto_ae_condExpproof · cited by 2
- MeasureTheory.Integrable.tendsto_eLpNorm_condExpproof · cited by 1