withDensityᵥ_eq_withDensity_pos_part_sub_withDensity_neg_part

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]

Похожие утверждения