mathlib documentation

measure_theory.measure.vector_measure

Vector valued measures #

This file defines vector valued measures, which are σ-additive functions from a set to a 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 signed_measure α. Similarly, when M = ℂ, we call the measure a complex measure and write complex_measure α.

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 has_sum instead of tsum in the definition of vector measures in comparison to measure since this provides summablity.

Tags #

vector measure, signed measure, complex measure

structure measure_theory.vector_measure (α : Type u_3) [measurable_space α] (M : Type u_4) [add_comm_monoid M] [topological_space 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.

def measure_theory.signed_measure (α : Type u_1) [measurable_space α] :
Type u_1

A signed_measure is a -vector measure.

def measure_theory.complex_measure (α : Type u_1) [measurable_space α] :
Type u_1

A complex_measure is a -vector_measure.

@[simp]
theorem measure_theory.vector_measure.empty {α : Type u_1} {m : measurable_space α} {M : Type u_3} [add_comm_monoid M] [topological_space M] (v : measure_theory.vector_measure α M) :
v = 0
theorem measure_theory.vector_measure.not_measurable {α : Type u_1} {m : measurable_space α} {M : Type u_3} [add_comm_monoid M] [topological_space M] (v : measure_theory.vector_measure α M) {i : set α} (hi : ¬measurable_set i) :
v i = 0
theorem measure_theory.vector_measure.m_Union {α : Type u_1} {m : measurable_space α} {M : Type u_3} [add_comm_monoid M] [topological_space M] (v : measure_theory.vector_measure α M) {f : set α} (hf₁ : ∀ (i : ), measurable_set (f i)) (hf₂ : pairwise (disjoint on f)) :
has_sum (λ (i : ), v (f i)) (v (⋃ (i : ), f i))
theorem measure_theory.vector_measure.of_disjoint_Union_nat {α : Type u_1} {m : measurable_space α} {M : Type u_3} [add_comm_monoid M] [topological_space M] [t2_space M] (v : measure_theory.vector_measure α M) {f : set α} (hf₁ : ∀ (i : ), measurable_set (f i)) (hf₂ : pairwise (disjoint on f)) :
v (⋃ (i : ), f i) = ∑' (i : ), v (f i)
theorem measure_theory.vector_measure.ext_iff' {α : Type u_1} {m : measurable_space α} {M : Type u_3} [add_comm_monoid M] [topological_space M] (v w : measure_theory.vector_measure α M) :
v = w ∀ (i : set α), v i = w i
theorem measure_theory.vector_measure.ext_iff {α : Type u_1} {m : measurable_space α} {M : Type u_3} [add_comm_monoid M] [topological_space M] (v w : measure_theory.vector_measure α M) :
v = w ∀ (i : set α), measurable_set iv i = w i
@[ext]
theorem measure_theory.vector_measure.ext {α : Type u_1} {m : measurable_space α} {M : Type u_3} [add_comm_monoid M] [topological_space M] {s t : measure_theory.vector_measure α M} (h : ∀ (i : set α), measurable_set is i = t i) :
s = t
theorem measure_theory.vector_measure.has_sum_of_disjoint_Union {α : Type u_1} {β : Type u_2} {m : measurable_space α} {M : Type u_3} [add_comm_monoid M] [topological_space M] [t2_space M] {v : measure_theory.vector_measure α M} [encodable β] {f : β → set α} (hf₁ : ∀ (i : β), measurable_set (f i)) (hf₂ : pairwise (disjoint on f)) :
has_sum (λ (i : β), v (f i)) (v (⋃ (i : β), f i))
theorem measure_theory.vector_measure.of_disjoint_Union {α : Type u_1} {β : Type u_2} {m : measurable_space α} {M : Type u_3} [add_comm_monoid M] [topological_space M] [t2_space M] {v : measure_theory.vector_measure α M} [encodable β] {f : β → set α} (hf₁ : ∀ (i : β), measurable_set (f i)) (hf₂ : pairwise (disjoint on f)) :
v (⋃ (i : β), f i) = ∑' (i : β), v (f i)
theorem measure_theory.vector_measure.of_union {α : Type u_1} {m : measurable_space α} {M : Type u_3} [add_comm_monoid M] [topological_space M] [t2_space M] {v : measure_theory.vector_measure α M} {A B : set α} (h : disjoint A B) (hA : measurable_set A) (hB : measurable_set B) :
v (A B) = v A + v B
theorem measure_theory.vector_measure.of_add_of_diff {α : Type u_1} {m : measurable_space α} {M : Type u_3} [add_comm_monoid M] [topological_space M] [t2_space M] {v : measure_theory.vector_measure α M} {A B : set α} (hA : measurable_set A) (hB : measurable_set B) (h : A B) :
v A + v (B \ A) = v B
theorem measure_theory.vector_measure.of_diff {α : Type u_1} {m : measurable_space α} {M : Type u_2} [add_comm_group M] [topological_space M] [t2_space M] {v : measure_theory.vector_measure α M} {A B : set α} (hA : measurable_set A) (hB : measurable_set B) (h : A B) :
v (B \ A) = v B - v A
theorem measure_theory.vector_measure.of_diff_of_diff_eq_zero {α : Type u_1} {m : measurable_space α} {M : Type u_3} [add_comm_monoid M] [topological_space M] [t2_space M] {v : measure_theory.vector_measure α M} {A B : set α} (hA : measurable_set A) (hB : measurable_set B) (h' : v (B \ A) = 0) :
v (A \ B) + v B = v A
theorem measure_theory.vector_measure.of_Union_nonneg {α : Type u_1} {m : measurable_space α} {f : set α} {M : Type u_2} [topological_space M] [ordered_add_comm_monoid M] [order_closed_topology M] {v : measure_theory.vector_measure α M} (hf₁ : ∀ (i : ), measurable_set (f i)) (hf₂ : pairwise (disjoint on f)) (hf₃ : ∀ (i : ), 0 v (f i)) :
0 v (⋃ (i : ), f i)
theorem measure_theory.vector_measure.of_Union_nonpos {α : Type u_1} {m : measurable_space α} {f : set α} {M : Type u_2} [topological_space M] [ordered_add_comm_monoid M] [order_closed_topology M] {v : measure_theory.vector_measure α M} (hf₁ : ∀ (i : ), measurable_set (f i)) (hf₂ : pairwise (disjoint on f)) (hf₃ : ∀ (i : ), v (f i) 0) :
v (⋃ (i : ), f i) 0
theorem measure_theory.vector_measure.of_nonneg_disjoint_union_eq_zero {α : Type u_1} {m : measurable_space α} {s : measure_theory.signed_measure α} {A B : set α} (h : disjoint A B) (hA₁ : measurable_set A) (hB₁ : measurable_set B) (hA₂ : 0 s A) (hB₂ : 0 s B) (hAB : s (A B) = 0) :
s A = 0
theorem measure_theory.vector_measure.of_nonpos_disjoint_union_eq_zero {α : Type u_1} {m : measurable_space α} {s : measure_theory.signed_measure α} {A B : set α} (h : disjoint A B) (hA₁ : measurable_set A) (hB₁ : measurable_set B) (hA₂ : s A 0) (hB₂ : s B 0) (hAB : s (A B) = 0) :
s A = 0
@[simp]
theorem measure_theory.vector_measure.coe_zero {α : Type u_1} {m : measurable_space α} {M : Type u_3} [add_comm_monoid M] [topological_space M] :
0 = 0
theorem measure_theory.vector_measure.zero_apply {α : Type u_1} {m : measurable_space α} {M : Type u_3} [add_comm_monoid M] [topological_space M] (i : set α) :
0 i = 0

The sum of two vector measure is a vector measure.

Equations
@[simp]
theorem measure_theory.vector_measure.coe_add {α : Type u_1} {m : measurable_space α} {M : Type u_3} [add_comm_monoid M] [topological_space M] [has_continuous_add M] (v w : measure_theory.vector_measure α M) :
(v + w) = v + w
theorem measure_theory.vector_measure.add_apply {α : Type u_1} {m : measurable_space α} {M : Type u_3} [add_comm_monoid M] [topological_space M] [has_continuous_add M] (v w : measure_theory.vector_measure α M) (i : set α) :
(v + w) i = v i + w i

The negative of a vector measure is a vector measure.

Equations
theorem measure_theory.vector_measure.neg_apply {α : Type u_1} {m : measurable_space α} {M : Type u_3} [add_comm_group M] [topological_space M] [topological_add_group M] (v : measure_theory.vector_measure α M) (i : set α) :
(-v) i = -v i

The difference of two vector measure is a vector measure.

Equations
@[simp]
theorem measure_theory.vector_measure.sub_apply {α : Type u_1} {m : measurable_space α} {M : Type u_3} [add_comm_group M] [topological_space M] [topological_add_group M] (v w : measure_theory.vector_measure α M) (i : set α) :
(v - w) i = v i - w i
@[instance]
Equations

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

Equations
@[simp]
theorem measure_theory.vector_measure.coe_smul {α : Type u_1} {m : measurable_space α} {M : Type u_3} [add_comm_monoid M] [topological_space M] {R : Type u_4} [semiring R] [distrib_mul_action R M] [topological_space R] [has_continuous_smul R M] (r : R) (v : measure_theory.vector_measure α M) :
(r v) = r v
theorem measure_theory.vector_measure.smul_apply {α : Type u_1} {m : measurable_space α} {M : Type u_3} [add_comm_monoid M] [topological_space M] {R : Type u_4} [semiring R] [distrib_mul_action R M] [topological_space R] [has_continuous_smul R M] (r : R) (v : measure_theory.vector_measure α M) (i : set α) :
(r v) i = r v i

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

Equations

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

Equations

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

Equations
def measure_theory.vector_measure.map {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {M : Type u_3} [add_comm_monoid M] [topological_space M] (v : measure_theory.vector_measure α M) (f : α → β) :

The pushforward of a vector measure along a function.

Equations
theorem measure_theory.vector_measure.map_not_measurable {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {M : Type u_3} [add_comm_monoid M] [topological_space M] (v : measure_theory.vector_measure α M) {f : α → β} (hf : ¬measurable f) :
v.map f = 0
theorem measure_theory.vector_measure.map_apply {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {M : Type u_3} [add_comm_monoid M] [topological_space M] (v : measure_theory.vector_measure α M) {f : α → β} (hf : measurable f) {s : set β} (hs : measurable_set s) :
(v.map f) s = v (f ⁻¹' s)
@[simp]
@[simp]
theorem measure_theory.vector_measure.map_zero {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {M : Type u_3} [add_comm_monoid M] [topological_space M] (f : α → β) :
0.map f = 0

The restriction of a vector measure on some set.

Equations
theorem measure_theory.vector_measure.restrict_apply {α : Type u_1} [measurable_space α] {M : Type u_3} [add_comm_monoid M] [topological_space M] (v : measure_theory.vector_measure α M) {i : set α} (hi : measurable_set i) {j : set α} (hj : measurable_set j) :
(v.restrict i) j = v (j i)
theorem measure_theory.vector_measure.restrict_eq_self {α : Type u_1} [measurable_space α] {M : Type u_3} [add_comm_monoid M] [topological_space M] (v : measure_theory.vector_measure α M) {i : set α} (hi : measurable_set i) {j : set α} (hj : measurable_set j) (hij : j i) :
(v.restrict i) j = v j
@[simp]
theorem measure_theory.vector_measure.restrict_zero {α : Type u_1} [measurable_space α] {M : Type u_3} [add_comm_monoid M] [topological_space M] {i : set α} :
0.restrict i = 0
theorem measure_theory.vector_measure.map_add {α : Type u_1} {β : Type u_2} [measurable_space α] [measurable_space β] {M : Type u_3} [add_comm_monoid M] [topological_space M] [has_continuous_add M] (v w : measure_theory.vector_measure α M) (f : α → β) :
(v + w).map f = v.map f + w.map f
@[simp]

vector_measure.map as an additive monoid homomorphism.

Equations

vector_measure.restrict as an additive monoid homomorphism.

Equations
@[simp]
theorem measure_theory.vector_measure.map_smul {α : Type u_1} {β : Type u_2} {m : measurable_space α} [measurable_space β] {M : Type u_3} [add_comm_monoid M] [topological_space M] {R : Type u_4} [semiring R] [distrib_mul_action R M] [topological_space R] [has_continuous_smul R M] {v : measure_theory.vector_measure α M} {f : α → β} (c : R) :
(c v).map f = c v.map f
@[simp]
theorem measure_theory.vector_measure.restrict_smul {α : Type u_1} {m : measurable_space α} {M : Type u_3} [add_comm_monoid M] [topological_space M] {R : Type u_4} [semiring R] [distrib_mul_action R M] [topological_space R] [has_continuous_smul R M] {v : measure_theory.vector_measure α M} {i : set α} (c : R) :
(c v).restrict i = c v.restrict i
@[simp]
theorem measure_theory.vector_measure.mapₗ_apply {α : Type u_1} {β : Type u_2} {m : measurable_space α} [measurable_space β] {M : Type u_3} [add_comm_monoid M] [topological_space M] {R : Type u_4} [semiring R] [module R M] [topological_space R] [has_continuous_smul R M] [has_continuous_add M] (f : α → β) (v : measure_theory.vector_measure α M) :
def measure_theory.vector_measure.mapₗ {α : Type u_1} {β : Type u_2} {m : measurable_space α} [measurable_space β] {M : Type u_3} [add_comm_monoid M] [topological_space M] {R : Type u_4} [semiring R] [module R M] [topological_space R] [has_continuous_smul R M] [has_continuous_add M] (f : α → β) :

vector_measure.map as a linear map.

Equations

vector_measure.restrict as an additive monoid homomorphism.

Equations
@[instance]

Vector measures over a partially ordered monoid is partially ordered.

This definition is consistent with measure.partial_order.

Equations
theorem measure_theory.vector_measure.le_iff {α : Type u_1} {m : measurable_space α} {M : Type u_3} [topological_space M] [add_comm_monoid M] [partial_order M] {v w : measure_theory.vector_measure α M} :
v w ∀ (i : set α), measurable_set iv i w i
theorem measure_theory.vector_measure.le_iff' {α : Type u_1} {m : measurable_space α} {M : Type u_3} [topological_space M] [add_comm_monoid M] [partial_order M] {v w : measure_theory.vector_measure α M} :
v w ∀ (i : set α), v i w i
theorem measure_theory.vector_measure.restrict_le_restrict_iff {α : Type u_1} {m : measurable_space α} {M : Type u_3} [topological_space M] [add_comm_monoid M] [partial_order M] (v w : measure_theory.vector_measure α M) {i : set α} (hi : measurable_set i) :
v.restrict i w.restrict i ∀ ⦃j : set α⦄, measurable_set jj iv j w j
theorem measure_theory.vector_measure.subset_le_of_restrict_le_restrict {α : Type u_1} {m : measurable_space α} {M : Type u_3} [topological_space M] [add_comm_monoid M] [partial_order M] (v w : measure_theory.vector_measure α M) {i : set α} (hi : measurable_set i) (hi₂ : v.restrict i w.restrict i) {j : set α} (hj : j i) :
v j w j
theorem measure_theory.vector_measure.restrict_le_restrict_of_subset_le {α : Type u_1} {m : measurable_space α} {M : Type u_3} [topological_space M] [add_comm_monoid M] [partial_order M] (v w : measure_theory.vector_measure α M) {i : set α} (h : ∀ ⦃j : set α⦄, measurable_set jj iv j w j) :
theorem measure_theory.vector_measure.restrict_le_restrict_subset {α : Type u_1} {m : measurable_space α} {M : Type u_3} [topological_space M] [add_comm_monoid M] [partial_order M] (v w : measure_theory.vector_measure α M) {i j : set α} (hi₁ : measurable_set i) (hi₂ : v.restrict i w.restrict i) (hij : j i) :
theorem measure_theory.vector_measure.restrict_le_restrict_Union {α : Type u_1} {m : measurable_space α} {M : Type u_3} [topological_space M] [ordered_add_comm_monoid M] [order_closed_topology M] (v w : measure_theory.vector_measure α M) {f : set α} (hf₁ : ∀ (n : ), measurable_set (f n)) (hf₂ : ∀ (n : ), v.restrict (f n) w.restrict (f n)) :
v.restrict (⋃ (n : ), f n) w.restrict (⋃ (n : ), f n)
theorem measure_theory.vector_measure.restrict_le_restrict_encodable_Union {α : Type u_1} {β : Type u_2} {m : measurable_space α} {M : Type u_3} [topological_space M] [ordered_add_comm_monoid M] [order_closed_topology M] (v w : measure_theory.vector_measure α M) [encodable β] {f : β → set α} (hf₁ : ∀ (b : β), measurable_set (f b)) (hf₂ : ∀ (b : β), v.restrict (f b) w.restrict (f b)) :
v.restrict (⋃ (b : β), f b) w.restrict (⋃ (b : β), f b)
theorem measure_theory.vector_measure.restrict_le_restrict_union {α : Type u_1} {m : measurable_space α} {M : Type u_3} [topological_space M] [ordered_add_comm_monoid M] [order_closed_topology M] (v w : measure_theory.vector_measure α M) {i j : set α} (hi₁ : measurable_set i) (hi₂ : v.restrict i w.restrict i) (hj₁ : measurable_set j) (hj₂ : v.restrict j w.restrict j) :
v.restrict (i j) w.restrict (i j)
theorem measure_theory.vector_measure.zero_le_restrict_subset {α : Type u_1} {m : measurable_space α} {M : Type u_3} [topological_space M] [ordered_add_comm_monoid M] (v : measure_theory.vector_measure α M) {i j : set α} (hi₁ : measurable_set i) (hij : j i) (hi₂ : 0.restrict i v.restrict i) :
theorem measure_theory.vector_measure.restrict_le_zero_subset {α : Type u_1} {m : measurable_space α} {M : Type u_3} [topological_space M] [ordered_add_comm_monoid M] (v : measure_theory.vector_measure α M) {i j : set α} (hi₁ : measurable_set i) (hij : j i) (hi₂ : v.restrict i 0.restrict i) :

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
theorem measure_theory.vector_measure.absolutely_continuous.mk {α : Type u_1} {m : measurable_space α} {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [topological_space M] [add_comm_monoid N] [topological_space N] {v : measure_theory.vector_measure α M} {w : measure_theory.vector_measure α N} (h : ∀ ⦃s : set α⦄, measurable_set sw s = 0v s = 0) :
v ≪ᵥ w
theorem measure_theory.vector_measure.absolutely_continuous.add {α : Type u_1} {m : measurable_space α} {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [topological_space M] [add_comm_monoid N] [topological_space N] [has_continuous_add M] {v₁ v₂ : measure_theory.vector_measure α M} {w : measure_theory.vector_measure α N} (hv₁ : v₁ ≪ᵥ w) (hv₂ : v₂ ≪ᵥ w) :
v₁ + v₂ ≪ᵥ w
theorem measure_theory.vector_measure.absolutely_continuous.sub {α : Type u_1} {m : measurable_space α} {N : Type u_5} [add_comm_monoid N] [topological_space N] {M : Type u_2} [add_comm_group M] [topological_space M] [topological_add_group M] {v₁ v₂ : measure_theory.vector_measure α M} {w : measure_theory.vector_measure α N} (hv₁ : v₁ ≪ᵥ w) (hv₂ : v₂ ≪ᵥ w) :
v₁ - v₂ ≪ᵥ w
theorem measure_theory.vector_measure.absolutely_continuous.map {α : Type u_1} {β : Type u_2} {m : measurable_space α} {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [topological_space M] [add_comm_monoid N] [topological_space N] {v : measure_theory.vector_measure α M} {w : measure_theory.vector_measure α N} [measure_theory.measure_space β] (h : v ≪ᵥ w) (f : α → β) :
v.map f ≪ᵥ w.map f

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 mutually_singular with the measurability condition, use measure_theory.vector_measure.mutually_singular.mk.

Equations
theorem measure_theory.vector_measure.mutually_singular.mk {α : Type u_1} {m : measurable_space α} {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [topological_space M] [add_comm_monoid N] [topological_space N] {v : measure_theory.vector_measure α M} {w : measure_theory.vector_measure α N} (s : set α) (hs : measurable_set s) (h₁ : ∀ (t : set α), t smeasurable_set tv t = 0) (h₂ : ∀ (t : set α), t smeasurable_set tw t = 0) :
v ⊥ᵥ w
theorem measure_theory.vector_measure.mutually_singular.add_left {α : Type u_1} {m : measurable_space α} {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [topological_space M] [add_comm_monoid N] [topological_space N] {v₁ v₂ : measure_theory.vector_measure α M} {w : measure_theory.vector_measure α N} [t2_space N] [has_continuous_add M] (h₁ : v₁ ⊥ᵥ w) (h₂ : v₂ ⊥ᵥ w) :
v₁ + v₂ ⊥ᵥ w
theorem measure_theory.vector_measure.mutually_singular.add_right {α : Type u_1} {m : measurable_space α} {M : Type u_4} {N : Type u_5} [add_comm_monoid M] [topological_space M] [add_comm_monoid N] [topological_space N] {v : measure_theory.vector_measure α M} {w₁ w₂ : measure_theory.vector_measure α N} [t2_space M] [has_continuous_add N] (h₁ : v ⊥ᵥ w₁) (h₂ : v ⊥ᵥ w₂) :
v ⊥ᵥ w₁ + w₂

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

Equations
@[simp]
theorem measure_theory.vector_measure.trim_apply {α : Type u_1} {M : Type u_4} [add_comm_monoid M] [topological_space M] {m n : measurable_space α} (v : measure_theory.vector_measure α M) (hle : m n) (i : set α) :
(v.trim hle) i = ite (measurable_set i) (v i) 0
@[simp]
theorem measure_theory.vector_measure.zero_trim {α : Type u_1} {m : measurable_space α} {M : Type u_4} [add_comm_monoid M] [topological_space M] {n : measurable_space α} (hle : m n) :
0.trim hle = 0
theorem measure_theory.vector_measure.trim_measurable_set_eq {α : Type u_1} {m : measurable_space α} {M : Type u_4} [add_comm_monoid M] [topological_space M] {n : measurable_space α} {v : measure_theory.vector_measure α M} (hle : m n) {i : set α} (hi : measurable_set i) :
(v.trim hle) i = v i
theorem measure_theory.vector_measure.restrict_trim {α : Type u_1} {m : measurable_space α} {M : Type u_4} [add_comm_monoid M] [topological_space M] {n : measurable_space α} {v : measure_theory.vector_measure α M} (hle : m n) {i : set α} (hi : measurable_set i) :
(v.trim hle).restrict i = (v.restrict i).trim hle

The underlying function for signed_measure.to_measure_of_zero_le.

Equations

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

Equations

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

Equations
@[instance]

signed_measure.to_measure_of_zero_le is a finite measure.

@[instance]

signed_measure.to_measure_of_le_zero is a finite measure.