Documentation

Mathlib.MeasureTheory.Measure.VectorMeasure

Vector valued measures #

This file defines vector valued measures, which are σ-additive functions from a set to an add monoid M such that it maps the empty set and non-measurable sets to zero. In the case that M = ℝ, we called the vector measure a signed measure and write SignedMeasure α. Similarly, when M = ℂ, we call the measure a complex measure and write ComplexMeasure α (defined in MeasureTheory/Measure/Complex).

Main definitions #

Notation #

Implementation notes #

We require all non-measurable sets to be mapped to zero in order for the extensionality lemma to only compare the underlying functions for measurable sets.

We use HasSum instead of tsum in the definition of vector measures in comparison to Measure since this provides summability.

Tags #

vector measure, signed measure, complex measure

structure MeasureTheory.VectorMeasure (α : Type u_3) [MeasurableSpace α] (M : Type u_4) [AddCommMonoid M] [TopologicalSpace M] :
Type (max u_3 u_4)

A vector measure on a measurable space α is a σ-additive M-valued function (for some M an add monoid) such that the empty set and non-measurable sets are mapped to zero.

Instances For
    theorem MeasureTheory.VectorMeasure.m_iUnion' {α : Type u_3} [MeasurableSpace α] {M : Type u_4} [AddCommMonoid M] [TopologicalSpace M] (self : MeasureTheory.VectorMeasure α M) ⦃f : Set α :
    (∀ (i : ), MeasurableSet (f i))Pairwise (Disjoint on f)HasSum (fun (i : ) => self (f i)) (self (⋃ (i : ), f i))
    @[reducible, inline]
    abbrev MeasureTheory.SignedMeasure (α : Type u_3) [MeasurableSpace α] :
    Type (max u_3 0)

    A SignedMeasure is an -vector measure.

    Equations
    Instances For
      Equations
      • MeasureTheory.VectorMeasure.instCoeFun = { coe := MeasureTheory.VectorMeasure.measureOf' }
      theorem MeasureTheory.VectorMeasure.m_iUnion {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : MeasureTheory.VectorMeasure α M) {f : Set α} (hf₁ : ∀ (i : ), MeasurableSet (f i)) (hf₂ : Pairwise (Disjoint on f)) :
      HasSum (fun (i : ) => v (f i)) (v (⋃ (i : ), f i))
      theorem MeasureTheory.VectorMeasure.coe_injective {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] :
      Function.Injective MeasureTheory.VectorMeasure.measureOf'
      theorem MeasureTheory.VectorMeasure.ext_iff' {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : MeasureTheory.VectorMeasure α M) (w : MeasureTheory.VectorMeasure α M) :
      v = w ∀ (i : Set α), v i = w i
      theorem MeasureTheory.VectorMeasure.ext_iff {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : MeasureTheory.VectorMeasure α M) (w : MeasureTheory.VectorMeasure α M) :
      v = w ∀ (i : Set α), MeasurableSet iv i = w i
      theorem MeasureTheory.VectorMeasure.ext {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {s : MeasureTheory.VectorMeasure α M} {t : MeasureTheory.VectorMeasure α M} (h : ∀ (i : Set α), MeasurableSet is i = t i) :
      s = t
      theorem MeasureTheory.VectorMeasure.hasSum_of_disjoint_iUnion {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [Countable β] {v : MeasureTheory.VectorMeasure α M} {f : βSet α} (hm : ∀ (i : β), MeasurableSet (f i)) (hd : Pairwise (Disjoint on f)) :
      HasSum (fun (i : β) => v (f i)) (v (⋃ (i : β), f i))
      theorem MeasureTheory.VectorMeasure.of_disjoint_iUnion {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [Countable β] {v : MeasureTheory.VectorMeasure α M} {f : βSet α} [T2Space M] (hm : ∀ (i : β), MeasurableSet (f i)) (hd : Pairwise (Disjoint on f)) :
      v (⋃ (i : β), f i) = ∑' (i : β), v (f i)
      @[deprecated MeasureTheory.VectorMeasure.of_disjoint_iUnion]
      theorem MeasureTheory.VectorMeasure.of_disjoint_iUnion_nat {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [T2Space M] (v : MeasureTheory.VectorMeasure α M) {f : Set α} (hf₁ : ∀ (i : ), MeasurableSet (f i)) (hf₂ : Pairwise (Disjoint on f)) :
      v (⋃ (i : ), f i) = ∑' (i : ), v (f i)
      theorem MeasureTheory.VectorMeasure.of_union {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {v : MeasureTheory.VectorMeasure α M} [T2Space M] {A : Set α} {B : Set α} (h : Disjoint A B) (hA : MeasurableSet A) (hB : MeasurableSet B) :
      v (A B) = v A + v B
      theorem MeasureTheory.VectorMeasure.of_add_of_diff {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {v : MeasureTheory.VectorMeasure α M} [T2Space M] {A : Set α} {B : Set α} (hA : MeasurableSet A) (hB : MeasurableSet B) (h : A B) :
      v A + v (B \ A) = v B
      theorem MeasureTheory.VectorMeasure.of_diff {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [AddCommGroup M] [TopologicalSpace M] [T2Space M] {v : MeasureTheory.VectorMeasure α M} {A : Set α} {B : Set α} (hA : MeasurableSet A) (hB : MeasurableSet B) (h : A B) :
      v (B \ A) = v B - v A
      theorem MeasureTheory.VectorMeasure.of_diff_of_diff_eq_zero {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {v : MeasureTheory.VectorMeasure α M} [T2Space M] {A : Set α} {B : Set α} (hA : MeasurableSet A) (hB : MeasurableSet B) (h' : v (B \ A) = 0) :
      v (A \ B) + v B = v A
      theorem MeasureTheory.VectorMeasure.of_iUnion_nonneg {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [Countable β] {f : βSet α} {M : Type u_4} [TopologicalSpace M] [OrderedAddCommMonoid M] [OrderClosedTopology M] {v : MeasureTheory.VectorMeasure α M} (hf₁ : ∀ (i : β), MeasurableSet (f i)) (hf₂ : Pairwise (Disjoint on f)) (hf₃ : ∀ (i : β), 0 v (f i)) :
      0 v (⋃ (i : β), f i)
      theorem MeasureTheory.VectorMeasure.of_iUnion_nonpos {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [Countable β] {f : βSet α} {M : Type u_4} [TopologicalSpace M] [OrderedAddCommMonoid M] [OrderClosedTopology M] {v : MeasureTheory.VectorMeasure α M} (hf₁ : ∀ (i : β), MeasurableSet (f i)) (hf₂ : Pairwise (Disjoint on f)) (hf₃ : ∀ (i : β), v (f i) 0) :
      v (⋃ (i : β), f i) 0
      theorem MeasureTheory.VectorMeasure.of_nonneg_disjoint_union_eq_zero {α : Type u_1} {m : MeasurableSpace α} {s : MeasureTheory.SignedMeasure α} {A : Set α} {B : Set α} (h : Disjoint A B) (hA₁ : MeasurableSet A) (hB₁ : MeasurableSet B) (hA₂ : 0 s A) (hB₂ : 0 s B) (hAB : s (A B) = 0) :
      s A = 0
      theorem MeasureTheory.VectorMeasure.of_nonpos_disjoint_union_eq_zero {α : Type u_1} {m : MeasurableSpace α} {s : MeasureTheory.SignedMeasure α} {A : Set α} {B : Set α} (h : Disjoint A B) (hA₁ : MeasurableSet A) (hB₁ : MeasurableSet B) (hA₂ : s A 0) (hB₂ : s B 0) (hAB : s (A B) = 0) :
      s A = 0

      Given a real number r and a signed measure s, smul r s is the signed measure corresponding to the function r • s.

      Equations
      Instances For
        Equations
        • MeasureTheory.VectorMeasure.instSMul = { smul := MeasureTheory.VectorMeasure.smul }
        @[simp]
        theorem MeasureTheory.VectorMeasure.coe_smul {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {R : Type u_4} [Semiring R] [DistribMulAction R M] [ContinuousConstSMul R M] (r : R) (v : MeasureTheory.VectorMeasure α M) :
        (r v) = r v
        theorem MeasureTheory.VectorMeasure.smul_apply {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {R : Type u_4} [Semiring R] [DistribMulAction R M] [ContinuousConstSMul R M] (r : R) (v : MeasureTheory.VectorMeasure α M) (i : Set α) :
        (r v) i = r v i
        Equations
        • MeasureTheory.VectorMeasure.instZero = { zero := { measureOf' := 0, empty' := , not_measurable' := , m_iUnion' := } }
        Equations
        • MeasureTheory.VectorMeasure.instInhabited = { default := 0 }
        @[simp]
        theorem MeasureTheory.VectorMeasure.coe_zero {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] :
        0 = 0
        theorem MeasureTheory.VectorMeasure.zero_apply {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (i : Set α) :
        0 i = 0

        The sum of two vector measure is a vector measure.

        Equations
        • v.add w = { measureOf' := v + w, empty' := , not_measurable' := , m_iUnion' := }
        Instances For
          Equations
          • MeasureTheory.VectorMeasure.instAdd = { add := MeasureTheory.VectorMeasure.add }
          @[simp]
          theorem MeasureTheory.VectorMeasure.add_apply {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] (v : MeasureTheory.VectorMeasure α M) (w : MeasureTheory.VectorMeasure α M) (i : Set α) :
          (v + w) i = v i + w i
          Equations
          @[simp]
          theorem MeasureTheory.VectorMeasure.coeFnAddMonoidHom_apply {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] (self : MeasureTheory.VectorMeasure α M) :
          ∀ (a : Set α), MeasureTheory.VectorMeasure.coeFnAddMonoidHom self a = self a

          (⇑) is an AddMonoidHom.

          Equations
          • MeasureTheory.VectorMeasure.coeFnAddMonoidHom = { toFun := MeasureTheory.VectorMeasure.measureOf', map_zero' := , map_add' := }
          Instances For

            The negative of a vector measure is a vector measure.

            Equations
            • v.neg = { measureOf' := -v, empty' := , not_measurable' := , m_iUnion' := }
            Instances For
              Equations
              • MeasureTheory.VectorMeasure.instNeg = { neg := MeasureTheory.VectorMeasure.neg }

              The difference of two vector measure is a vector measure.

              Equations
              • v.sub w = { measureOf' := v - w, empty' := , not_measurable' := , m_iUnion' := }
              Instances For
                Equations
                • MeasureTheory.VectorMeasure.instSub = { sub := MeasureTheory.VectorMeasure.sub }
                theorem MeasureTheory.VectorMeasure.sub_apply {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommGroup M] [TopologicalSpace M] [TopologicalAddGroup M] (v : MeasureTheory.VectorMeasure α M) (w : MeasureTheory.VectorMeasure α M) (i : Set α) :
                (v - w) i = v i - w i
                Equations
                Equations
                Equations
                @[simp]
                theorem MeasureTheory.Measure.toSignedMeasure_apply {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [hμ : MeasureTheory.IsFiniteMeasure μ] (s : Set α) :
                μ.toSignedMeasure s = if MeasurableSet s then (μ s).toReal else 0

                A finite measure coerced into a real function is a signed measure.

                Equations
                • μ.toSignedMeasure = { measureOf' := fun (s : Set α) => if MeasurableSet s then (μ s).toReal else 0, empty' := , not_measurable' := , m_iUnion' := }
                Instances For
                  theorem MeasureTheory.Measure.toSignedMeasure_apply_measurable {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] {i : Set α} (hi : MeasurableSet i) :
                  μ.toSignedMeasure i = (μ i).toReal
                  theorem MeasureTheory.Measure.toSignedMeasure_congr {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] (h : μ = ν) :
                  μ.toSignedMeasure = ν.toSignedMeasure
                  @[simp]
                  theorem MeasureTheory.Measure.toSignedMeasure_add {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] :
                  (μ + ν).toSignedMeasure = μ.toSignedMeasure + ν.toSignedMeasure
                  @[simp]
                  theorem MeasureTheory.Measure.toSignedMeasure_smul {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (r : NNReal) :
                  (r μ).toSignedMeasure = r μ.toSignedMeasure
                  @[simp]
                  theorem MeasureTheory.Measure.toENNRealVectorMeasure_apply {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (i : Set α) :
                  μ.toENNRealVectorMeasure i = if MeasurableSet i then μ i else 0

                  A measure is a vector measure over ℝ≥0∞.

                  Equations
                  • μ.toENNRealVectorMeasure = { measureOf' := fun (i : Set α) => if MeasurableSet i then μ i else 0, empty' := , not_measurable' := , m_iUnion' := }
                  Instances For
                    theorem MeasureTheory.Measure.toENNRealVectorMeasure_apply_measurable {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {i : Set α} (hi : MeasurableSet i) :
                    μ.toENNRealVectorMeasure i = μ i
                    @[simp]
                    theorem MeasureTheory.Measure.toENNRealVectorMeasure_add {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) (ν : MeasureTheory.Measure α) :
                    (μ + ν).toENNRealVectorMeasure = μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure
                    theorem MeasureTheory.Measure.toSignedMeasure_sub_apply {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν] {i : Set α} (hi : MeasurableSet i) :
                    (μ.toSignedMeasure - ν.toSignedMeasure) i = (μ i).toReal - (ν i).toReal

                    A vector measure over ℝ≥0∞ is a measure.

                    Equations
                    Instances For
                      theorem MeasureTheory.VectorMeasure.ennrealToMeasure_apply {α : Type u_1} {m : MeasurableSpace α} {v : MeasureTheory.VectorMeasure α ENNReal} {s : Set α} (hs : MeasurableSet s) :
                      v.ennrealToMeasure s = v s
                      @[simp]
                      theorem MeasureTheory.Measure.toENNRealVectorMeasure_ennrealToMeasure {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.VectorMeasure α ENNReal) :
                      μ.ennrealToMeasure.toENNRealVectorMeasure = μ
                      @[simp]
                      theorem MeasureTheory.VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) :
                      μ.toENNRealVectorMeasure.ennrealToMeasure = μ
                      @[simp]
                      theorem MeasureTheory.VectorMeasure.equivMeasure_symm_apply {α : Type u_1} [MeasurableSpace α] (μ : MeasureTheory.Measure α) :
                      MeasureTheory.VectorMeasure.equivMeasure.symm μ = μ.toENNRealVectorMeasure
                      @[simp]
                      theorem MeasureTheory.VectorMeasure.equivMeasure_apply {α : Type u_1} [MeasurableSpace α] (v : MeasureTheory.VectorMeasure α ENNReal) :
                      MeasureTheory.VectorMeasure.equivMeasure v = v.ennrealToMeasure

                      The equiv between VectorMeasure α ℝ≥0∞ and Measure α formed by MeasureTheory.VectorMeasure.ennrealToMeasure and MeasureTheory.Measure.toENNRealVectorMeasure.

                      Equations
                      • MeasureTheory.VectorMeasure.equivMeasure = { toFun := MeasureTheory.VectorMeasure.ennrealToMeasure, invFun := MeasureTheory.Measure.toENNRealVectorMeasure, left_inv := , right_inv := }
                      Instances For

                        The pushforward of a vector measure along a function.

                        Equations
                        • v.map f = if hf : Measurable f then { measureOf' := fun (s : Set β) => if MeasurableSet s then v (f ⁻¹' s) else 0, empty' := , not_measurable' := , m_iUnion' := } else 0
                        Instances For
                          theorem MeasureTheory.VectorMeasure.map_not_measurable {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : MeasureTheory.VectorMeasure α M) {f : αβ} (hf : ¬Measurable f) :
                          v.map f = 0
                          theorem MeasureTheory.VectorMeasure.map_apply {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : MeasureTheory.VectorMeasure α M) {f : αβ} (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) :
                          (v.map f) s = v (f ⁻¹' s)
                          @[simp]
                          @[simp]

                          Given a vector measure v on M and a continuous AddMonoidHom f : M → N, f ∘ v is a vector measure on N.

                          Equations
                          • v.mapRange f hf = { measureOf' := fun (s : Set α) => f (v s), empty' := , not_measurable' := , m_iUnion' := }
                          Instances For
                            @[simp]
                            theorem MeasureTheory.VectorMeasure.mapRange_apply {α : Type u_1} [MeasurableSpace α] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : MeasureTheory.VectorMeasure α M) {N : Type u_4} [AddCommMonoid N] [TopologicalSpace N] {f : M →+ N} (hf : Continuous f) {s : Set α} :
                            (v.mapRange f hf) s = f (v s)
                            @[simp]
                            theorem MeasureTheory.VectorMeasure.mapRange_add {α : Type u_1} [MeasurableSpace α] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {N : Type u_4} [AddCommMonoid N] [TopologicalSpace N] [ContinuousAdd M] [ContinuousAdd N] {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α M} {f : M →+ N} (hf : Continuous f) :
                            (v + w).mapRange f hf = v.mapRange f hf + w.mapRange f hf

                            Given a continuous AddMonoidHom f : M → N, mapRangeHom is the AddMonoidHom mapping the vector measure v on M to the vector measure f ∘ v on N.

                            Equations
                            Instances For

                              Given a continuous linear map f : M → N, mapRangeₗ is the linear map mapping the vector measure v on M to the vector measure f ∘ v on N.

                              Equations
                              Instances For

                                The restriction of a vector measure on some set.

                                Equations
                                • v.restrict i = if hi : MeasurableSet i then { measureOf' := fun (s : Set α) => if MeasurableSet s then v (s i) else 0, empty' := , not_measurable' := , m_iUnion' := } else 0
                                Instances For
                                  theorem MeasureTheory.VectorMeasure.restrict_apply {α : Type u_1} [MeasurableSpace α] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : MeasureTheory.VectorMeasure α M) {i : Set α} (hi : MeasurableSet i) {j : Set α} (hj : MeasurableSet j) :
                                  (v.restrict i) j = v (j i)
                                  theorem MeasureTheory.VectorMeasure.restrict_eq_self {α : Type u_1} [MeasurableSpace α] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : MeasureTheory.VectorMeasure α M) {i : Set α} (hi : MeasurableSet i) {j : Set α} (hj : MeasurableSet j) (hij : j i) :
                                  (v.restrict i) j = v j
                                  @[simp]
                                  theorem MeasureTheory.VectorMeasure.restrict_univ {α : Type u_1} [MeasurableSpace α] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : MeasureTheory.VectorMeasure α M) :
                                  v.restrict Set.univ = v
                                  theorem MeasureTheory.VectorMeasure.map_add {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] (v : MeasureTheory.VectorMeasure α M) (w : MeasureTheory.VectorMeasure α M) (f : αβ) :
                                  (v + w).map f = v.map f + w.map f

                                  VectorMeasure.map as an additive monoid homomorphism.

                                  Equations
                                  Instances For
                                    theorem MeasureTheory.VectorMeasure.restrict_add {α : Type u_1} [MeasurableSpace α] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] (v : MeasureTheory.VectorMeasure α M) (w : MeasureTheory.VectorMeasure α M) (i : Set α) :
                                    (v + w).restrict i = v.restrict i + w.restrict i

                                    VectorMeasure.restrict as an additive monoid homomorphism.

                                    Equations
                                    Instances For
                                      @[simp]
                                      theorem MeasureTheory.VectorMeasure.map_smul {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [MeasurableSpace β] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {R : Type u_4} [Semiring R] [DistribMulAction R M] [ContinuousConstSMul R M] {v : MeasureTheory.VectorMeasure α M} {f : αβ} (c : R) :
                                      (c v).map f = c v.map f
                                      @[simp]
                                      theorem MeasureTheory.VectorMeasure.restrict_smul {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {R : Type u_4} [Semiring R] [DistribMulAction R M] [ContinuousConstSMul R M] {v : MeasureTheory.VectorMeasure α M} {i : Set α} (c : R) :
                                      (c v).restrict i = c v.restrict i
                                      @[simp]
                                      theorem MeasureTheory.VectorMeasure.mapₗ_apply {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [MeasurableSpace β] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {R : Type u_4} [Semiring R] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] (f : αβ) (v : MeasureTheory.VectorMeasure α M) :

                                      VectorMeasure.map as a linear map.

                                      Equations
                                      Instances For

                                        VectorMeasure.restrict as an additive monoid homomorphism.

                                        Equations
                                        Instances For

                                          Vector measures over a partially ordered monoid is partially ordered.

                                          This definition is consistent with Measure.instPartialOrder.

                                          Equations
                                          theorem MeasureTheory.VectorMeasure.le_iff {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α M} :
                                          v w ∀ (i : Set α), MeasurableSet iv i w i
                                          theorem MeasureTheory.VectorMeasure.le_iff' {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α M} :
                                          v w ∀ (i : Set α), v i w i
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            theorem MeasureTheory.VectorMeasure.restrict_le_restrict_iff {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v : MeasureTheory.VectorMeasure α M) (w : MeasureTheory.VectorMeasure α M) {i : Set α} (hi : MeasurableSet i) :
                                            v.restrict i w.restrict i ∀ ⦃j : Set α⦄, MeasurableSet jj iv j w j
                                            theorem MeasureTheory.VectorMeasure.subset_le_of_restrict_le_restrict {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v : MeasureTheory.VectorMeasure α M) (w : MeasureTheory.VectorMeasure α M) {i : Set α} (hi : MeasurableSet i) (hi₂ : v.restrict i w.restrict i) {j : Set α} (hj : j i) :
                                            v j w j
                                            theorem MeasureTheory.VectorMeasure.restrict_le_restrict_of_subset_le {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v : MeasureTheory.VectorMeasure α M) (w : MeasureTheory.VectorMeasure α M) {i : Set α} (h : ∀ ⦃j : Set α⦄, MeasurableSet jj iv j w j) :
                                            v.restrict i w.restrict i
                                            theorem MeasureTheory.VectorMeasure.restrict_le_restrict_subset {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v : MeasureTheory.VectorMeasure α M) (w : MeasureTheory.VectorMeasure α M) {i : Set α} {j : Set α} (hi₁ : MeasurableSet i) (hi₂ : v.restrict i w.restrict i) (hij : j i) :
                                            v.restrict j w.restrict j
                                            theorem MeasureTheory.VectorMeasure.le_restrict_univ_iff_le {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v : MeasureTheory.VectorMeasure α M) (w : MeasureTheory.VectorMeasure α M) :
                                            v.restrict Set.univ w.restrict Set.univ v w
                                            theorem MeasureTheory.VectorMeasure.neg_le_neg {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [OrderedAddCommGroup M] [TopologicalAddGroup M] (v : MeasureTheory.VectorMeasure α M) (w : MeasureTheory.VectorMeasure α M) {i : Set α} (hi : MeasurableSet i) (h : v.restrict i w.restrict i) :
                                            (-w).restrict i (-v).restrict i
                                            @[simp]
                                            theorem MeasureTheory.VectorMeasure.neg_le_neg_iff {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [OrderedAddCommGroup M] [TopologicalAddGroup M] (v : MeasureTheory.VectorMeasure α M) (w : MeasureTheory.VectorMeasure α M) {i : Set α} (hi : MeasurableSet i) :
                                            (-w).restrict i (-v).restrict i v.restrict i w.restrict i
                                            theorem MeasureTheory.VectorMeasure.restrict_le_restrict_iUnion {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [OrderedAddCommMonoid M] [OrderClosedTopology M] (v : MeasureTheory.VectorMeasure α M) (w : MeasureTheory.VectorMeasure α M) {f : Set α} (hf₁ : ∀ (n : ), MeasurableSet (f n)) (hf₂ : ∀ (n : ), v.restrict (f n) w.restrict (f n)) :
                                            v.restrict (⋃ (n : ), f n) w.restrict (⋃ (n : ), f n)
                                            theorem MeasureTheory.VectorMeasure.restrict_le_restrict_countable_iUnion {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [OrderedAddCommMonoid M] [OrderClosedTopology M] (v : MeasureTheory.VectorMeasure α M) (w : MeasureTheory.VectorMeasure α M) [Countable β] {f : βSet α} (hf₁ : ∀ (b : β), MeasurableSet (f b)) (hf₂ : ∀ (b : β), v.restrict (f b) w.restrict (f b)) :
                                            v.restrict (⋃ (b : β), f b) w.restrict (⋃ (b : β), f b)
                                            theorem MeasureTheory.VectorMeasure.restrict_le_restrict_union {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [OrderedAddCommMonoid M] [OrderClosedTopology M] (v : MeasureTheory.VectorMeasure α M) (w : MeasureTheory.VectorMeasure α M) {i : Set α} {j : Set α} (hi₁ : MeasurableSet i) (hi₂ : v.restrict i w.restrict i) (hj₁ : MeasurableSet j) (hj₂ : v.restrict j w.restrict j) :
                                            v.restrict (i j) w.restrict (i j)

                                            A vector measure v is absolutely continuous with respect to a measure μ if for all sets s, μ s = 0, we have v s = 0.

                                            Equations
                                            • v.AbsolutelyContinuous w = ∀ ⦃s : Set α⦄, w s = 0v s = 0
                                            Instances For

                                              A vector measure v is absolutely continuous with respect to a measure μ if for all sets s, μ s = 0, we have v s = 0.

                                              Equations
                                              Instances For
                                                theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.mk {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N} (h : ∀ ⦃s : Set α⦄, MeasurableSet sw s = 0v s = 0) :
                                                v.AbsolutelyContinuous w
                                                theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.eq {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [AddCommMonoid M] [TopologicalSpace M] {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α M} (h : v = w) :
                                                v.AbsolutelyContinuous w
                                                theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.trans {α : Type u_1} {m : MeasurableSpace α} {L : Type u_3} {M : Type u_4} {N : Type u_5} [AddCommMonoid L] [TopologicalSpace L] [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {u : MeasureTheory.VectorMeasure α L} {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N} (huv : u.AbsolutelyContinuous v) (hvw : v.AbsolutelyContinuous w) :
                                                u.AbsolutelyContinuous w
                                                theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.neg_left {α : Type u_1} {m : MeasurableSpace α} {N : Type u_5} [AddCommMonoid N] [TopologicalSpace N] {M : Type u_6} [AddCommGroup M] [TopologicalSpace M] [TopologicalAddGroup M] {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N} (h : v.AbsolutelyContinuous w) :
                                                (-v).AbsolutelyContinuous w
                                                theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.neg_right {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [AddCommMonoid M] [TopologicalSpace M] {N : Type u_6} [AddCommGroup N] [TopologicalSpace N] [TopologicalAddGroup N] {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N} (h : v.AbsolutelyContinuous w) :
                                                v.AbsolutelyContinuous (-w)
                                                theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.add {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] [ContinuousAdd M] {v₁ : MeasureTheory.VectorMeasure α M} {v₂ : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N} (hv₁ : v₁.AbsolutelyContinuous w) (hv₂ : v₂.AbsolutelyContinuous w) :
                                                (v₁ + v₂).AbsolutelyContinuous w
                                                theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.sub {α : Type u_1} {m : MeasurableSpace α} {N : Type u_5} [AddCommMonoid N] [TopologicalSpace N] {M : Type u_6} [AddCommGroup M] [TopologicalSpace M] [TopologicalAddGroup M] {v₁ : MeasureTheory.VectorMeasure α M} {v₂ : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N} (hv₁ : v₁.AbsolutelyContinuous w) (hv₂ : v₂.AbsolutelyContinuous w) :
                                                (v₁ - v₂).AbsolutelyContinuous w
                                                theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.smul {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {R : Type u_6} [Semiring R] [DistribMulAction R M] [ContinuousConstSMul R M] {r : R} {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N} (h : v.AbsolutelyContinuous w) :
                                                (r v).AbsolutelyContinuous w
                                                theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.map {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N} [MeasureTheory.MeasureSpace β] (h : v.AbsolutelyContinuous w) (f : αβ) :
                                                (v.map f).AbsolutelyContinuous (w.map f)
                                                theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.ennrealToMeasure {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [AddCommMonoid M] [TopologicalSpace M] {v : MeasureTheory.VectorMeasure α M} {μ : MeasureTheory.VectorMeasure α ENNReal} :
                                                (∀ ⦃s : Set α⦄, μ.ennrealToMeasure s = 0v s = 0) v.AbsolutelyContinuous μ

                                                Two vector measures v and w are said to be mutually singular if there exists a measurable set s, such that for all t ⊆ s, v t = 0 and for all t ⊆ sᶜ, w t = 0.

                                                We note that we do not require the measurability of t in the definition since this makes it easier to use. This is equivalent to the definition which requires measurability. To prove MutuallySingular with the measurability condition, use MeasureTheory.VectorMeasure.MutuallySingular.mk.

                                                Equations
                                                Instances For

                                                  Two vector measures v and w are said to be mutually singular if there exists a measurable set s, such that for all t ⊆ s, v t = 0 and for all t ⊆ sᶜ, w t = 0.

                                                  We note that we do not require the measurability of t in the definition since this makes it easier to use. This is equivalent to the definition which requires measurability. To prove MutuallySingular with the measurability condition, use MeasureTheory.VectorMeasure.MutuallySingular.mk.

                                                  Equations
                                                  Instances For
                                                    theorem MeasureTheory.VectorMeasure.MutuallySingular.mk {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N} (s : Set α) (hs : MeasurableSet s) (h₁ : ts, MeasurableSet tv t = 0) (h₂ : ts, MeasurableSet tw t = 0) :
                                                    v.MutuallySingular w
                                                    theorem MeasureTheory.VectorMeasure.MutuallySingular.symm {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N} (h : v.MutuallySingular w) :
                                                    w.MutuallySingular v
                                                    theorem MeasureTheory.VectorMeasure.MutuallySingular.add_left {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {v₁ : MeasureTheory.VectorMeasure α M} {v₂ : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N} [T2Space N] [ContinuousAdd M] (h₁ : v₁.MutuallySingular w) (h₂ : v₂.MutuallySingular w) :
                                                    (v₁ + v₂).MutuallySingular w
                                                    theorem MeasureTheory.VectorMeasure.MutuallySingular.add_right {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {v : MeasureTheory.VectorMeasure α M} {w₁ : MeasureTheory.VectorMeasure α N} {w₂ : MeasureTheory.VectorMeasure α N} [T2Space M] [ContinuousAdd N] (h₁ : v.MutuallySingular w₁) (h₂ : v.MutuallySingular w₂) :
                                                    v.MutuallySingular (w₁ + w₂)
                                                    theorem MeasureTheory.VectorMeasure.MutuallySingular.smul_right {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N} {R : Type u_6} [Semiring R] [DistribMulAction R N] [ContinuousConstSMul R N] (r : R) (h : v.MutuallySingular w) :
                                                    v.MutuallySingular (r w)
                                                    theorem MeasureTheory.VectorMeasure.MutuallySingular.smul_left {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N} {R : Type u_6} [Semiring R] [DistribMulAction R M] [ContinuousConstSMul R M] (r : R) (h : v.MutuallySingular w) :
                                                    (r v).MutuallySingular w
                                                    theorem MeasureTheory.VectorMeasure.MutuallySingular.neg_left {α : Type u_1} {m : MeasurableSpace α} {N : Type u_5} [AddCommMonoid N] [TopologicalSpace N] {M : Type u_6} [AddCommGroup M] [TopologicalSpace M] [TopologicalAddGroup M] {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N} (h : v.MutuallySingular w) :
                                                    (-v).MutuallySingular w
                                                    theorem MeasureTheory.VectorMeasure.MutuallySingular.neg_right {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [AddCommMonoid M] [TopologicalSpace M] {N : Type u_6} [AddCommGroup N] [TopologicalSpace N] [TopologicalAddGroup N] {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N} (h : v.MutuallySingular w) :
                                                    v.MutuallySingular (-w)
                                                    @[simp]
                                                    theorem MeasureTheory.VectorMeasure.MutuallySingular.neg_left_iff {α : Type u_1} {m : MeasurableSpace α} {N : Type u_5} [AddCommMonoid N] [TopologicalSpace N] {M : Type u_6} [AddCommGroup M] [TopologicalSpace M] [TopologicalAddGroup M] {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N} :
                                                    (-v).MutuallySingular w v.MutuallySingular w
                                                    @[simp]
                                                    theorem MeasureTheory.VectorMeasure.MutuallySingular.neg_right_iff {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [AddCommMonoid M] [TopologicalSpace M] {N : Type u_6} [AddCommGroup N] [TopologicalSpace N] [TopologicalAddGroup N] {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N} :
                                                    v.MutuallySingular (-w) v.MutuallySingular w
                                                    @[simp]
                                                    theorem MeasureTheory.VectorMeasure.trim_apply {α : Type u_1} {M : Type u_4} [AddCommMonoid M] [TopologicalSpace M] {m : MeasurableSpace α} {n : MeasurableSpace α} (v : MeasureTheory.VectorMeasure α M) (hle : m n) (i : Set α) :
                                                    (v.trim hle) i = if MeasurableSet i then v i else 0

                                                    Restriction of a vector measure onto a sub-σ-algebra.

                                                    Equations
                                                    • v.trim hle = { measureOf' := fun (i : Set α) => if MeasurableSet i then v i else 0, empty' := , not_measurable' := , m_iUnion' := }
                                                    Instances For
                                                      theorem MeasureTheory.VectorMeasure.trim_measurableSet_eq {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [AddCommMonoid M] [TopologicalSpace M] {n : MeasurableSpace α} {v : MeasureTheory.VectorMeasure α M} (hle : m n) {i : Set α} (hi : MeasurableSet i) :
                                                      (v.trim hle) i = v i
                                                      theorem MeasureTheory.VectorMeasure.restrict_trim {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [AddCommMonoid M] [TopologicalSpace M] {n : MeasurableSpace α} {v : MeasureTheory.VectorMeasure α M} (hle : m n) {i : Set α} (hi : MeasurableSet i) :
                                                      (v.trim hle).restrict i = (v.restrict i).trim hle

                                                      The underlying function for SignedMeasure.toMeasureOfZeroLE.

                                                      Equations
                                                      Instances For

                                                        Given a signed measure s and a positive measurable set i, toMeasureOfZeroLE provides the measure, mapping measurable sets j to s (i ∩ j).

                                                        Equations
                                                        Instances For
                                                          theorem MeasureTheory.SignedMeasure.toMeasureOfZeroLE_apply {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) {i : Set α} {j : Set α} (hi : MeasureTheory.VectorMeasure.restrict 0 i MeasureTheory.VectorMeasure.restrict s i) (hi₁ : MeasurableSet i) (hj₁ : MeasurableSet j) :
                                                          (s.toMeasureOfZeroLE i hi₁ hi) j = s (i j),

                                                          Given a signed measure s and a negative measurable set i, toMeasureOfLEZero provides the measure, mapping measurable sets j to -s (i ∩ j).

                                                          Equations
                                                          • s.toMeasureOfLEZero i hi₁ hi₂ = (-s).toMeasureOfZeroLE i hi₁
                                                          Instances For
                                                            theorem MeasureTheory.SignedMeasure.toMeasureOfLEZero_apply {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) {i : Set α} {j : Set α} (hi : MeasureTheory.VectorMeasure.restrict s i MeasureTheory.VectorMeasure.restrict 0 i) (hi₁ : MeasurableSet i) (hj₁ : MeasurableSet j) :
                                                            (s.toMeasureOfLEZero i hi₁ hi) j = -s (i j),
                                                            theorem MeasureTheory.SignedMeasure.toMeasureOfZeroLE_toSignedMeasure {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (hs : MeasureTheory.VectorMeasure.restrict 0 Set.univ MeasureTheory.VectorMeasure.restrict s Set.univ) :
                                                            (s.toMeasureOfZeroLE Set.univ hs).toSignedMeasure = s
                                                            theorem MeasureTheory.SignedMeasure.toMeasureOfLEZero_toSignedMeasure {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (hs : MeasureTheory.VectorMeasure.restrict s Set.univ MeasureTheory.VectorMeasure.restrict 0 Set.univ) :
                                                            (s.toMeasureOfLEZero Set.univ hs).toSignedMeasure = -s
                                                            theorem MeasureTheory.Measure.toSignedMeasure_toMeasureOfZeroLE {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] :
                                                            μ.toSignedMeasure.toMeasureOfZeroLE Set.univ = μ