# mathlibdocumentation

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 #

• `measure_theory.vector_measure` is a vector valued, σ-additive function that maps the empty and non-measurable set to zero.
• `measure_theory.vector_measure.map` is the pushforward of a vector measure along a function.
• `measure_theory.vector_measure.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 `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) (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.

def measure_theory.signed_measure (α : Type u_1)  :
Type u_1

A `signed_measure` is a `ℝ`-vector measure.

def measure_theory.complex_measure (α : Type u_1)  :
Type u_1

A `complex_measure` is a `ℂ`-vector_measure.

@[protected, instance]
def measure_theory.vector_measure.has_coe_to_fun {α : Type u_1} {m : measurable_space α} {M : Type u_3}  :
(λ (_x : , set α → M)
Equations
@[simp]
theorem measure_theory.vector_measure.measure_of_eq_coe {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v : M) :
@[simp]
theorem measure_theory.vector_measure.empty {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v : M) :
v = 0
theorem measure_theory.vector_measure.not_measurable {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v : M) {i : set α} (hi : ¬) :
v i = 0
theorem measure_theory.vector_measure.m_Union {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v : 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} [t2_space M] (v : 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.coe_injective {α : Type u_1} {m : measurable_space α} {M : Type u_3}  :
theorem measure_theory.vector_measure.ext_iff' {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v w : 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} (v w : 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} {s t : M} (h : ∀ (i : set α), 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} [t2_space M] {v : 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} [t2_space M] {v : 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} [t2_space M] {v : M} {A B : set α} (h : 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} [t2_space M] {v : 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} [t2_space M] {v : 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} [t2_space M] {v : 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} {v : 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} {v : 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 α} {A B : set α} (h : 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 α} {A B : set α} (h : 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
@[protected, instance]
def measure_theory.vector_measure.has_zero {α : Type u_1} {m : measurable_space α} {M : Type u_3}  :
Equations
@[protected, instance]
def measure_theory.vector_measure.inhabited {α : Type u_1} {m : measurable_space α} {M : Type u_3}  :
Equations
@[simp]
theorem measure_theory.vector_measure.coe_zero {α : Type u_1} {m : measurable_space α} {M : Type u_3}  :
0 = 0
theorem measure_theory.vector_measure.zero_apply {α : Type u_1} {m : measurable_space α} {M : Type u_3} (i : set α) :
0 i = 0
def measure_theory.vector_measure.add {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v w : M) :

The sum of two vector measure is a vector measure.

Equations
@[protected, instance]
def measure_theory.vector_measure.has_add {α : Type u_1} {m : measurable_space α} {M : Type u_3}  :
Equations
@[simp]
theorem measure_theory.vector_measure.coe_add {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v w : M) :
(v + w) = v + w
theorem measure_theory.vector_measure.add_apply {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v w : M) (i : set α) :
(v + w) i = v i + w i
@[protected, instance]
def measure_theory.vector_measure.add_comm_monoid {α : Type u_1} {m : measurable_space α} {M : Type u_3}  :
Equations
def measure_theory.vector_measure.coe_fn_add_monoid_hom {α : Type u_1} {m : measurable_space α} {M : Type u_3}  :
→+ set α → M

`coe_fn` is an `add_monoid_hom`.

Equations
@[simp]
theorem measure_theory.vector_measure.coe_fn_add_monoid_hom_apply {α : Type u_1} {m : measurable_space α} {M : Type u_3} (x : M) (ᾰ : set α) :
def measure_theory.vector_measure.neg {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v : M) :

The negative of a vector measure is a vector measure.

Equations
@[protected, instance]
def measure_theory.vector_measure.has_neg {α : Type u_1} {m : measurable_space α} {M : Type u_3}  :
Equations
@[simp]
theorem measure_theory.vector_measure.coe_neg {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v : M) :
theorem measure_theory.vector_measure.neg_apply {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v : M) (i : set α) :
(-v) i = -v i
def measure_theory.vector_measure.sub {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v w : M) :

The difference of two vector measure is a vector measure.

Equations
@[protected, instance]
def measure_theory.vector_measure.has_sub {α : Type u_1} {m : measurable_space α} {M : Type u_3}  :
Equations
@[simp]
theorem measure_theory.vector_measure.coe_sub {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v w : M) :
(v - w) = v - w
theorem measure_theory.vector_measure.sub_apply {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v w : M) (i : set α) :
(v - w) i = v i - w i
@[protected, instance]
def measure_theory.vector_measure.add_comm_group {α : Type u_1} {m : measurable_space α} {M : Type u_3}  :
Equations
def measure_theory.vector_measure.smul {α : Type u_1} {m : measurable_space α} {M : Type u_3} {R : Type u_4} [semiring R] [ M] [ M] (r : R) (v : M) :

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

Equations
@[protected, instance]
def measure_theory.vector_measure.has_scalar {α : Type u_1} {m : measurable_space α} {M : Type u_3} {R : Type u_4} [semiring R] [ M] [ M] :
Equations
@[simp]
theorem measure_theory.vector_measure.coe_smul {α : Type u_1} {m : measurable_space α} {M : Type u_3} {R : Type u_4} [semiring R] [ M] [ M] (r : R) (v : M) :
(r v) = r v
theorem measure_theory.vector_measure.smul_apply {α : Type u_1} {m : measurable_space α} {M : Type u_3} {R : Type u_4} [semiring R] [ M] [ M] (r : R) (v : M) (i : set α) :
(r v) i = r v i
@[protected, instance]
def measure_theory.vector_measure.distrib_mul_action {α : Type u_1} {m : measurable_space α} {M : Type u_3} {R : Type u_4} [semiring R] [ M] [ M]  :
Equations
@[protected, instance]
def measure_theory.vector_measure.module {α : Type u_1} {m : measurable_space α} {M : Type u_3} {R : Type u_4} [semiring R] [ M] [ M]  :
Equations
@[simp]
noncomputable def measure_theory.measure.to_signed_measure {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α)  :

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

Equations
theorem measure_theory.measure.to_signed_measure_congr {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} (h : μ = ν) :
@[simp]
@[simp]
@[simp]
theorem measure_theory.measure.to_ennreal_vector_measure_apply {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) (i : set α) :
= (μ i) 0
noncomputable def measure_theory.measure.to_ennreal_vector_measure {α : Type u_1} {m : measurable_space α} (μ : measure_theory.measure α) :

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

Equations
theorem measure_theory.measure.to_signed_measure_sub_apply {α : Type u_1} {m : measurable_space α} {μ ν : measure_theory.measure α} {i : set α} (hi : measurable_set i) :
i = (μ i).to_real - (ν i).to_real
noncomputable def measure_theory.vector_measure.ennreal_to_measure {α : Type u_1} {m : measurable_space α}  :

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

Equations
noncomputable def measure_theory.vector_measure.equiv_measure {α : Type u_1}  :

The equiv between `vector_measure α ℝ≥0∞` and `measure α` formed by `measure_theory.vector_measure.ennreal_to_measure` and `measure_theory.measure.to_ennreal_vector_measure`.

Equations
@[simp]
noncomputable def measure_theory.vector_measure.map {α : Type u_1} {β : Type u_2} {M : Type u_3} (v : 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} {M : Type u_3} (v : M) {f : α → β} (hf : ¬) :
v.map f = 0
theorem measure_theory.vector_measure.map_apply {α : Type u_1} {β : Type u_2} {M : Type u_3} (v : 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_id {α : Type u_1} {M : Type u_3} (v : M) :
v.map id = v
@[simp]
theorem measure_theory.vector_measure.map_zero {α : Type u_1} {β : Type u_2} {M : Type u_3} (f : α → β) :
0.map f = 0
def measure_theory.vector_measure.map_range {α : Type u_1} {M : Type u_3} {N : Type u_4} (v : M) (f : M →+ N) (hf : continuous f) :

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} {M : Type u_3} (v : M) {N : Type u_4} {f : M →+ N} (hf : continuous f) {s : set α} :
(v.map_range f hf) s = f (v s)
@[simp]
theorem measure_theory.vector_measure.map_range_id {α : Type u_1} {M : Type u_3} (v : M) :
@[simp]
theorem measure_theory.vector_measure.map_range_zero {α : Type u_1} {M : Type u_3} {N : Type u_4} {f : M →+ N} (hf : continuous f) :
0.map_range f hf = 0
@[simp]
theorem measure_theory.vector_measure.map_range_add {α : Type u_1} {M : Type u_3} {N : Type u_4} {v w : M} {f : M →+ N} (hf : continuous f) :
(v + w).map_range f hf = v.map_range f hf + w.map_range f hf
def measure_theory.vector_measure.map_range_hom {α : Type u_1} {M : Type u_3} {N : Type u_4} (f : M →+ N) (hf : continuous f) :

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
def measure_theory.vector_measure.map_rangeₗ {α : Type u_1} {M : Type u_3} {N : Type u_4} {R : Type u_5} [semiring R] [ M] [ N] [ M] [ N] (f : M →ₗ[R] N) (hf : continuous f) :

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
noncomputable def measure_theory.vector_measure.restrict {α : Type u_1} {M : Type u_3} (v : M) (i : set α) :

The restriction of a vector measure on some set.

Equations
theorem measure_theory.vector_measure.restrict_not_measurable {α : Type u_1} {M : Type u_3} (v : M) {i : set α} (hi : ¬) :
v.restrict i = 0
theorem measure_theory.vector_measure.restrict_apply {α : Type u_1} {M : Type u_3} (v : 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} {M : Type u_3} (v : 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_empty {α : Type u_1} {M : Type u_3} (v : M) :
= 0
@[simp]
theorem measure_theory.vector_measure.restrict_univ {α : Type u_1} {M : Type u_3} (v : M) :
@[simp]
theorem measure_theory.vector_measure.restrict_zero {α : Type u_1} {M : Type u_3} {i : set α} :
0.restrict i = 0
theorem measure_theory.vector_measure.map_add {α : Type u_1} {β : Type u_2} {M : Type u_3} (v w : M) (f : α → β) :
(v + w).map f = v.map f + w.map f
@[simp]
theorem measure_theory.vector_measure.map_gm_apply {α : Type u_1} {β : Type u_2} {M : Type u_3} (f : α → β) (v : M) :
noncomputable def measure_theory.vector_measure.map_gm {α : Type u_1} {β : Type u_2} {M : Type u_3} (f : α → β) :

`vector_measure.map` as an additive monoid homomorphism.

Equations
theorem measure_theory.vector_measure.restrict_add {α : Type u_1} {M : Type u_3} (v w : M) (i : set α) :
(v + w).restrict i = v.restrict i + w.restrict i
@[simp]
theorem measure_theory.vector_measure.restrict_gm_apply {α : Type u_1} {M : Type u_3} (i : set α) (v : M) :
noncomputable def measure_theory.vector_measure.restrict_gm {α : Type u_1} {M : Type u_3} (i : set α) :

`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 α} {M : Type u_3} {R : Type u_4} [semiring R] [ M] [ M] {v : 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} {R : Type u_4} [semiring R] [ M] [ M] {v : 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 α} {M : Type u_3} {R : Type u_4} [semiring R] [ M] [ M] (f : α → β) (v : M) :
= v.map f
noncomputable def measure_theory.vector_measure.mapₗ {α : Type u_1} {β : Type u_2} {m : measurable_space α} {M : Type u_3} {R : Type u_4} [semiring R] [ M] [ M] (f : α → β) :

`vector_measure.map` as a linear map.

Equations
@[simp]
theorem measure_theory.vector_measure.restrictₗ_apply {α : Type u_1} {m : measurable_space α} {M : Type u_3} {R : Type u_4} [semiring R] [ M] [ M] (i : set α) (v : M) :
noncomputable def measure_theory.vector_measure.restrictₗ {α : Type u_1} {m : measurable_space α} {M : Type u_3} {R : Type u_4} [semiring R] [ M] [ M] (i : set α) :

`vector_measure.restrict` as an additive monoid homomorphism.

Equations
@[protected, instance]
def measure_theory.vector_measure.partial_order {α : Type u_1} {m : measurable_space α} {M : Type u_3}  :

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} {v w : M} :
v w ∀ (i : set α), v i w i
theorem measure_theory.vector_measure.le_iff' {α : Type u_1} {m : measurable_space α} {M : Type u_3} {v w : 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} (v w : M) {i : set α} (hi : measurable_set i) :
v.restrict i w.restrict i ∀ ⦃j : set α⦄, j 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} (v w : 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} (v w : M) {i : set α} (h : ∀ ⦃j : set α⦄, j iv j w j) :
theorem measure_theory.vector_measure.restrict_le_restrict_subset {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v w : M) {i j : set α} (hi₁ : measurable_set i) (hi₂ : v.restrict i w.restrict i) (hij : j i) :
theorem measure_theory.vector_measure.le_restrict_empty {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v w : M) :
theorem measure_theory.vector_measure.le_restrict_univ_iff_le {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v w : M) :
v w
theorem measure_theory.vector_measure.neg_le_neg {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v w : M) {i : set α} (hi : measurable_set i) (h : v.restrict i w.restrict i) :
(-w).restrict i (-v).restrict i
@[simp]
theorem measure_theory.vector_measure.neg_le_neg_iff {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v w : M) {i : set α} (hi : measurable_set i) :
theorem measure_theory.vector_measure.restrict_le_restrict_Union {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v w : 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} (v w : 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} (v w : 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.nonneg_of_zero_le_restrict {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v : M) {i : set α} (hi₂ : 0.restrict i v.restrict i) :
0 v i
theorem measure_theory.vector_measure.nonpos_of_restrict_le_zero {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v : M) {i : set α} (hi₂ : v.restrict i 0.restrict i) :
v i 0
theorem measure_theory.vector_measure.zero_le_restrict_not_measurable {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v : M) {i : set α} (hi : ¬) :
theorem measure_theory.vector_measure.restrict_le_zero_of_not_measurable {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v : M) {i : set α} (hi : ¬) :
theorem measure_theory.vector_measure.measurable_of_not_zero_le_restrict {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v : M) {i : set α} (hi : ¬0.restrict i v.restrict i) :
theorem measure_theory.vector_measure.measurable_of_not_restrict_le_zero {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v : M) {i : set α} (hi : ¬v.restrict i 0.restrict i) :
theorem measure_theory.vector_measure.zero_le_restrict_subset {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v : 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} (v : M) {i j : set α} (hi₁ : measurable_set i) (hij : j i) (hi₂ : v.restrict i 0.restrict i) :
theorem measure_theory.vector_measure.exists_pos_measure_of_not_restrict_le_zero {α : Type u_1} {m : measurable_space α} {M : Type u_3} (v : M) {i : set α} (hi : ¬v.restrict i 0.restrict i) :
∃ (j : set α), j i 0 < v j
@[protected, instance]
def measure_theory.vector_measure.covariant_add_le {α : Type u_1} {m : measurable_space α} {M : Type u_3}  :
def measure_theory.vector_measure.absolutely_continuous {α : Type u_1} {m : measurable_space α} {M : Type u_4} {N : Type u_5} (v : M) (w : N) :
Prop

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} {v : M} {w : N} (h : ∀ ⦃s : set α⦄, w s = 0v s = 0) :
v ≪ᵥ w
theorem measure_theory.vector_measure.absolutely_continuous.eq {α : Type u_1} {m : measurable_space α} {M : Type u_4} {v w : M} (h : v = w) :
v ≪ᵥ w
theorem measure_theory.vector_measure.absolutely_continuous.refl {α : Type u_1} {m : measurable_space α} {M : Type u_4} (v : M) :
v ≪ᵥ v
theorem measure_theory.vector_measure.absolutely_continuous.trans {α : Type u_1} {m : measurable_space α} {L : Type u_3} {M : Type u_4} {N : Type u_5} {v : M} {w : N} {u : L} (huv : u ≪ᵥ v) (hvw : v ≪ᵥ w) :
u ≪ᵥ w
theorem measure_theory.vector_measure.absolutely_continuous.zero {α : Type u_1} {m : measurable_space α} {M : Type u_4} {N : Type u_5} (v : N) :
0 ≪ᵥ v
theorem measure_theory.vector_measure.absolutely_continuous.neg_left {α : Type u_1} {m : measurable_space α} {N : Type u_5} {M : Type u_2} {v : M} {w : N} (h : v ≪ᵥ w) :
theorem measure_theory.vector_measure.absolutely_continuous.neg_right {α : Type u_1} {m : measurable_space α} {M : Type u_4} {N : Type u_2} {v : M} {w : N} (h : v ≪ᵥ w) :
theorem measure_theory.vector_measure.absolutely_continuous.add {α : Type u_1} {m : measurable_space α} {M : Type u_4} {N : Type u_5} {v₁ v₂ : M} {w : 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} {M : Type u_2} {v₁ v₂ : M} {w : N} (hv₁ : v₁ ≪ᵥ w) (hv₂ : v₂ ≪ᵥ w) :
v₁ - v₂ ≪ᵥ w
theorem measure_theory.vector_measure.absolutely_continuous.smul {α : Type u_1} {m : measurable_space α} {M : Type u_4} {N : Type u_5} {R : Type u_2} [semiring R] [ M] [ M] {r : R} {v : M} {w : N} (h : v ≪ᵥ w) :
r 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} {v : M} {w : N} (h : v ≪ᵥ w) (f : α → β) :
v.map f ≪ᵥ w.map f
theorem measure_theory.vector_measure.absolutely_continuous.ennreal_to_measure {α : Type u_1} {m : measurable_space α} {M : Type u_4} {v : M}  :
(∀ ⦃s : set α⦄, (μ.ennreal_to_measure) s = 0v s = 0) v ≪ᵥ μ
def measure_theory.vector_measure.mutually_singular {α : Type u_1} {m : measurable_space α} {M : Type u_4} {N : Type u_5} (v : M) (w : N) :
Prop

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} {v : M} {w : N} (s : set α) (hs : measurable_set s) (h₁ : ∀ (t : set α), t sv t = 0) (h₂ : ∀ (t : set α), t sw t = 0) :
v ⊥ᵥ w
theorem measure_theory.vector_measure.mutually_singular.symm {α : Type u_1} {m : measurable_space α} {M : Type u_4} {N : Type u_5} {v : M} {w : N} (h : v ⊥ᵥ w) :
w ⊥ᵥ v
theorem measure_theory.vector_measure.mutually_singular.zero_right {α : Type u_1} {m : measurable_space α} {M : Type u_4} {N : Type u_5} {v : M} :
v ⊥ᵥ 0
theorem measure_theory.vector_measure.mutually_singular.zero_left {α : Type u_1} {m : measurable_space α} {M : Type u_4} {N : Type u_5} {w : N} :
0 ⊥ᵥ w
theorem measure_theory.vector_measure.mutually_singular.add_left {α : Type u_1} {m : measurable_space α} {M : Type u_4} {N : Type u_5} {v₁ v₂ : M} {w : N} [t2_space N] (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} {v : M} {w₁ w₂ : N} [t2_space M] (h₁ : v ⊥ᵥ w₁) (h₂ : v ⊥ᵥ w₂) :
v ⊥ᵥ w₁ + w₂
theorem measure_theory.vector_measure.mutually_singular.smul_right {α : Type u_1} {m : measurable_space α} {M : Type u_4} {N : Type u_5} {v : M} {w : N} {R : Type u_2} [semiring R] [ N] [ N] (r : R) (h : v ⊥ᵥ w) :
v ⊥ᵥ r w
theorem measure_theory.vector_measure.mutually_singular.smul_left {α : Type u_1} {m : measurable_space α} {M : Type u_4} {N : Type u_5} {v : M} {w : N} {R : Type u_2} [semiring R] [ M] [ M] (r : R) (h : v ⊥ᵥ w) :
r v ⊥ᵥ w
theorem measure_theory.vector_measure.mutually_singular.neg_left {α : Type u_1} {m : measurable_space α} {N : Type u_5} {M : Type u_2} {v : M} {w : N} (h : v ⊥ᵥ w) :
theorem measure_theory.vector_measure.mutually_singular.neg_right {α : Type u_1} {m : measurable_space α} {M : Type u_4} {N : Type u_2} {v : M} {w : N} (h : v ⊥ᵥ w) :
@[simp]
theorem measure_theory.vector_measure.mutually_singular.neg_left_iff {α : Type u_1} {m : measurable_space α} {N : Type u_5} {M : Type u_2} {v : M} {w : N} :
@[simp]
theorem measure_theory.vector_measure.mutually_singular.neg_right_iff {α : Type u_1} {m : measurable_space α} {M : Type u_4} {N : Type u_2} {v : M} {w : N} :
noncomputable def measure_theory.vector_measure.trim {α : Type u_1} {M : Type u_4} {m n : measurable_space α} (v : M) (hle : m n) :

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} {m n : measurable_space α} (v : M) (hle : m n) (i : set α) :
(v.trim hle) i = (v i) 0
theorem measure_theory.vector_measure.trim_eq_self {α : Type u_1} {M : Type u_4} {n : measurable_space α} {v : M} :
= v
@[simp]
theorem measure_theory.vector_measure.zero_trim {α : Type u_1} {m : measurable_space α} {M : Type u_4} {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} {n : measurable_space α} {v : 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} {n : measurable_space α} {v : M} (hle : m n) {i : set α} (hi : measurable_set i) :
(v.trim hle).restrict i = (v.restrict i).trim hle
noncomputable def measure_theory.signed_measure.to_measure_of_zero_le' {α : Type u_1} {m : measurable_space α} (i : set α) (hi : 0.restrict i ) (j : set α) (hj : measurable_set j) :

The underlying function for `signed_measure.to_measure_of_zero_le`.

Equations
noncomputable def measure_theory.signed_measure.to_measure_of_zero_le {α : Type u_1} {m : measurable_space α} (i : set α) (hi₁ : measurable_set i) (hi₂ : 0.restrict i ) :

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
• hi₁ hi₂ =
theorem measure_theory.signed_measure.to_measure_of_zero_le_apply {α : Type u_1} {m : measurable_space α} {i j : set α} (hi : 0.restrict i ) (hi₁ : measurable_set i) (hj₁ : measurable_set j) :
hi₁ hi) j = s (i j), _⟩
noncomputable def measure_theory.signed_measure.to_measure_of_le_zero {α : Type u_1} {m : measurable_space α} (i : set α) (hi₁ : measurable_set i) (hi₂ : 0.restrict i) :

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
• hi₁ hi₂ = hi₁ _
theorem measure_theory.signed_measure.to_measure_of_le_zero_apply {α : Type u_1} {m : measurable_space α} {i j : set α} (hi : 0.restrict i) (hi₁ : measurable_set i) (hj₁ : measurable_set j) :
hi₁ hi) j = -s (i j), _⟩
@[protected, instance]
def measure_theory.signed_measure.to_measure_of_zero_le_finite {α : Type u_1} {m : measurable_space α} {i : set α} (hi : 0.restrict i ) (hi₁ : measurable_set i) :

`signed_measure.to_measure_of_zero_le` is a finite measure.

@[protected, instance]
def measure_theory.signed_measure.to_measure_of_le_zero_finite {α : Type u_1} {m : measurable_space α} {i : set α} (hi : 0.restrict i) (hi₁ : measurable_set i) :

`signed_measure.to_measure_of_le_zero` is a finite measure.