Theorems · Theorem · probability

MeasureTheory.Filtration.memLp_limitProcess_of_eLpNorm_bdd

∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {R : NNReal} {p : ENNReal} {F : Type u_5}
  [inst : NormedAddCommGroup F] {ℱ : MeasureTheory.Filtration ℕ m} {f : ℕ → Ω → F},
  (∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) →
    (∀ (n : ℕ), MeasureTheory.eLpNorm (f n) p μ ≤ ↑R) →
      MeasureTheory.MemLp (MeasureTheory.Filtration.limitProcess f ℱ μ) p μ

Defined in: Mathlib.Probability.Process.Filtration
Cited by: 4 results in Mathlib
Foundations: Depth 212 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: NormedAddCommGroup

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites31

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

NormedAddCommGroupstatement and proof · cited by 15,752
MeasurableSpacestatement and proof · cited by 13,106
MeasureTheory.Measurestatement and proof · cited by 10,939
ENNRealstatement and proof · cited by 9,879
Set.ofPredproof · cited by 6,101
nhdsproof · cited by 5,554
Set.rangeproof · cited by 4,705
NNRealstatement and proof · cited by 4,310
Filter.Tendstoproof · cited by 3,814
LE.le.transproof · cited by 3,151
Filter.Eventuallyproof · cited by 3,134
Filter.atTopproof · cited by 2,405

Cited by4

Results whose statement or proof uses this declaration.

MeasureTheory.Submartingale.tendsto_eLpNorm_one_limitProcessproof · cited by 2
MeasureTheory.Integrable.tendsto_ae_condExpproof · cited by 2
MeasureTheory.Martingale.ae_eq_condExp_limitProcessproof · cited by 1
MeasureTheory.Submartingale.memLp_limitProcessproof · cited by 1