Theorems · Theorem · measure theory
MeasureTheory.lintegral_withDensity_eq_lintegral_mul_non_measurable
∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) {f : α → ENNReal},
Measurable f →
(∀ᵐ (x : α) ∂μ, f x < ⊤) → ∀ (g : α → ENNReal), ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ- Cited by
- 2 results in Mathlib
- Foundations
- Depth 206 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites34
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
- Top.topstatement and proof · cited by 9,680
- Filter.Eventuallystatement and proof · cited by 3,134
- one_mulproof · cited by 2,841
- iSupproof · cited by 2,415
- MeasureTheory.aestatement and proof · cited by 2,352
- mul_commproof · cited by 2,262
- MulZeroClass.mul_zeroproof · cited by 2,091
- le_antisymmproof · cited by 2,068
- Filter.univ_mem'proof · cited by 1,672
Cited by2
Results whose statement or proof uses this declaration.
- MeasureTheory.lintegral_withDensity_eq_lintegral_mul_non_measurable₀proof · cited by 2