withDensityᵥ_add — Mathlib

English

If f and g are integrable, then μ.withDensityᵥ (f + g) equals μ.withDensityᵥ f plus μ.withDensityᵥ g.

Русский

Если f и g интегрируемы, тогда μ.withDensityᵥ (f + g) равен сумме μ.withDensityᵥ f и μ.withDensityᵥ g.

LaTeX

$$$ μ.withDensityᵥ (f + g) = μ.withDensityᵥ f + μ.withDensityᵥ g $$$

Lean4

@[simp]
theorem withDensityᵥ_add (hf : Integrable f μ) (hg : Integrable g μ) :
    μ.withDensityᵥ (f + g) = μ.withDensityᵥ f + μ.withDensityᵥ g :=
  by
  ext1 i hi
  rw [withDensityᵥ_apply (hf.add hg) hi, VectorMeasure.add_apply, withDensityᵥ_apply hf hi, withDensityᵥ_apply hg hi]
  simp_rw [Pi.add_apply]
  rw [integral_add]
  · exact hf.integrableOn
  · exact hg.integrableOn

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