Theorems · Theorem · measure theory
MeasureTheory.Integrable.of_mem_Icc
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] (a b : ℝ)
{X : α → ℝ}, AEMeasurable X μ → (∀ᵐ (ω : α) ∂μ, X ω ∈ Set.Icc a b) → MeasureTheory.Integrable X μ- Cited by
- 4 results in Mathlib
- Foundations
- Depth 203 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites12
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Setstatement · cited by 53,352
- Realstatement and proof · cited by 25,697
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- Filter.Eventuallystatement and proof · cited by 3,134
- MeasureTheory.aestatement and proof · cited by 2,352
- Set.Iccstatement and proof · cited by 1,702
- MeasureTheory.Integrablestatement · cited by 1,367
- MeasureTheory.IsFiniteMeasurestatement and proof · cited by 1,078
- AEMeasurablestatement and proof · cited by 840
- AEMeasurable.aestronglyMeasurableproof · cited by 57
- MeasureTheory.HasFiniteIntegral.of_mem_Iccproof · cited by 1
Cited by4
Results whose statement or proof uses this declaration.
- ProbabilityTheory.integrable_exp_mul_of_mem_Iccproof · cited by 2
- IsOpen.measure_eq_biSup_integral_continuousproof · cited by 1
- ProbabilityTheory.hasSubgaussianMGF_of_mem_Iccproof · cited by 0
- ProbabilityTheory.integrable_exp_mul_of_leproof · cited by 0