English
For a real-valued integrable f, the vector density μ.withDensityᵥ f equals the difference of signed measures built from the positive and negative parts via ENNReal.ofReal.
Русский
Для действительной интегрируемой f векторная плотность μ.withDensityᵥ f равна разности знаковых мер, построенных по положительной и отрицательной частям через ENNReal.ofReal.
LaTeX
$$$\mu.withDensityᵥ f = \text{toSignedMeasure}(\mu.withDensity (x \mapsto ENNReal.ofReal(f(x)))) - \text{toSignedMeasure}(\mu.withDensity (x \mapsto ENNReal.ofReal(-f(x))))$$$
Lean4
theorem withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part {f : α → ℝ} (hfi : Integrable f μ) :
μ.withDensityᵥ f =
@toSignedMeasure α _ (μ.withDensity fun x => ENNReal.ofReal <| f x) (isFiniteMeasure_withDensity_ofReal hfi.2) -
@toSignedMeasure α _ (μ.withDensity fun x => ENNReal.ofReal <| -f x)
(isFiniteMeasure_withDensity_ofReal hfi.neg.2) :=
by
haveI := isFiniteMeasure_withDensity_ofReal hfi.2
haveI := isFiniteMeasure_withDensity_ofReal hfi.neg.2
ext i hi
rw [withDensityᵥ_apply hfi hi, integral_eq_lintegral_pos_part_sub_lintegral_neg_part hfi.integrableOn,
VectorMeasure.sub_apply, toSignedMeasure_apply_measurable hi, toSignedMeasure_apply_measurable hi, measureReal_def,
measureReal_def, withDensity_apply _ hi, withDensity_apply _ hi]