haveLebesgueDecomposition_neg — Mathlib

English

If s has a Lebesgue decomposition with respect to μ, then (−s) also has one, with the positive/negative parts swapped.

Русский

Если у s есть разложение Лебега относительно μ, то и −s обладает разложением, при этом части положительная и отрицательная меняются местами.

LaTeX

$$$(-s).HaveLebesgueDecomposition\mu$, with posPart = s.negPart and negPart = s.posPart$$

Lean4

instance haveLebesgueDecomposition_neg (s : SignedMeasure α) (μ : Measure α) [s.HaveLebesgueDecomposition μ] :
    (-s).HaveLebesgueDecomposition μ
    where
  posPart := by
    rw [toJordanDecomposition_neg, JordanDecomposition.neg_posPart]
    infer_instance
  negPart := by
    rw [toJordanDecomposition_neg, JordanDecomposition.neg_negPart]
    infer_instance

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