English
If f is a.e.-measurable, the equality for the lintegral over μ.withDensity f and μ holds with AEMeasurable g.
Русский
Если f измерима почти совсем, равенство линеграла над μ.withDensity f и μ сохраняется для AEMeasurable g.
LaTeX
$$∫⁻ a, g a d(μ.withDensity f) = ∫⁻ a, (f * g) a dμ$$
Lean4
/-- The Lebesgue integral of `g` with respect to the measure `μ.withDensity f` coincides with
the integral of `f * g`. This version assumes that `g` is almost everywhere measurable. For a
version without conditions on `g` but requiring that `f` is almost everywhere finite, see
`lintegral_withDensity_eq_lintegral_mul_non_measurable` -/
theorem lintegral_withDensity_eq_lintegral_mul₀' {μ : Measure α} {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) {g : α → ℝ≥0∞}
(hg : AEMeasurable g (μ.withDensity f)) : ∫⁻ a, g a ∂μ.withDensity f = ∫⁻ a, (f * g) a ∂μ :=
by
let f' := hf.mk f
have : μ.withDensity f = μ.withDensity f' := withDensity_congr_ae hf.ae_eq_mk
rw [this] at hg ⊢
let g' := hg.mk g
calc
∫⁻ a, g a ∂μ.withDensity f' = ∫⁻ a, g' a ∂μ.withDensity f' := lintegral_congr_ae hg.ae_eq_mk
_ = ∫⁻ a, (f' * g') a ∂μ := (lintegral_withDensity_eq_lintegral_mul _ hf.measurable_mk hg.measurable_mk)
_ = ∫⁻ a, (f' * g) a ∂μ := by
apply lintegral_congr_ae
apply ae_of_ae_restrict_of_ae_restrict_compl {x | f' x ≠ 0}
· have Z := hg.ae_eq_mk
rw [EventuallyEq, ae_withDensity_iff_ae_restrict hf.measurable_mk] at Z
filter_upwards [Z]
intro x hx
simp only [g', hx, Pi.mul_apply]
· have M : MeasurableSet {x : α | f' x ≠ 0}ᶜ := (hf.measurable_mk (measurableSet_singleton 0).compl).compl
filter_upwards [ae_restrict_mem M]
intro x hx
simp only [Classical.not_not, mem_setOf_eq, mem_compl_iff] at hx
simp only [hx, zero_mul, Pi.mul_apply]
_ = ∫⁻ a : α, (f * g) a ∂μ := by
apply lintegral_congr_ae
filter_upwards [hf.ae_eq_mk]
intro x hx
simp only [f', hx, Pi.mul_apply]
