Documentation

Mathlib.MeasureTheory.Decomposition.Jordan

Jordan decomposition #

This file proves the existence and uniqueness of the Jordan decomposition for signed measures. The Jordan decomposition theorem states that, given a signed measure s, there exists a unique pair of mutually singular measures μ and ν, such that s = μ - ν.

The Jordan decomposition theorem for measures is a corollary of the Hahn decomposition theorem and is useful for the Lebesgue decomposition theorem.

Main definitions #

Main results #

Tags #

Jordan decomposition theorem

theorem MeasureTheory.JordanDecomposition.ext {α : Type u_3} :
∀ {inst : MeasurableSpace α} (x y : MeasureTheory.JordanDecomposition α), x.posPart = y.posPartx.negPart = y.negPartx = y
theorem MeasureTheory.JordanDecomposition.ext_iff {α : Type u_3} :
∀ {inst : MeasurableSpace α} (x y : MeasureTheory.JordanDecomposition α), x = y x.posPart = y.posPart x.negPart = y.negPart

A Jordan decomposition of a measurable space is a pair of mutually singular, finite measures.

Instances For
    theorem MeasureTheory.JordanDecomposition.mutuallySingular {α : Type u_3} [MeasurableSpace α] (self : MeasureTheory.JordanDecomposition α) :
    self.posPart.MutuallySingular self.negPart
    Equations
    Equations
    • MeasureTheory.JordanDecomposition.instInhabited = { default := 0 }
    Equations
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    @[simp]
    @[simp]
    theorem MeasureTheory.JordanDecomposition.real_smul_def {α : Type u_1} [MeasurableSpace α] (r : ) (j : MeasureTheory.JordanDecomposition α) :
    r j = if 0 r then r.toNNReal j else -((-r).toNNReal j)
    theorem MeasureTheory.JordanDecomposition.real_smul_neg {α : Type u_1} [MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) (r : ) (hr : r < 0) :
    r j = -((-r).toNNReal j)
    theorem MeasureTheory.JordanDecomposition.real_smul_posPart_nonneg {α : Type u_1} [MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) (r : ) (hr : 0 r) :
    (r j).posPart = r.toNNReal j.posPart
    theorem MeasureTheory.JordanDecomposition.real_smul_negPart_nonneg {α : Type u_1} [MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) (r : ) (hr : 0 r) :
    (r j).negPart = r.toNNReal j.negPart
    theorem MeasureTheory.JordanDecomposition.real_smul_posPart_neg {α : Type u_1} [MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) (r : ) (hr : r < 0) :
    (r j).posPart = (-r).toNNReal j.negPart
    theorem MeasureTheory.JordanDecomposition.real_smul_negPart_neg {α : Type u_1} [MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) (r : ) (hr : r < 0) :
    (r j).negPart = (-r).toNNReal j.posPart

    The signed measure associated with a Jordan decomposition.

    Equations
    • j.toSignedMeasure = j.posPart.toSignedMeasure - j.negPart.toSignedMeasure
    Instances For
      theorem MeasureTheory.JordanDecomposition.toSignedMeasure_neg {α : Type u_1} [MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) :
      (-j).toSignedMeasure = -j.toSignedMeasure
      theorem MeasureTheory.JordanDecomposition.toSignedMeasure_smul {α : Type u_1} [MeasurableSpace α] (j : MeasureTheory.JordanDecomposition α) (r : NNReal) :
      (r j).toSignedMeasure = r j.toSignedMeasure

      Given a signed measure s, s.toJordanDecomposition is the Jordan decomposition j, such that s = j.toSignedMeasure. This property is known as the Jordan decomposition theorem, and is shown by MeasureTheory.SignedMeasure.toSignedMeasure_toJordanDecomposition.

      Equations
      Instances For
        theorem MeasureTheory.SignedMeasure.toJordanDecomposition_spec {α : Type u_1} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) :
        ∃ (i : Set α) (hi₁ : MeasurableSet i) (hi₂ : MeasureTheory.VectorMeasure.restrict 0 i MeasureTheory.VectorMeasure.restrict s i) (hi₃ : MeasureTheory.VectorMeasure.restrict s i MeasureTheory.VectorMeasure.restrict 0 i), s.toJordanDecomposition.posPart = s.toMeasureOfZeroLE i hi₁ hi₂ s.toJordanDecomposition.negPart = s.toMeasureOfLEZero i hi₃
        @[simp]
        theorem MeasureTheory.SignedMeasure.toSignedMeasure_toJordanDecomposition {α : Type u_1} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) :
        s.toJordanDecomposition.toSignedMeasure = s

        The Jordan decomposition theorem: Given a signed measure s, there exists a pair of mutually singular measures μ and ν such that s = μ - ν. In this case, the measures μ and ν are given by s.toJordanDecomposition.posPart and s.toJordanDecomposition.negPart respectively.

        Note that we use MeasureTheory.JordanDecomposition.toSignedMeasure to represent the signed measure corresponding to s.toJordanDecomposition.posPart - s.toJordanDecomposition.negPart.

        theorem MeasureTheory.SignedMeasure.subset_positive_null_set {α : Type u_1} [MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {u : Set α} {v : Set α} {w : Set α} (hu : MeasurableSet u) (hv : MeasurableSet v) (hw : MeasurableSet w) (hsu : MeasureTheory.VectorMeasure.restrict 0 u MeasureTheory.VectorMeasure.restrict s u) (hw₁ : s w = 0) (hw₂ : w u) (hwt : v w) :
        s v = 0

        A subset v of a null-set w has zero measure if w is a subset of a positive set u.

        theorem MeasureTheory.SignedMeasure.subset_negative_null_set {α : Type u_1} [MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {u : Set α} {v : Set α} {w : Set α} (hu : MeasurableSet u) (hv : MeasurableSet v) (hw : MeasurableSet w) (hsu : MeasureTheory.VectorMeasure.restrict s u MeasureTheory.VectorMeasure.restrict 0 u) (hw₁ : s w = 0) (hw₂ : w u) (hwt : v w) :
        s v = 0

        A subset v of a null-set w has zero measure if w is a subset of a negative set u.

        If the symmetric difference of two positive sets is a null-set, then so are the differences between the two sets.

        If the symmetric difference of two negative sets is a null-set, then so are the differences between the two sets.

        theorem MeasureTheory.JordanDecomposition.toSignedMeasure_injective {α : Type u_1} [MeasurableSpace α] :
        Function.Injective MeasureTheory.JordanDecomposition.toSignedMeasure

        The Jordan decomposition of a signed measure is unique.

        @[simp]
        theorem MeasureTheory.SignedMeasure.toJordanDecomposition_neg {α : Type u_1} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) :
        (-s).toJordanDecomposition = -s.toJordanDecomposition
        theorem MeasureTheory.SignedMeasure.toJordanDecomposition_smul {α : Type u_1} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) (r : NNReal) :
        (r s).toJordanDecomposition = r s.toJordanDecomposition
        theorem MeasureTheory.SignedMeasure.toJordanDecomposition_smul_real {α : Type u_1} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) (r : ) :
        (r s).toJordanDecomposition = r s.toJordanDecomposition
        theorem MeasureTheory.SignedMeasure.toJordanDecomposition_eq {α : Type u_1} [MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {j : MeasureTheory.JordanDecomposition α} (h : s = j.toSignedMeasure) :
        s.toJordanDecomposition = j

        The total variation of a signed measure.

        Equations
        • s.totalVariation = s.toJordanDecomposition.posPart + s.toJordanDecomposition.negPart
        Instances For
          theorem MeasureTheory.SignedMeasure.totalVariation_neg {α : Type u_1} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) :
          (-s).totalVariation = s.totalVariation
          theorem MeasureTheory.SignedMeasure.null_of_totalVariation_zero {α : Type u_1} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) {i : Set α} (hs : s.totalVariation i = 0) :
          s i = 0
          theorem MeasureTheory.SignedMeasure.totalVariation_absolutelyContinuous_iff {α : Type u_1} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) :
          s.totalVariation.AbsolutelyContinuous μ s.toJordanDecomposition.posPart.AbsolutelyContinuous μ s.toJordanDecomposition.negPart.AbsolutelyContinuous μ
          theorem MeasureTheory.SignedMeasure.totalVariation_mutuallySingular_iff {α : Type u_1} [MeasurableSpace α] (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) :
          s.totalVariation.MutuallySingular μ s.toJordanDecomposition.posPart.MutuallySingular μ s.toJordanDecomposition.negPart.MutuallySingular μ