English
For a measurable f: X → ℝ≥0 and g: X → E integrable w.r.t. μ, ∫ g d(μ.withDensity f) = ∫ f·g dμ with appropriate reductions when needed.
Русский
Для измеримой плотности f: X → ℝ≥0 и интегрируемой g: X → E по μ, имеем ∫ g d(μ.withDensity f) = ∫ f·g dμ (с необходимыми сведениями).
LaTeX
$$$\\int_X g(x) \\,d(\\mu.withDensity f) = \\int_X f(x)\\,g(x) \\,d\\mu$$$
Lean4
theorem integral_withDensity_eq_integral_smul₀ {f : X → ℝ≥0} (hf : AEMeasurable f μ) (g : X → E) :
∫ x, g x ∂μ.withDensity (fun x => f x) = ∫ x, f x • g x ∂μ :=
by
let f' := hf.mk _
calc
∫ x, g x ∂μ.withDensity (fun x => f x) = ∫ x, g x ∂μ.withDensity fun x => f' x :=
by
congr 1
apply withDensity_congr_ae
filter_upwards [hf.ae_eq_mk] with x hx
rw [hx]
_ = ∫ x, f' x • g x ∂μ := (integral_withDensity_eq_integral_smul hf.measurable_mk _)
_ = ∫ x, f x • g x ∂μ := by
apply integral_congr_ae
filter_upwards [hf.ae_eq_mk] with x hx
rw [hx]
