English
Given a measurable f≥0 and a function g, integrability with density μ.withDensity f is equivalent to integrability of f·g with respect to μ.
Русский
При заданной измеримой f≥0 и функции g, интегрируемость по плотности μ.withDensity f равносильна интегрируемости по μ функции f·g.
LaTeX
$$Integrable g (μ.withDensity f) ↔ Integrable (f · g) μ$$
Lean4
theorem integrable_withDensity_iff_integrable_coe_smul {f : α → ℝ≥0} (hf : Measurable f) {g : α → E} :
Integrable g (μ.withDensity fun x => f x) ↔ Integrable (fun x => (f x : ℝ) • g x) μ :=
by
by_cases H : AEStronglyMeasurable (fun x : α => (f x : ℝ) • g x) μ
· simp only [Integrable, aestronglyMeasurable_withDensity_iff hf, hasFiniteIntegral_iff_enorm, H, true_and]
rw [lintegral_withDensity_eq_lintegral_mul₀' hf.coe_nnreal_ennreal.aemeasurable]
· simp [enorm_smul]
· simpa [aemeasurable_withDensity_ennreal_iff hf, enorm_smul] using H.enorm
· simp only [Integrable, aestronglyMeasurable_withDensity_iff hf, H, false_and]
