English
For f≥0 measurable, Integrable g (μ.withDensity f) is equivalent to Integrable (f.toReal • g) μ.
Русский
Для измеримой f≥0, Integrable g (μ.withDensity f) эквивалентно Integrable (f.toReal • g) μ.
LaTeX
$$Integrable g (μ.withDensity (fun x => f x)) ↔ Integrable (fun x => (f x).toReal • g x) μ$$
Lean4
theorem integrable_withDensity_iff_integrable_coe_smul₀ {f : α → ℝ≥0} (hf : AEMeasurable f μ) {g : α → E} :
Integrable g (μ.withDensity fun x => f x) ↔ Integrable (fun x => (f x : ℝ) • g x) μ :=
calc
Integrable g (μ.withDensity fun x => f x) ↔ Integrable g (μ.withDensity fun x => (hf.mk f x : ℝ≥0)) :=
by
suffices (fun x => (f x : ℝ≥0∞)) =ᵐ[μ] (fun x => (hf.mk f x : ℝ≥0)) by rw [withDensity_congr_ae this]
filter_upwards [hf.ae_eq_mk] with x hx
simp [hx]
_ ↔ Integrable (fun x => ((hf.mk f x : ℝ≥0) : ℝ) • g x) μ :=
(integrable_withDensity_iff_integrable_coe_smul hf.measurable_mk)
_ ↔ Integrable (fun x => (f x : ℝ) • g x) μ :=
by
apply integrable_congr
filter_upwards [hf.ae_eq_mk] with x hx
simp [hx]
