mathlib3 documentation

measure_theory.measure.vector_measure

Vector valued measures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

Instances for measure_theory.vector_measure
@[reducible]

A signed_measure is a -vector measure.

@[reducible]

A complex_measure is a -vector_measure.

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
@[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 i s 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} [countable β] {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} [countable β] {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

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

The negative of a vector measure is a vector measure.

Equations

The difference of two vector measure is a vector measure.

Equations
@[protected, instance]
Equations

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

The pushforward of a vector measure along a function.

Equations
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]
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

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

Equations
@[simp]
theorem measure_theory.vector_measure.map_range_apply {α : Type u_1} [measurable_space α] {M : Type u_3} [add_comm_monoid M] [topological_space M] (v : measure_theory.vector_measure α M) {N : Type u_4} [add_comm_monoid N] [topological_space N] {f : M →+ N} (hf : continuous f) {s : set α} :
(v.map_range f hf) s = f (v s)
@[simp]

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

Equations

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

Equations

The restriction of a vector measure on some set.

Equations
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.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

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] [has_continuous_const_smul R M] {v : measure_theory.vector_measure α M} {f : α β} (c : R) :
(c v).map f = c v.map f
@[simp]

vector_measure.map as a linear map.

Equations

vector_measure.restrict as an additive monoid homomorphism.

Equations
@[protected, 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.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_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_countable_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) [countable β] {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)

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

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

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
Instances for measure_theory.signed_measure.to_measure_of_zero_le

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
Instances for measure_theory.signed_measure.to_measure_of_le_zero
@[protected, instance]

signed_measure.to_measure_of_zero_le is a finite measure.

@[protected, instance]

signed_measure.to_measure_of_le_zero is a finite measure.