Theorems · Definition · measure theory
MeasureTheory.lintegral
- #86 of the 100 theorems: Lebesgue Measure and Integration
{α : Type u_4} → {m : MeasurableSpace α} → MeasureTheory.Measure α → (α → ENNReal) → ENNRealThe lower Lebesgue integral of a function f with respect to a measure μ.
- Cited by
- 1,152 results in Mathlib
- Foundations
- Depth 174 from the axioms, rests on 4,592 definitions · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites3
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement · cited by 13,106
- MeasureTheory.Measurestatement · cited by 10,939
- ENNRealstatement · cited by 9,879
Cited by1,175
Results whose statement or proof uses this declaration.
- MeasureTheory.Measure.withDensityproof · cited by 265
- MeasureTheory.lintegral_conststatement and proof · cited by 123
- MeasureTheory.HasFiniteIntegralproof · cited by 120
- MeasureTheory.lintegral_congr_aestatement · cited by 95
- MeasureTheory.withDensity_applystatement · cited by 73
- MeasureTheory.eLpNorm'proof · cited by 73
- MeasureTheory.memLp_one_iff_integrableproof · cited by 73
- MeasureTheory.lintegral_monostatement · cited by 51
- MeasureTheory.lintegral_indicatorstatement · cited by 47
- MeasureTheory.laverageproof · cited by 44
- MeasureTheory.lintegral_mono_aestatement and proof · cited by 36
- MeasureTheory.lintegral_zero_measurestatement · cited by 34
Showing the 200 most cited of 1,175.