# 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 α.

## Main definitions #

• MeasureTheory.VectorMeasure is a vector valued, σ-additive function that maps the empty and non-measurable set to zero.
• MeasureTheory.VectorMeasure.map is the pushforward of a vector measure along a function.
• MeasureTheory.VectorMeasure.restrict is the restriction of a vector measure on some set.

## Notation #

• v ≤[i] w means that the vector measure v restricted on the set i is less than or equal to the vector measure w restricted on i, i.e. v.restrict i ≤ w.restrict i.

## 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) [] (M : Type u_4) [] [] :
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.

• measureOf' : Set αM
• empty' : self = 0
• not_measurable' : ∀ ⦃i : Set α⦄, self i = 0
• m_iUnion' : ∀ ⦃f : Set α⦄, (∀ (i : ), MeasurableSet (f i))Pairwise (Disjoint on f)HasSum (fun (i : ) => self (f i)) (self (⋃ (i : ), f i))
Instances For
theorem MeasureTheory.VectorMeasure.empty' {α : Type u_3} [] {M : Type u_4} [] [] (self : ) :
self = 0
theorem MeasureTheory.VectorMeasure.not_measurable' {α : Type u_3} [] {M : Type u_4} [] [] (self : ) ⦃i : Set α :
self i = 0
theorem MeasureTheory.VectorMeasure.m_iUnion' {α : Type u_3} [] {M : Type u_4} [] [] (self : ) ⦃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) [] :
Type u_3

A SignedMeasure is an ℝ-vector measure.

Equations
Instances For
@[reducible, inline]
abbrev MeasureTheory.ComplexMeasure (α : Type u_3) [] :
Type u_3

A ComplexMeasure is a ℂ-vector measure.

Equations
Instances For
instance MeasureTheory.VectorMeasure.instCoeFun {α : Type u_1} {m : } {M : Type u_3} [] [] :
CoeFun fun (x : ) => Set αM
Equations
• MeasureTheory.VectorMeasure.instCoeFun = { coe := MeasureTheory.VectorMeasure.measureOf' }
@[simp]
theorem MeasureTheory.VectorMeasure.empty {α : Type u_1} {m : } {M : Type u_3} [] [] (v : ) :
v = 0
theorem MeasureTheory.VectorMeasure.not_measurable {α : Type u_1} {m : } {M : Type u_3} [] [] (v : ) {i : Set α} (hi : ) :
v i = 0
theorem MeasureTheory.VectorMeasure.m_iUnion {α : Type u_1} {m : } {M : Type u_3} [] [] (v : ) {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.of_disjoint_iUnion_nat {α : Type u_1} {m : } {M : Type u_3} [] [] [] (v : ) {f : Set α} (hf₁ : ∀ (i : ), MeasurableSet (f i)) (hf₂ : Pairwise (Disjoint on f)) :
v (⋃ (i : ), f i) = ∑' (i : ), v (f i)
theorem MeasureTheory.VectorMeasure.coe_injective {α : Type u_1} {m : } {M : Type u_3} [] [] :
Function.Injective MeasureTheory.VectorMeasure.measureOf'
theorem MeasureTheory.VectorMeasure.ext_iff' {α : Type u_1} {m : } {M : Type u_3} [] [] (v : ) (w : ) :
v = w ∀ (i : Set α), v i = w i
theorem MeasureTheory.VectorMeasure.ext_iff {α : Type u_1} {m : } {M : Type u_3} [] [] (v : ) (w : ) :
v = w ∀ (i : Set α), v i = w i
theorem MeasureTheory.VectorMeasure.ext {α : Type u_1} {m : } {M : Type u_3} [] [] {s : } {t : } (h : ∀ (i : Set α), s i = t i) :
s = t
theorem MeasureTheory.VectorMeasure.hasSum_of_disjoint_iUnion {α : Type u_1} {β : Type u_2} {m : } {M : Type u_3} [] [] [] {v : } [] {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.of_disjoint_iUnion {α : Type u_1} {β : Type u_2} {m : } {M : Type u_3} [] [] [] {v : } [] {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 : } {M : Type u_3} [] [] [] {v : } {A : Set α} {B : Set α} (h : Disjoint A B) (hA : ) (hB : ) :
v (A B) = v A + v B
theorem MeasureTheory.VectorMeasure.of_add_of_diff {α : Type u_1} {m : } {M : Type u_3} [] [] [] {v : } {A : Set α} {B : Set α} (hA : ) (hB : ) (h : A B) :
v A + v (B \ A) = v B
theorem MeasureTheory.VectorMeasure.of_diff {α : Type u_1} {m : } {M : Type u_4} [] [] [] {v : } {A : Set α} {B : Set α} (hA : ) (hB : ) (h : A B) :
v (B \ A) = v B - v A
theorem MeasureTheory.VectorMeasure.of_diff_of_diff_eq_zero {α : Type u_1} {m : } {M : Type u_3} [] [] [] {v : } {A : Set α} {B : Set α} (hA : ) (hB : ) (h' : v (B \ A) = 0) :
v (A \ B) + v B = v A
theorem MeasureTheory.VectorMeasure.of_iUnion_nonneg {α : Type u_1} {m : } {f : Set α} {M : Type u_4} [] {v : } (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} {m : } {f : Set α} {M : Type u_4} [] {v : } (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 : } {s : } {A : Set α} {B : Set α} (h : Disjoint A B) (hA₁ : ) (hB₁ : ) (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 : } {s : } {A : Set α} {B : Set α} (h : Disjoint A B) (hA₁ : ) (hB₁ : ) (hA₂ : s A 0) (hB₂ : s B 0) (hAB : s (A B) = 0) :
s A = 0
def MeasureTheory.VectorMeasure.smul {α : Type u_1} {m : } {M : Type u_3} [] [] {R : Type u_4} [] [] [] (r : R) (v : ) :

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

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

The sum of two vector measure is a vector measure.

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

(⇑) is an AddMonoidHom.

Equations
• MeasureTheory.VectorMeasure.coeFnAddMonoidHom = { toFun := MeasureTheory.VectorMeasure.measureOf', map_zero' := , map_add' := }
Instances For
def MeasureTheory.VectorMeasure.neg {α : Type u_1} {m : } {M : Type u_3} [] [] (v : ) :

The negative of a vector measure is a vector measure.

Equations
• v.neg = { measureOf' := -v, empty' := , not_measurable' := , m_iUnion' := }
Instances For
instance MeasureTheory.VectorMeasure.instNeg {α : Type u_1} {m : } {M : Type u_3} [] [] :
Equations
• MeasureTheory.VectorMeasure.instNeg = { neg := MeasureTheory.VectorMeasure.neg }
@[simp]
theorem MeasureTheory.VectorMeasure.coe_neg {α : Type u_1} {m : } {M : Type u_3} [] [] (v : ) :
(-v) = -v
theorem MeasureTheory.VectorMeasure.neg_apply {α : Type u_1} {m : } {M : Type u_3} [] [] (v : ) (i : Set α) :
(-v) i = -v i
def MeasureTheory.VectorMeasure.sub {α : Type u_1} {m : } {M : Type u_3} [] [] (v : ) (w : ) :

The difference of two vector measure is a vector measure.

Equations
• v.sub w = { measureOf' := v - w, empty' := , not_measurable' := , m_iUnion' := }
Instances For
instance MeasureTheory.VectorMeasure.instSub {α : Type u_1} {m : } {M : Type u_3} [] [] :
Equations
• MeasureTheory.VectorMeasure.instSub = { sub := MeasureTheory.VectorMeasure.sub }
@[simp]
theorem MeasureTheory.VectorMeasure.coe_sub {α : Type u_1} {m : } {M : Type u_3} [] [] (v : ) (w : ) :
(v - w) = v - w
theorem MeasureTheory.VectorMeasure.sub_apply {α : Type u_1} {m : } {M : Type u_3} [] [] (v : ) (w : ) (i : Set α) :
(v - w) i = v i - w i
instance MeasureTheory.VectorMeasure.instAddCommGroup {α : Type u_1} {m : } {M : Type u_3} [] [] :
Equations
instance MeasureTheory.VectorMeasure.instDistribMulAction {α : Type u_1} {m : } {M : Type u_3} [] [] {R : Type u_4} [] [] [] [] :
Equations
instance MeasureTheory.VectorMeasure.instModule {α : Type u_1} {m : } {M : Type u_3} [] [] {R : Type u_4} [] [Module R M] [] [] :
Equations
@[simp]
theorem MeasureTheory.Measure.toSignedMeasure_apply {α : Type u_1} {m : } (μ : ) [hμ : ] (s : Set α) :
μ.toSignedMeasure s = if then (μ s).toReal else 0
def MeasureTheory.Measure.toSignedMeasure {α : Type u_1} {m : } (μ : ) [hμ : ] :

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

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

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

Equations
• μ.toENNRealVectorMeasure = { measureOf' := fun (i : Set α) => if then μ i else 0, empty' := , not_measurable' := , m_iUnion' := }
Instances For
theorem MeasureTheory.Measure.toENNRealVectorMeasure_apply_measurable {α : Type u_1} {m : } {μ : } {i : Set α} (hi : ) :
μ.toENNRealVectorMeasure i = μ i
@[simp]
theorem MeasureTheory.Measure.toENNRealVectorMeasure_add {α : Type u_1} {m : } (μ : ) (ν : ) :
(μ + ν).toENNRealVectorMeasure = μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure
theorem MeasureTheory.Measure.toSignedMeasure_sub_apply {α : Type u_1} {m : } {μ : } {ν : } {i : Set α} (hi : ) :
(μ.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 : } {s : Set α} (hs : ) :
v.ennrealToMeasure s = v s
@[simp]
theorem MeasureTheory.Measure.toENNRealVectorMeasure_ennrealToMeasure {α : Type u_1} {m : } :
μ.ennrealToMeasure.toENNRealVectorMeasure = μ
@[simp]
theorem MeasureTheory.VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure {α : Type u_1} {m : } (μ : ) :
μ.toENNRealVectorMeasure.ennrealToMeasure = μ
@[simp]
theorem MeasureTheory.VectorMeasure.equivMeasure_apply {α : Type u_1} [] :
MeasureTheory.VectorMeasure.equivMeasure v = v.ennrealToMeasure
@[simp]
theorem MeasureTheory.VectorMeasure.equivMeasure_symm_apply {α : Type u_1} [] (μ : ) :
MeasureTheory.VectorMeasure.equivMeasure.symm μ = μ.toENNRealVectorMeasure

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
def MeasureTheory.VectorMeasure.map {α : Type u_1} {β : Type u_2} [] [] {M : Type u_3} [] [] (v : ) (f : αβ) :

The pushforward of a vector measure along a function.

Equations
• v.map f = if hf : then { measureOf' := fun (s : Set β) => if 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} [] [] {M : Type u_3} [] [] (v : ) {f : αβ} (hf : ) :
v.map f = 0
theorem MeasureTheory.VectorMeasure.map_apply {α : Type u_1} {β : Type u_2} [] [] {M : Type u_3} [] [] (v : ) {f : αβ} (hf : ) {s : Set β} (hs : ) :
(v.map f) s = v (f ⁻¹' s)
@[simp]
theorem MeasureTheory.VectorMeasure.map_id {α : Type u_1} [] {M : Type u_3} [] [] (v : ) :
v.map id = v
@[simp]
theorem MeasureTheory.VectorMeasure.map_zero {α : Type u_1} {β : Type u_2} [] [] {M : Type u_3} [] [] (f : αβ) :
def MeasureTheory.VectorMeasure.mapRange {α : Type u_1} [] {M : Type u_3} [] [] {N : Type u_4} [] [] (v : ) (f : M →+ N) (hf : ) :

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} [] {M : Type u_3} [] [] (v : ) {N : Type u_4} [] [] {f : M →+ N} (hf : ) {s : Set α} :
(v.mapRange f hf) s = f (v s)
@[simp]
theorem MeasureTheory.VectorMeasure.mapRange_id {α : Type u_1} [] {M : Type u_3} [] [] (v : ) :
v.mapRange () = v
@[simp]
theorem MeasureTheory.VectorMeasure.mapRange_zero {α : Type u_1} [] {M : Type u_3} [] [] {N : Type u_4} [] [] {f : M →+ N} (hf : ) :
@[simp]
theorem MeasureTheory.VectorMeasure.mapRange_add {α : Type u_1} [] {M : Type u_3} [] [] {N : Type u_4} [] [] [] [] {v : } {w : } {f : M →+ N} (hf : ) :
(v + w).mapRange f hf = v.mapRange f hf + w.mapRange f hf
def MeasureTheory.VectorMeasure.mapRangeHom {α : Type u_1} [] {M : Type u_3} [] [] {N : Type u_4} [] [] [] [] (f : M →+ N) (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
• = { toFun := fun (v : ) => v.mapRange f hf, map_zero' := , map_add' := }
Instances For
def MeasureTheory.VectorMeasure.mapRangeₗ {α : Type u_1} [] {M : Type u_3} [] [] {N : Type u_4} [] [] {R : Type u_5} [] [Module R M] [Module R N] [] [] [] [] (f : M →ₗ[R] N) (hf : ) :

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
• = { toFun := fun (v : ) => v.mapRange f.toAddMonoidHom hf, map_add' := , map_smul' := }
Instances For
def MeasureTheory.VectorMeasure.restrict {α : Type u_1} [] {M : Type u_3} [] [] (v : ) (i : Set α) :

The restriction of a vector measure on some set.

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

VectorMeasure.map as an additive monoid homomorphism.

Equations
• = { toFun := fun (v : ) => v.map f, map_zero' := , map_add' := }
Instances For
theorem MeasureTheory.VectorMeasure.restrict_add {α : Type u_1} [] {M : Type u_3} [] [] [] (v : ) (w : ) (i : Set α) :
(v + w).restrict i = v.restrict i + w.restrict i
@[simp]
theorem MeasureTheory.VectorMeasure.restrictGm_apply {α : Type u_1} [] {M : Type u_3} [] [] [] (i : Set α) (v : ) :
= v.restrict i
def MeasureTheory.VectorMeasure.restrictGm {α : Type u_1} [] {M : Type u_3} [] [] [] (i : Set α) :

VectorMeasure.restrict as an additive monoid homomorphism.

Equations
• = { toFun := fun (v : ) => v.restrict i, map_zero' := , map_add' := }
Instances For
@[simp]
theorem MeasureTheory.VectorMeasure.map_smul {α : Type u_1} {β : Type u_2} {m : } [] {M : Type u_3} [] [] {R : Type u_4} [] [] [] {v : } {f : αβ} (c : R) :
(c v).map f = c v.map f
@[simp]
theorem MeasureTheory.VectorMeasure.restrict_smul {α : Type u_1} {m : } {M : Type u_3} [] [] {R : Type u_4} [] [] [] {v : } {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 : } [] {M : Type u_3} [] [] {R : Type u_4} [] [Module R M] [] [] (f : αβ) (v : ) :
= v.map f
def MeasureTheory.VectorMeasure.mapₗ {α : Type u_1} {β : Type u_2} {m : } [] {M : Type u_3} [] [] {R : Type u_4} [] [Module R M] [] [] (f : αβ) :

VectorMeasure.map as a linear map.

Equations
• = { toFun := fun (v : ) => v.map f, map_add' := , map_smul' := }
Instances For
@[simp]
theorem MeasureTheory.VectorMeasure.restrictₗ_apply {α : Type u_1} {m : } {M : Type u_3} [] [] {R : Type u_4} [] [Module R M] [] [] (i : Set α) (v : ) :
= v.restrict i
def MeasureTheory.VectorMeasure.restrictₗ {α : Type u_1} {m : } {M : Type u_3} [] [] {R : Type u_4} [] [Module R M] [] [] (i : Set α) :

VectorMeasure.restrict as an additive monoid homomorphism.

Equations
• = { toFun := fun (v : ) => v.restrict i, map_add' := , map_smul' := }
Instances For
instance MeasureTheory.VectorMeasure.instPartialOrder {α : Type u_1} {m : } {M : Type u_3} [] [] [] :

Vector measures over a partially ordered monoid is partially ordered.

This definition is consistent with Measure.instPartialOrder.

Equations
• MeasureTheory.VectorMeasure.instPartialOrder =
theorem MeasureTheory.VectorMeasure.le_iff {α : Type u_1} {m : } {M : Type u_3} [] [] [] {v : } {w : } :
v w ∀ (i : Set α), v i w i
theorem MeasureTheory.VectorMeasure.le_iff' {α : Type u_1} {m : } {M : Type u_3} [] [] [] {v : } {w : } :
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 : } {M : Type u_3} [] [] [] (v : ) (w : ) {i : Set α} (hi : ) :
v.restrict i w.restrict i ∀ ⦃j : Set α⦄, j iv j w j
theorem MeasureTheory.VectorMeasure.subset_le_of_restrict_le_restrict {α : Type u_1} {m : } {M : Type u_3} [] [] [] (v : ) (w : ) {i : Set α} (hi : ) (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 : } {M : Type u_3} [] [] [] (v : ) (w : ) {i : Set α} (h : ∀ ⦃j : Set α⦄, j iv j w j) :
v.restrict i w.restrict i
theorem MeasureTheory.VectorMeasure.restrict_le_restrict_subset {α : Type u_1} {m : } {M : Type u_3} [] [] [] (v : ) (w : ) {i : Set α} {j : Set α} (hi₁ : ) (hi₂ : v.restrict i w.restrict i) (hij : j i) :
v.restrict j w.restrict j
theorem MeasureTheory.VectorMeasure.le_restrict_empty {α : Type u_1} {m : } {M : Type u_3} [] [] [] (v : ) (w : ) :
v.restrict w.restrict
theorem MeasureTheory.VectorMeasure.le_restrict_univ_iff_le {α : Type u_1} {m : } {M : Type u_3} [] [] [] (v : ) (w : ) :
v.restrict Set.univ w.restrict Set.univ v w
theorem MeasureTheory.VectorMeasure.neg_le_neg {α : Type u_1} {m : } {M : Type u_3} [] (v : ) (w : ) {i : Set α} (hi : ) (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 : } {M : Type u_3} [] (v : ) (w : ) {i : Set α} (hi : ) :
(-w).restrict i (-v).restrict i v.restrict i w.restrict i
theorem MeasureTheory.VectorMeasure.restrict_le_restrict_iUnion {α : Type u_1} {m : } {M : Type u_3} [] (v : ) (w : ) {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 : } {M : Type u_3} [] (v : ) (w : ) [] {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 : } {M : Type u_3} [] (v : ) (w : ) {i : Set α} {j : Set α} (hi₁ : ) (hi₂ : v.restrict i w.restrict i) (hj₁ : ) (hj₂ : v.restrict j w.restrict j) :
v.restrict (i j) w.restrict (i j)
theorem MeasureTheory.VectorMeasure.nonneg_of_zero_le_restrict {α : Type u_1} {m : } {M : Type u_3} [] (v : ) {i : Set α} (hi₂ : v.restrict i) :
0 v i
theorem MeasureTheory.VectorMeasure.nonpos_of_restrict_le_zero {α : Type u_1} {m : } {M : Type u_3} [] (v : ) {i : Set α} (hi₂ : v.restrict i ) :
v i 0
theorem MeasureTheory.VectorMeasure.zero_le_restrict_not_measurable {α : Type u_1} {m : } {M : Type u_3} [] (v : ) {i : Set α} (hi : ) :
v.restrict i
theorem MeasureTheory.VectorMeasure.restrict_le_zero_of_not_measurable {α : Type u_1} {m : } {M : Type u_3} [] (v : ) {i : Set α} (hi : ) :
v.restrict i
theorem MeasureTheory.VectorMeasure.measurable_of_not_zero_le_restrict {α : Type u_1} {m : } {M : Type u_3} [] (v : ) {i : Set α} (hi : ¬ v.restrict i) :
theorem MeasureTheory.VectorMeasure.measurable_of_not_restrict_le_zero {α : Type u_1} {m : } {M : Type u_3} [] (v : ) {i : Set α} (hi : ¬v.restrict i ) :
theorem MeasureTheory.VectorMeasure.zero_le_restrict_subset {α : Type u_1} {m : } {M : Type u_3} [] (v : ) {i : Set α} {j : Set α} (hi₁ : ) (hij : j i) (hi₂ : v.restrict i) :
v.restrict j
theorem MeasureTheory.VectorMeasure.restrict_le_zero_subset {α : Type u_1} {m : } {M : Type u_3} [] (v : ) {i : Set α} {j : Set α} (hi₁ : ) (hij : j i) (hi₂ : v.restrict i ) :
v.restrict j
theorem MeasureTheory.VectorMeasure.exists_pos_measure_of_not_restrict_le_zero {α : Type u_1} {m : } {M : Type u_3} [] (v : ) {i : Set α} (hi : ¬v.restrict i ) :
∃ (j : Set α), j i 0 < v j
instance MeasureTheory.VectorMeasure.covariant_add_le {α : Type u_1} {m : } {M : Type u_3} [] [] [] [CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x x_1] [] :
CovariantClass (fun (x x_1 : ) => x + x_1) fun (x x_1 : ) => x x_1
Equations
• =
def MeasureTheory.VectorMeasure.AbsolutelyContinuous {α : Type u_1} {m : } {M : Type u_4} {N : Type u_5} [] [] [] [] (v : ) (w : ) :

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 : } {M : Type u_4} {N : Type u_5} [] [] [] [] {v : } {w : } (h : ∀ ⦃s : Set α⦄, w s = 0v s = 0) :
v.AbsolutelyContinuous w
theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.eq {α : Type u_1} {m : } {M : Type u_4} [] [] {v : } {w : } (h : v = w) :
v.AbsolutelyContinuous w
theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.refl {α : Type u_1} {m : } {M : Type u_4} [] [] (v : ) :
v.AbsolutelyContinuous v
theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.trans {α : Type u_1} {m : } {L : Type u_3} {M : Type u_4} {N : Type u_5} [] [] [] [] [] [] {u : } {v : } {w : } (huv : u.AbsolutelyContinuous v) (hvw : v.AbsolutelyContinuous w) :
u.AbsolutelyContinuous w
theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.zero {α : Type u_1} {m : } {M : Type u_4} {N : Type u_5} [] [] [] [] (v : ) :
theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.neg_left {α : Type u_1} {m : } {N : Type u_5} [] [] {M : Type u_6} [] [] {v : } {w : } (h : v.AbsolutelyContinuous w) :
(-v).AbsolutelyContinuous w
theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.neg_right {α : Type u_1} {m : } {M : Type u_4} [] [] {N : Type u_6} [] [] {v : } {w : } (h : v.AbsolutelyContinuous w) :
v.AbsolutelyContinuous (-w)
theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.add {α : Type u_1} {m : } {M : Type u_4} {N : Type u_5} [] [] [] [] [] {v₁ : } {v₂ : } {w : } (hv₁ : v₁.AbsolutelyContinuous w) (hv₂ : v₂.AbsolutelyContinuous w) :
(v₁ + v₂).AbsolutelyContinuous w
theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.sub {α : Type u_1} {m : } {N : Type u_5} [] [] {M : Type u_6} [] [] {v₁ : } {v₂ : } {w : } (hv₁ : v₁.AbsolutelyContinuous w) (hv₂ : v₂.AbsolutelyContinuous w) :
(v₁ - v₂).AbsolutelyContinuous w
theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.smul {α : Type u_1} {m : } {M : Type u_4} {N : Type u_5} [] [] [] [] {R : Type u_6} [] [] [] {r : R} {v : } {w : } (h : v.AbsolutelyContinuous w) :
(r v).AbsolutelyContinuous w
theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.map {α : Type u_1} {β : Type u_2} {m : } {M : Type u_4} {N : Type u_5} [] [] [] [] {v : } {w : } (h : v.AbsolutelyContinuous w) (f : αβ) :
(v.map f).AbsolutelyContinuous (w.map f)
theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.ennrealToMeasure {α : Type u_1} {m : } {M : Type u_4} [] [] {v : } :
(∀ ⦃s : Set α⦄, μ.ennrealToMeasure s = 0v s = 0) v.AbsolutelyContinuous μ
def MeasureTheory.VectorMeasure.MutuallySingular {α : Type u_1} {m : } {M : Type u_4} {N : Type u_5} [] [] [] [] (v : ) (w : ) :

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
• v.MutuallySingular w = ∃ (s : Set α), (ts, v t = 0) ts, w t = 0
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 : } {M : Type u_4} {N : Type u_5} [] [] [] [] {v : } {w : } (s : Set α) (hs : ) (h₁ : ts, v t = 0) (h₂ : ts, w t = 0) :
v.MutuallySingular w
theorem MeasureTheory.VectorMeasure.MutuallySingular.symm {α : Type u_1} {m : } {M : Type u_4} {N : Type u_5} [] [] [] [] {v : } {w : } (h : v.MutuallySingular w) :
w.MutuallySingular v
theorem MeasureTheory.VectorMeasure.MutuallySingular.zero_right {α : Type u_1} {m : } {M : Type u_4} {N : Type u_5} [] [] [] [] {v : } :
v.MutuallySingular 0
theorem MeasureTheory.VectorMeasure.MutuallySingular.zero_left {α : Type u_1} {m : } {M : Type u_4} {N : Type u_5} [] [] [] [] {w : } :
theorem MeasureTheory.VectorMeasure.MutuallySingular.add_left {α : Type u_1} {m : } {M : Type u_4} {N : Type u_5} [] [] [] [] {v₁ : } {v₂ : } {w : } [] [] (h₁ : v₁.MutuallySingular w) (h₂ : v₂.MutuallySingular w) :
(v₁ + v₂).MutuallySingular w
theorem MeasureTheory.VectorMeasure.MutuallySingular.add_right {α : Type u_1} {m : } {M : Type u_4} {N : Type u_5} [] [] [] [] {v : } {w₁ : } {w₂ : } [] [] (h₁ : v.MutuallySingular w₁) (h₂ : v.MutuallySingular w₂) :
v.MutuallySingular (w₁ + w₂)
theorem MeasureTheory.VectorMeasure.MutuallySingular.smul_right {α : Type u_1} {m : } {M : Type u_4} {N : Type u_5} [] [] [] [] {v : } {w : } {R : Type u_6} [] [] [] (r : R) (h : v.MutuallySingular w) :
v.MutuallySingular (r w)
theorem MeasureTheory.VectorMeasure.MutuallySingular.smul_left {α : Type u_1} {m : } {M : Type u_4} {N : Type u_5} [] [] [] [] {v : } {w : } {R : Type u_6} [] [] [] (r : R) (h : v.MutuallySingular w) :
(r v).MutuallySingular w
theorem MeasureTheory.VectorMeasure.MutuallySingular.neg_left {α : Type u_1} {m : } {N : Type u_5} [] [] {M : Type u_6} [] [] {v : } {w : } (h : v.MutuallySingular w) :
(-v).MutuallySingular w
theorem MeasureTheory.VectorMeasure.MutuallySingular.neg_right {α : Type u_1} {m : } {M : Type u_4} [] [] {N : Type u_6} [] [] {v : } {w : } (h : v.MutuallySingular w) :
v.MutuallySingular (-w)
@[simp]
theorem MeasureTheory.VectorMeasure.MutuallySingular.neg_left_iff {α : Type u_1} {m : } {N : Type u_5} [] [] {M : Type u_6} [] [] {v : } {w : } :
(-v).MutuallySingular w v.MutuallySingular w
@[simp]
theorem MeasureTheory.VectorMeasure.MutuallySingular.neg_right_iff {α : Type u_1} {m : } {M : Type u_4} [] [] {N : Type u_6} [] [] {v : } {w : } :
v.MutuallySingular (-w) v.MutuallySingular w
@[simp]
theorem MeasureTheory.VectorMeasure.trim_apply {α : Type u_1} {M : Type u_4} [] [] {m : } {n : } (v : ) (hle : m n) (i : Set α) :
(v.trim hle) i = if then v i else 0
def MeasureTheory.VectorMeasure.trim {α : Type u_1} {M : Type u_4} [] [] {m : } {n : } (v : ) (hle : m n) :

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

Equations
• v.trim hle = { measureOf' := fun (i : Set α) => if then v i else 0, empty' := , not_measurable' := , m_iUnion' := }
Instances For
theorem MeasureTheory.VectorMeasure.trim_eq_self {α : Type u_1} {M : Type u_4} [] [] {n : } {v : } :
v.trim = v
@[simp]
theorem MeasureTheory.VectorMeasure.zero_trim {α : Type u_1} {m : } {M : Type u_4} [] [] {n : } (hle : m n) :
theorem MeasureTheory.VectorMeasure.trim_measurableSet_eq {α : Type u_1} {m : } {M : Type u_4} [] [] {n : } {v : } (hle : m n) {i : Set α} (hi : ) :
(v.trim hle) i = v i
theorem MeasureTheory.VectorMeasure.restrict_trim {α : Type u_1} {m : } {M : Type u_4} [] [] {n : } {v : } (hle : m n) {i : Set α} (hi : ) :
(v.trim hle).restrict i = (v.restrict i).trim hle
def MeasureTheory.SignedMeasure.toMeasureOfZeroLE' {α : Type u_1} {m : } (s : ) (i : Set α) (j : Set α) (hj : ) :

The underlying function for SignedMeasure.toMeasureOfZeroLE.

Equations
• s.toMeasureOfZeroLE' i hi j hj = ⟨,
Instances For
def MeasureTheory.SignedMeasure.toMeasureOfZeroLE {α : Type u_1} {m : } (s : ) (i : Set α) (hi₁ : ) :

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 : } (s : ) {i : Set α} {j : Set α} (hi₁ : ) (hj₁ : ) :
(s.toMeasureOfZeroLE i hi₁ hi) j = s (i j),
def MeasureTheory.SignedMeasure.toMeasureOfLEZero {α : Type u_1} {m : } (s : ) (i : Set α) (hi₁ : ) :

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 : } (s : ) {i : Set α} {j : Set α} (hi₁ : ) (hj₁ : ) :
(s.toMeasureOfLEZero i hi₁ hi) j = -s (i j),
instance MeasureTheory.SignedMeasure.toMeasureOfZeroLE_finite {α : Type u_1} {m : } (s : ) {i : Set α} (hi₁ : ) :
MeasureTheory.IsFiniteMeasure (s.toMeasureOfZeroLE i hi₁ hi)

SignedMeasure.toMeasureOfZeroLE is a finite measure.

Equations
• =
instance MeasureTheory.SignedMeasure.toMeasureOfLEZero_finite {α : Type u_1} {m : } (s : ) {i : Set α} (hi₁ : ) :
MeasureTheory.IsFiniteMeasure (s.toMeasureOfLEZero i hi₁ hi)

SignedMeasure.toMeasureOfLEZero is a finite measure.

Equations
• =
theorem MeasureTheory.SignedMeasure.toMeasureOfZeroLE_toSignedMeasure {α : Type u_1} {m : } (s : ) (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 : } (s : ) (hs : MeasureTheory.VectorMeasure.restrict s Set.univ MeasureTheory.VectorMeasure.restrict 0 Set.univ) :
(s.toMeasureOfLEZero Set.univ hs).toSignedMeasure = -s
theorem MeasureTheory.Measure.zero_le_toSignedMeasure {α : Type u_1} {m : } (μ : ) :
0 μ.toSignedMeasure
theorem MeasureTheory.Measure.toSignedMeasure_toMeasureOfZeroLE {α : Type u_1} {m : } (μ : ) :
μ.toSignedMeasure.toMeasureOfZeroLE Set.univ = μ