Theorems · Theorem · measure theory
MeasureTheory.lintegral_withDensity_le_lintegral_mul
∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f : α → ENNReal},
Measurable f → ∀ (g : α → ENNReal), ∫⁻ (a : α), g a ∂μ.withDensity f ≤ ∫⁻ (a : α), (f * g) a ∂μ- Cited by
- 1 results in Mathlib
- Foundations
- Depth 205 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites18
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- MeasurableSpacestatement and proof · cited by 13,106
- MeasureTheory.Measurestatement and proof · cited by 10,939
- ENNRealstatement and proof · cited by 9,879
- iSupproof · cited by 2,415
- le_reflproof · cited by 2,061
- le_rflproof · cited by 1,558
- Measurablestatement and proof · cited by 1,499
- MeasureTheory.lintegralstatement and proof · cited by 1,152
- le_imp_le_of_le_of_leproof · cited by 576
- mul_le_mul'proof · cited by 274
- MeasureTheory.Measure.withDensitystatement and proof · cited by 265
- iSup_leproof · cited by 190
Cited by1
Results whose statement or proof uses this declaration.
- MeasureTheory.lintegral_withDensity_eq_lintegral_mul_non_measurableproof · cited by 2