Theorems · Theorem · measure theory

MeasureTheory.SignedMeasure.toJordanDecomposition_eq_of_eq_add_withDensity

∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : MeasureTheory.SignedMeasure α} {f : α → ℝ}
  (hf : Measurable f) (hfi : MeasureTheory.Integrable f μ)
  (htμ : MeasureTheory.VectorMeasure.MutuallySingular t μ.toENNRealVectorMeasure),
  s = t + μ.withDensityᵥ f →
    s.toJordanDecomposition =
      { posPart := t.toJordanDecomposition.posPart + μ.withDensity fun x => ENNReal.ofReal (f x),
        negPart := t.toJordanDecomposition.negPart + μ.withDensity fun x => ENNReal.ofReal (-f x), posPart_finite := ⋯,
        negPart_finite := ⋯, mutuallySingular := ⋯ }

Defined in

Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue

Cited by

0 results in Mathlib

Foundations

Depth 262 from the axioms · uses propext, Classical.choice, Quot.sound