withDensityᵥ_neg — Mathlib

English

A signed measure s is absolutely continuous with respect to μ if and only if μ.withDensityᵥ (s.rnDeriv μ) = s.

Русский

Знаковая мера s абсолютно непрерывна по отношению к μ если и только если μ.withDensityᵥ (s.rnDeriv μ) = s.

LaTeX

$$$ s ≪ᵥ μ.toENNRealVectorMeasure \\iff μ.withDensityᵥ (s.rnDeriv μ) = s $$$

Lean4

@[simp]
theorem withDensityᵥ_neg : μ.withDensityᵥ (-f) = -μ.withDensityᵥ f :=
  by
  by_cases hf : Integrable f μ
  · ext1 i hi
    rw [VectorMeasure.neg_apply, withDensityᵥ_apply hf hi, ← integral_neg, withDensityᵥ_apply hf.neg hi]
    simp only [Pi.neg_apply]
  · rw [withDensityᵥ, withDensityᵥ, dif_neg hf, dif_neg, neg_zero]
    rwa [integrable_neg_iff]

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