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 #
measure_theory.vector_measureis a vector valued, σ-additive function that maps the empty and non-measurable set to zero.measure_theory.vector_measure.mapis the pushforward of a vector measure along a function.measure_theory.vector_measure.restrictis the restriction of a vector measure on some set.
Notation #
v ≤[i] wmeans that the vector measurevrestricted on the setiis less than or equal to the vector measurewrestricted oni, 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)
[measurable_space α]
(M : Type u_4)
[add_comm_monoid M]
[topological_space M] :
Type (max u_3 u_4)
- measure_of' : set α → M
- empty' : self.measure_of' ∅ = 0
- not_measurable' : ∀ ⦃i : set α⦄, ¬measurable_set i → self.measure_of' i = 0
- m_Union' : ∀ ⦃f : ℕ → set α⦄, (∀ (i : ℕ), measurable_set (f i)) → pairwise (disjoint on f) → has_sum (λ (i : ℕ), self.measure_of' (f i)) (self.measure_of' (⋃ (i : ℕ), f i))
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
- measure_theory.vector_measure.has_sizeof_inst
- measure_theory.vector_measure.has_coe_to_fun
- measure_theory.vector_measure.has_smul
- measure_theory.vector_measure.has_zero
- measure_theory.vector_measure.inhabited
- measure_theory.vector_measure.has_add
- measure_theory.vector_measure.add_comm_monoid
- measure_theory.vector_measure.has_neg
- measure_theory.vector_measure.has_sub
- measure_theory.vector_measure.add_comm_group
- measure_theory.vector_measure.distrib_mul_action
- measure_theory.vector_measure.module
- measure_theory.vector_measure.partial_order
- measure_theory.vector_measure.covariant_add_le
@[reducible]
A signed_measure is a ℝ-vector measure.
@[reducible]
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}
[add_comm_monoid M]
[topological_space M] :
has_coe_to_fun (measure_theory.vector_measure α M) (λ (_x : measure_theory.vector_measure α M), set α → M)
Equations
@[simp]
theorem
measure_theory.vector_measure.measure_of_eq_coe
{α : Type u_1}
{m : measurable_space α}
{M : Type u_3}
[add_comm_monoid M]
[topological_space M]
(v : measure_theory.vector_measure α M) :
v.measure_of' = ⇑v
@[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) :
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) :
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)) :
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)) :
theorem
measure_theory.vector_measure.coe_injective
{α : Type u_1}
{m : measurable_space α}
{M : Type u_3}
[add_comm_monoid M]
[topological_space M] :
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) :
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) :
@[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)) :
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)) :
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) :
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) :
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) :
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) :
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)) :
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) :
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) :
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) :
def
measure_theory.vector_measure.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]
[has_continuous_const_smul R M]
(r : R)
(v : measure_theory.vector_measure α 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
- measure_theory.vector_measure.smul r v = {measure_of' := r • ⇑v, empty' := _, not_measurable' := _, m_Union' := _}
@[protected, instance]
def
measure_theory.vector_measure.has_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]
[has_continuous_const_smul R M] :
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]
[has_continuous_const_smul R M]
(r : R)
(v : measure_theory.vector_measure α M) :
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]
[has_continuous_const_smul R M]
(r : R)
(v : measure_theory.vector_measure α M)
(i : set α) :
@[protected, instance]
def
measure_theory.vector_measure.has_zero
{α : Type u_1}
{m : measurable_space α}
{M : Type u_3}
[add_comm_monoid M]
[topological_space M] :
Equations
- measure_theory.vector_measure.has_zero = {zero := {measure_of' := 0, empty' := _, not_measurable' := _, m_Union' := _}}
@[protected, instance]
def
measure_theory.vector_measure.inhabited
{α : Type u_1}
{m : measurable_space α}
{M : Type u_3}
[add_comm_monoid M]
[topological_space M] :
Equations
@[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] :
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 α) :
def
measure_theory.vector_measure.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) :
The sum of two vector measure is a vector measure.
Equations
- v.add w = {measure_of' := ⇑v + ⇑w, empty' := _, not_measurable' := _, m_Union' := _}
@[protected, instance]
def
measure_theory.vector_measure.has_add
{α : Type u_1}
{m : measurable_space α}
{M : Type u_3}
[add_comm_monoid M]
[topological_space M]
[has_continuous_add M] :
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) :
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 α) :
@[protected, instance]
def
measure_theory.vector_measure.add_comm_monoid
{α : Type u_1}
{m : measurable_space α}
{M : Type u_3}
[add_comm_monoid M]
[topological_space M]
[has_continuous_add M] :
Equations
- measure_theory.vector_measure.add_comm_monoid = function.injective.add_comm_monoid coe_fn measure_theory.vector_measure.coe_injective measure_theory.vector_measure.coe_zero measure_theory.vector_measure.coe_add measure_theory.vector_measure.add_comm_monoid._proof_2
def
measure_theory.vector_measure.coe_fn_add_monoid_hom
{α : Type u_1}
{m : measurable_space α}
{M : Type u_3}
[add_comm_monoid M]
[topological_space M]
[has_continuous_add M] :
measure_theory.vector_measure α M →+ 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}
[add_comm_monoid M]
[topological_space M]
[has_continuous_add M]
(x : measure_theory.vector_measure α M)
(ᾰ : set α) :
def
measure_theory.vector_measure.neg
{α : 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) :
The negative of a vector measure is a vector measure.
Equations
- v.neg = {measure_of' := -⇑v, empty' := _, not_measurable' := _, m_Union' := _}
@[protected, instance]
def
measure_theory.vector_measure.has_neg
{α : Type u_1}
{m : measurable_space α}
{M : Type u_3}
[add_comm_group M]
[topological_space M]
[topological_add_group M] :
Equations
@[simp]
theorem
measure_theory.vector_measure.coe_neg
{α : 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) :
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 α) :
def
measure_theory.vector_measure.sub
{α : 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) :
The difference of two vector measure is a vector measure.
Equations
- v.sub w = {measure_of' := ⇑v - ⇑w, empty' := _, not_measurable' := _, m_Union' := _}
@[protected, instance]
def
measure_theory.vector_measure.has_sub
{α : Type u_1}
{m : measurable_space α}
{M : Type u_3}
[add_comm_group M]
[topological_space M]
[topological_add_group M] :
Equations
@[simp]
theorem
measure_theory.vector_measure.coe_sub
{α : 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) :
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 α) :
@[protected, instance]
def
measure_theory.vector_measure.add_comm_group
{α : Type u_1}
{m : measurable_space α}
{M : Type u_3}
[add_comm_group M]
[topological_space M]
[topological_add_group M] :
Equations
- measure_theory.vector_measure.add_comm_group = function.injective.add_comm_group coe_fn measure_theory.vector_measure.add_comm_group._proof_4 measure_theory.vector_measure.add_comm_group._proof_5 measure_theory.vector_measure.add_comm_group._proof_6 measure_theory.vector_measure.coe_neg measure_theory.vector_measure.coe_sub measure_theory.vector_measure.add_comm_group._proof_7 measure_theory.vector_measure.add_comm_group._proof_8
@[protected, instance]
def
measure_theory.vector_measure.distrib_mul_action
{α : 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]
[has_continuous_const_smul R M]
[has_continuous_add M] :
@[protected, instance]
def
measure_theory.vector_measure.module
{α : Type u_1}
{m : measurable_space α}
{M : Type u_3}
[add_comm_monoid M]
[topological_space M]
{R : Type u_4}
[semiring R]
[module R M]
[has_continuous_const_smul R M]
[has_continuous_add M] :
module R (measure_theory.vector_measure α M)
Equations
- measure_theory.vector_measure.module = function.injective.module R measure_theory.vector_measure.coe_fn_add_monoid_hom measure_theory.vector_measure.coe_injective measure_theory.vector_measure.module._proof_1
@[simp]
theorem
measure_theory.measure.to_signed_measure_apply
{α : Type u_1}
{m : measurable_space α}
(μ : measure_theory.measure α)
[hμ : measure_theory.is_finite_measure μ]
(i : set α) :
⇑(μ.to_signed_measure) i = ite (measurable_set i) (μ.to_outer_measure.measure_of i).to_real 0
noncomputable
def
measure_theory.measure.to_signed_measure
{α : Type u_1}
{m : measurable_space α}
(μ : measure_theory.measure α)
[hμ : measure_theory.is_finite_measure μ] :
A finite measure coerced into a real function is a signed measure.
Equations
- μ.to_signed_measure = {measure_of' := λ (i : set α), ite (measurable_set i) (μ.to_outer_measure.measure_of i).to_real 0, empty' := _, not_measurable' := _, m_Union' := _}
theorem
measure_theory.measure.to_signed_measure_apply_measurable
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
[measure_theory.is_finite_measure μ]
{i : set α}
(hi : measurable_set i) :
⇑(μ.to_signed_measure) i = (⇑μ i).to_real
theorem
measure_theory.measure.to_signed_measure_congr
{α : Type u_1}
{m : measurable_space α}
{μ ν : measure_theory.measure α}
[measure_theory.is_finite_measure μ]
[measure_theory.is_finite_measure ν]
(h : μ = ν) :
theorem
measure_theory.measure.to_signed_measure_eq_to_signed_measure_iff
{α : Type u_1}
{m : measurable_space α}
{μ ν : measure_theory.measure α}
[measure_theory.is_finite_measure μ]
[measure_theory.is_finite_measure ν] :
μ.to_signed_measure = ν.to_signed_measure ↔ μ = ν
@[simp]
theorem
measure_theory.measure.to_signed_measure_zero
{α : Type u_1}
{m : measurable_space α} :
0.to_signed_measure = 0
@[simp]
theorem
measure_theory.measure.to_signed_measure_add
{α : Type u_1}
{m : measurable_space α}
(μ ν : measure_theory.measure α)
[measure_theory.is_finite_measure μ]
[measure_theory.is_finite_measure ν] :
(μ + ν).to_signed_measure = μ.to_signed_measure + ν.to_signed_measure
@[simp]
theorem
measure_theory.measure.to_signed_measure_smul
{α : Type u_1}
{m : measurable_space α}
(μ : measure_theory.measure α)
[measure_theory.is_finite_measure μ]
(r : nnreal) :
(r • μ).to_signed_measure = r • μ.to_signed_measure
@[simp]
theorem
measure_theory.measure.to_ennreal_vector_measure_apply
{α : Type u_1}
{m : measurable_space α}
(μ : measure_theory.measure α)
(i : set α) :
⇑(μ.to_ennreal_vector_measure) i = ite (measurable_set i) (⇑μ 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
- μ.to_ennreal_vector_measure = {measure_of' := λ (i : set α), ite (measurable_set i) (⇑μ i) 0, empty' := _, not_measurable' := _, m_Union' := _}
theorem
measure_theory.measure.to_ennreal_vector_measure_apply_measurable
{α : Type u_1}
{m : measurable_space α}
{μ : measure_theory.measure α}
{i : set α}
(hi : measurable_set i) :
⇑(μ.to_ennreal_vector_measure) i = ⇑μ i
@[simp]
theorem
measure_theory.measure.to_ennreal_vector_measure_zero
{α : Type u_1}
{m : measurable_space α} :
@[simp]
theorem
measure_theory.measure.to_ennreal_vector_measure_add
{α : Type u_1}
{m : measurable_space α}
(μ ν : measure_theory.measure α) :
theorem
measure_theory.measure.to_signed_measure_sub_apply
{α : Type u_1}
{m : measurable_space α}
{μ ν : measure_theory.measure α}
[measure_theory.is_finite_measure μ]
[measure_theory.is_finite_measure ν]
{i : set α}
(hi : measurable_set i) :
⇑(μ.to_signed_measure - ν.to_signed_measure) i = (⇑μ i).to_real - (⇑ν i).to_real
noncomputable
def
measure_theory.vector_measure.ennreal_to_measure
{α : Type u_1}
{m : measurable_space α}
(v : measure_theory.vector_measure α ennreal) :
A vector measure over ℝ≥0∞ is a measure.
Equations
- v.ennreal_to_measure = measure_theory.measure.of_measurable (λ (s : set α) (_x : measurable_set s), ⇑v s) _ _
theorem
measure_theory.vector_measure.ennreal_to_measure_apply
{α : Type u_1}
{m : measurable_space α}
{v : measure_theory.vector_measure α ennreal}
{s : set α}
(hs : measurable_set s) :
⇑(v.ennreal_to_measure) s = ⇑v s
@[simp]
theorem
measure_theory.vector_measure.equiv_measure_symm_apply
{α : Type u_1}
[measurable_space α]
(μ : measure_theory.measure α) :
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
- measure_theory.vector_measure.equiv_measure = {to_fun := measure_theory.vector_measure.ennreal_to_measure _inst_1, inv_fun := measure_theory.measure.to_ennreal_vector_measure _inst_1, left_inv := _, right_inv := _}
@[simp]
theorem
measure_theory.vector_measure.equiv_measure_apply
{α : Type u_1}
[measurable_space α]
(v : measure_theory.vector_measure α ennreal) :
noncomputable
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
- v.map f = dite (measurable f) (λ (hf : measurable f), {measure_of' := λ (s : set β), ite (measurable_set s) (⇑v (f ⁻¹' s)) 0, empty' := _, not_measurable' := _, m_Union' := _}) (λ (hf : ¬measurable f), 0)
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) :
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) :
@[simp]
theorem
measure_theory.vector_measure.map_id
{α : Type u_1}
[measurable_space α]
{M : Type u_3}
[add_comm_monoid M]
[topological_space M]
(v : measure_theory.vector_measure α M) :
@[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 : α → β) :
def
measure_theory.vector_measure.map_range
{α : Type u_1}
[measurable_space α]
{M : Type u_3}
[add_comm_monoid M]
[topological_space M]
{N : Type u_4}
[add_comm_monoid N]
[topological_space N]
(v : measure_theory.vector_measure α 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
- v.map_range f hf = {measure_of' := λ (s : set α), ⇑f (⇑v s), empty' := _, not_measurable' := _, m_Union' := _}
@[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 α} :
@[simp]
theorem
measure_theory.vector_measure.map_range_id
{α : Type u_1}
[measurable_space α]
{M : Type u_3}
[add_comm_monoid M]
[topological_space M]
(v : measure_theory.vector_measure α M) :
v.map_range (add_monoid_hom.id M) continuous_id = v
@[simp]
theorem
measure_theory.vector_measure.map_range_zero
{α : Type u_1}
[measurable_space α]
{M : Type u_3}
[add_comm_monoid M]
[topological_space M]
{N : Type u_4}
[add_comm_monoid N]
[topological_space N]
{f : M →+ N}
(hf : continuous ⇑f) :
@[simp]
theorem
measure_theory.vector_measure.map_range_add
{α : Type u_1}
[measurable_space α]
{M : Type u_3}
[add_comm_monoid M]
[topological_space M]
{N : Type u_4}
[add_comm_monoid N]
[topological_space N]
[has_continuous_add M]
[has_continuous_add N]
{v w : measure_theory.vector_measure α M}
{f : M →+ N}
(hf : continuous ⇑f) :
def
measure_theory.vector_measure.map_range_hom
{α : Type u_1}
[measurable_space α]
{M : Type u_3}
[add_comm_monoid M]
[topological_space M]
{N : Type u_4}
[add_comm_monoid N]
[topological_space N]
[has_continuous_add M]
[has_continuous_add N]
(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
- measure_theory.vector_measure.map_range_hom f hf = {to_fun := λ (v : measure_theory.vector_measure α M), v.map_range f hf, map_zero' := _, map_add' := _}
def
measure_theory.vector_measure.map_rangeₗ
{α : Type u_1}
[measurable_space α]
{M : Type u_3}
[add_comm_monoid M]
[topological_space M]
{N : Type u_4}
[add_comm_monoid N]
[topological_space N]
{R : Type u_5}
[semiring R]
[module R M]
[module R N]
[has_continuous_add M]
[has_continuous_add N]
[has_continuous_const_smul R M]
[has_continuous_const_smul R 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
- measure_theory.vector_measure.map_rangeₗ f hf = {to_fun := λ (v : measure_theory.vector_measure α M), v.map_range f.to_add_monoid_hom hf, map_add' := _, map_smul' := _}
noncomputable
def
measure_theory.vector_measure.restrict
{α : Type u_1}
[measurable_space α]
{M : Type u_3}
[add_comm_monoid M]
[topological_space M]
(v : measure_theory.vector_measure α M)
(i : set α) :
The restriction of a vector measure on some set.
Equations
- v.restrict i = dite (measurable_set i) (λ (hi : measurable_set i), {measure_of' := λ (s : set α), ite (measurable_set s) (⇑v (s ∩ i)) 0, empty' := _, not_measurable' := _, m_Union' := _}) (λ (hi : ¬measurable_set i), 0)
theorem
measure_theory.vector_measure.restrict_not_measurable
{α : 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) :
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) :
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) :
@[simp]
theorem
measure_theory.vector_measure.restrict_empty
{α : Type u_1}
[measurable_space α]
{M : Type u_3}
[add_comm_monoid M]
[topological_space M]
(v : measure_theory.vector_measure α M) :
@[simp]
theorem
measure_theory.vector_measure.restrict_univ
{α : Type u_1}
[measurable_space α]
{M : Type u_3}
[add_comm_monoid M]
[topological_space M]
(v : measure_theory.vector_measure α M) :
@[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 α} :
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 : α → β) :
@[simp]
theorem
measure_theory.vector_measure.map_gm_apply
{α : 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]
(f : α → β)
(v : measure_theory.vector_measure α M) :
⇑(measure_theory.vector_measure.map_gm f) v = v.map f
noncomputable
def
measure_theory.vector_measure.map_gm
{α : 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]
(f : α → β) :
vector_measure.map as an additive monoid homomorphism.
Equations
- measure_theory.vector_measure.map_gm f = {to_fun := λ (v : measure_theory.vector_measure α M), v.map f, map_zero' := _, map_add' := _}
theorem
measure_theory.vector_measure.restrict_add
{α : Type u_1}
[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 α) :
@[simp]
theorem
measure_theory.vector_measure.restrict_gm_apply
{α : Type u_1}
[measurable_space α]
{M : Type u_3}
[add_comm_monoid M]
[topological_space M]
[has_continuous_add M]
(i : set α)
(v : measure_theory.vector_measure α M) :
noncomputable
def
measure_theory.vector_measure.restrict_gm
{α : Type u_1}
[measurable_space α]
{M : Type u_3}
[add_comm_monoid M]
[topological_space M]
[has_continuous_add M]
(i : set α) :
vector_measure.restrict as an additive monoid homomorphism.
Equations
- measure_theory.vector_measure.restrict_gm i = {to_fun := λ (v : measure_theory.vector_measure α M), v.restrict i, map_zero' := _, map_add' := _}
@[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) :
@[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]
[has_continuous_const_smul R M]
{v : measure_theory.vector_measure α M}
{i : set α}
(c : R) :
@[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]
[has_continuous_const_smul R M]
[has_continuous_add M]
(f : α → β)
(v : measure_theory.vector_measure α M) :
⇑(measure_theory.vector_measure.mapₗ f) v = v.map f
noncomputable
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]
[has_continuous_const_smul R M]
[has_continuous_add M]
(f : α → β) :
vector_measure.map as a linear map.
Equations
- measure_theory.vector_measure.mapₗ f = {to_fun := λ (v : measure_theory.vector_measure α M), v.map f, map_add' := _, map_smul' := _}
@[simp]
theorem
measure_theory.vector_measure.restrictₗ_apply
{α : Type u_1}
{m : measurable_space α}
{M : Type u_3}
[add_comm_monoid M]
[topological_space M]
{R : Type u_4}
[semiring R]
[module R M]
[has_continuous_const_smul R M]
[has_continuous_add M]
(i : set α)
(v : measure_theory.vector_measure α M) :
noncomputable
def
measure_theory.vector_measure.restrictₗ
{α : Type u_1}
{m : measurable_space α}
{M : Type u_3}
[add_comm_monoid M]
[topological_space M]
{R : Type u_4}
[semiring R]
[module R M]
[has_continuous_const_smul R M]
[has_continuous_add M]
(i : set α) :
vector_measure.restrict as an additive monoid homomorphism.
Equations
- measure_theory.vector_measure.restrictₗ i = {to_fun := λ (v : measure_theory.vector_measure α M), v.restrict i, map_add' := _, map_smul' := _}
@[protected, instance]
def
measure_theory.vector_measure.partial_order
{α : Type u_1}
{m : measurable_space α}
{M : Type u_3}
[topological_space M]
[add_comm_monoid M]
[partial_order M] :
Vector measures over a partially ordered monoid is partially ordered.
This definition is consistent with measure.partial_order.
Equations
- measure_theory.vector_measure.partial_order = {le := λ (v w : measure_theory.vector_measure α M), ∀ (i : set α), measurable_set i → ⇑v i ≤ ⇑w i, lt := preorder.lt._default (λ (v w : measure_theory.vector_measure α M), ∀ (i : set α), measurable_set i → ⇑v i ≤ ⇑w i), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _}
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} :
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} :
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) :
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) :
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 j → 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.le_restrict_empty
{α : 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) :
theorem
measure_theory.vector_measure.le_restrict_univ_iff_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) :
theorem
measure_theory.vector_measure.neg_le_neg
{α : Type u_1}
{m : measurable_space α}
{M : Type u_3}
[topological_space M]
[ordered_add_comm_group M]
[topological_add_group M]
(v w : measure_theory.vector_measure α M)
{i : set α}
(hi : measurable_set i)
(h : v.restrict i ≤ w.restrict i) :
@[simp]
theorem
measure_theory.vector_measure.neg_le_neg_iff
{α : Type u_1}
{m : measurable_space α}
{M : Type u_3}
[topological_space M]
[ordered_add_comm_group M]
[topological_add_group M]
(v w : measure_theory.vector_measure α 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}
[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)) :
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)) :
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) :
theorem
measure_theory.vector_measure.nonneg_of_zero_le_restrict
{α : 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 : set α}
(hi₂ : 0.restrict i ≤ v.restrict i) :
theorem
measure_theory.vector_measure.nonpos_of_restrict_le_zero
{α : 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 : set α}
(hi₂ : v.restrict i ≤ 0.restrict i) :
theorem
measure_theory.vector_measure.zero_le_restrict_not_measurable
{α : 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 : set α}
(hi : ¬measurable_set i) :
theorem
measure_theory.vector_measure.restrict_le_zero_of_not_measurable
{α : 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 : set α}
(hi : ¬measurable_set i) :
theorem
measure_theory.vector_measure.measurable_of_not_zero_le_restrict
{α : 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 : 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}
[topological_space M]
[ordered_add_comm_monoid M]
(v : measure_theory.vector_measure α 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}
[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) :
theorem
measure_theory.vector_measure.exists_pos_measure_of_not_restrict_le_zero
{α : Type u_1}
{m : measurable_space α}
{M : Type u_3}
[topological_space M]
[linear_ordered_add_comm_monoid M]
(v : measure_theory.vector_measure α M)
{i : set α}
(hi : ¬v.restrict i ≤ 0.restrict i) :
@[protected, instance]
def
measure_theory.vector_measure.covariant_add_le
{α : Type u_1}
{m : measurable_space α}
{M : Type u_3}
[topological_space M]
[add_comm_monoid M]
[partial_order M]
[covariant_class M M has_add.add has_le.le]
[has_continuous_add M] :
def
measure_theory.vector_measure.absolutely_continuous
{α : 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) :
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.
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 s → ⇑w s = 0 → ⇑v s = 0) :
theorem
measure_theory.vector_measure.absolutely_continuous.eq
{α : Type u_1}
{m : measurable_space α}
{M : Type u_4}
[add_comm_monoid M]
[topological_space M]
{v w : measure_theory.vector_measure α M}
(h : v = w) :
@[refl]
theorem
measure_theory.vector_measure.absolutely_continuous.refl
{α : Type u_1}
{m : measurable_space α}
{M : Type u_4}
[add_comm_monoid M]
[topological_space M]
(v : measure_theory.vector_measure α M) :
@[trans]
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}
[add_comm_monoid L]
[topological_space L]
[add_comm_monoid M]
[topological_space M]
[add_comm_monoid N]
[topological_space N]
{u : measure_theory.vector_measure α L}
{v : measure_theory.vector_measure α M}
{w : measure_theory.vector_measure α N}
(huv : u.absolutely_continuous v)
(hvw : v.absolutely_continuous w) :
theorem
measure_theory.vector_measure.absolutely_continuous.zero
{α : 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 α N) :
theorem
measure_theory.vector_measure.absolutely_continuous.neg_left
{α : 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 : measure_theory.vector_measure α M}
{w : measure_theory.vector_measure α N}
(h : v.absolutely_continuous w) :
(-v).absolutely_continuous w
theorem
measure_theory.vector_measure.absolutely_continuous.neg_right
{α : Type u_1}
{m : measurable_space α}
{M : Type u_4}
[add_comm_monoid M]
[topological_space M]
{N : Type u_2}
[add_comm_group N]
[topological_space N]
[topological_add_group N]
{v : measure_theory.vector_measure α M}
{w : measure_theory.vector_measure α N}
(h : v.absolutely_continuous w) :
v.absolutely_continuous (-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₁.absolutely_continuous w)
(hv₂ : v₂.absolutely_continuous w) :
(v₁ + v₂).absolutely_continuous 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₁.absolutely_continuous w)
(hv₂ : v₂.absolutely_continuous w) :
(v₁ - v₂).absolutely_continuous w
theorem
measure_theory.vector_measure.absolutely_continuous.smul
{α : 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]
{R : Type u_2}
[semiring R]
[distrib_mul_action R M]
[has_continuous_const_smul R M]
{r : R}
{v : measure_theory.vector_measure α M}
{w : measure_theory.vector_measure α N}
(h : v.absolutely_continuous w) :
(r • v).absolutely_continuous 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.absolutely_continuous w)
(f : α → β) :
(v.map f).absolutely_continuous (w.map f)
theorem
measure_theory.vector_measure.absolutely_continuous.ennreal_to_measure
{α : Type u_1}
{m : measurable_space α}
{M : Type u_4}
[add_comm_monoid M]
[topological_space M]
{v : measure_theory.vector_measure α M}
{μ : measure_theory.vector_measure α ennreal} :
(∀ ⦃s : set α⦄, ⇑(μ.ennreal_to_measure) s = 0 → ⇑v s = 0) ↔ v.absolutely_continuous μ
def
measure_theory.vector_measure.mutually_singular
{α : 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) :
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.
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 ⊆ s → measurable_set t → ⇑v t = 0)
(h₂ : ∀ (t : set α), t ⊆ sᶜ → measurable_set t → ⇑w t = 0) :
theorem
measure_theory.vector_measure.mutually_singular.symm
{α : 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 : v.mutually_singular w) :
theorem
measure_theory.vector_measure.mutually_singular.zero_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} :
theorem
measure_theory.vector_measure.mutually_singular.zero_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]
{w : measure_theory.vector_measure α N} :
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₁.mutually_singular w)
(h₂ : v₂.mutually_singular w) :
(v₁ + v₂).mutually_singular 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.mutually_singular w₁)
(h₂ : v.mutually_singular w₂) :
v.mutually_singular (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}
[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}
{R : Type u_2}
[semiring R]
[distrib_mul_action R N]
[has_continuous_const_smul R N]
(r : R)
(h : v.mutually_singular w) :
v.mutually_singular (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}
[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}
{R : Type u_2}
[semiring R]
[distrib_mul_action R M]
[has_continuous_const_smul R M]
(r : R)
(h : v.mutually_singular w) :
(r • v).mutually_singular w
theorem
measure_theory.vector_measure.mutually_singular.neg_left
{α : 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 : measure_theory.vector_measure α M}
{w : measure_theory.vector_measure α N}
(h : v.mutually_singular w) :
(-v).mutually_singular w
theorem
measure_theory.vector_measure.mutually_singular.neg_right
{α : Type u_1}
{m : measurable_space α}
{M : Type u_4}
[add_comm_monoid M]
[topological_space M]
{N : Type u_2}
[add_comm_group N]
[topological_space N]
[topological_add_group N]
{v : measure_theory.vector_measure α M}
{w : measure_theory.vector_measure α N}
(h : v.mutually_singular w) :
v.mutually_singular (-w)
@[simp]
theorem
measure_theory.vector_measure.mutually_singular.neg_left_iff
{α : 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 : measure_theory.vector_measure α M}
{w : measure_theory.vector_measure α N} :
(-v).mutually_singular w ↔ v.mutually_singular w
@[simp]
theorem
measure_theory.vector_measure.mutually_singular.neg_right_iff
{α : Type u_1}
{m : measurable_space α}
{M : Type u_4}
[add_comm_monoid M]
[topological_space M]
{N : Type u_2}
[add_comm_group N]
[topological_space N]
[topological_add_group N]
{v : measure_theory.vector_measure α M}
{w : measure_theory.vector_measure α N} :
v.mutually_singular (-w) ↔ v.mutually_singular w
noncomputable
def
measure_theory.vector_measure.trim
{α : 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) :
Restriction of a vector measure onto a sub-σ-algebra.
Equations
- v.trim hle = {measure_of' := λ (i : set α), ite (measurable_set i) (⇑v i) 0, empty' := _, not_measurable' := _, m_Union' := _}
@[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 α) :
theorem
measure_theory.vector_measure.trim_eq_self
{α : Type u_1}
{M : Type u_4}
[add_comm_monoid M]
[topological_space M]
{n : measurable_space α}
{v : measure_theory.vector_measure α M} :
@[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) :
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) :
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) :
noncomputable
def
measure_theory.signed_measure.to_measure_of_zero_le'
{α : Type u_1}
{m : measurable_space α}
(s : measure_theory.signed_measure α)
(i : set α)
(hi : 0.restrict i ≤ measure_theory.vector_measure.restrict s i)
(j : set α)
(hj : measurable_set j) :
The underlying function for signed_measure.to_measure_of_zero_le.
Equations
- s.to_measure_of_zero_le' i hi j hj = ↑⟨⇑(measure_theory.vector_measure.restrict s i) j, _⟩
noncomputable
def
measure_theory.signed_measure.to_measure_of_zero_le
{α : Type u_1}
{m : measurable_space α}
(s : measure_theory.signed_measure α)
(i : set α)
(hi₁ : measurable_set i)
(hi₂ : 0.restrict i ≤ measure_theory.vector_measure.restrict s 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
- s.to_measure_of_zero_le i hi₁ hi₂ = measure_theory.measure.of_measurable (s.to_measure_of_zero_le' i hi₂) _ _
Instances for measure_theory.signed_measure.to_measure_of_zero_le
theorem
measure_theory.signed_measure.to_measure_of_zero_le_apply
{α : Type u_1}
{m : measurable_space α}
(s : measure_theory.signed_measure α)
{i j : set α}
(hi : 0.restrict i ≤ measure_theory.vector_measure.restrict s i)
(hi₁ : measurable_set i)
(hj₁ : measurable_set j) :
noncomputable
def
measure_theory.signed_measure.to_measure_of_le_zero
{α : Type u_1}
{m : measurable_space α}
(s : measure_theory.signed_measure α)
(i : set α)
(hi₁ : measurable_set i)
(hi₂ : measure_theory.vector_measure.restrict s i ≤ 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
- s.to_measure_of_le_zero i hi₁ hi₂ = (-s).to_measure_of_zero_le i hi₁ _
Instances for measure_theory.signed_measure.to_measure_of_le_zero
theorem
measure_theory.signed_measure.to_measure_of_le_zero_apply
{α : Type u_1}
{m : measurable_space α}
(s : measure_theory.signed_measure α)
{i j : set α}
(hi : measure_theory.vector_measure.restrict s i ≤ 0.restrict i)
(hi₁ : measurable_set i)
(hj₁ : measurable_set j) :
@[protected, instance]
def
measure_theory.signed_measure.to_measure_of_zero_le_finite
{α : Type u_1}
{m : measurable_space α}
(s : measure_theory.signed_measure α)
{i : set α}
(hi : 0.restrict i ≤ measure_theory.vector_measure.restrict s i)
(hi₁ : measurable_set i) :
measure_theory.is_finite_measure (s.to_measure_of_zero_le i hi₁ hi)
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 α}
(s : measure_theory.signed_measure α)
{i : set α}
(hi : measure_theory.vector_measure.restrict s i ≤ 0.restrict i)
(hi₁ : measurable_set i) :
measure_theory.is_finite_measure (s.to_measure_of_le_zero i hi₁ hi)
signed_measure.to_measure_of_le_zero is a finite measure.
theorem
measure_theory.signed_measure.to_measure_of_zero_le_to_signed_measure
{α : Type u_1}
{m : measurable_space α}
(s : measure_theory.signed_measure α)
(hs : 0.restrict set.univ ≤ measure_theory.vector_measure.restrict s set.univ) :
theorem
measure_theory.signed_measure.to_measure_of_le_zero_to_signed_measure
{α : Type u_1}
{m : measurable_space α}
(s : measure_theory.signed_measure α)
(hs : measure_theory.vector_measure.restrict s set.univ ≤ 0.restrict set.univ) :
theorem
measure_theory.measure.zero_le_to_signed_measure
{α : Type u_1}
{m : measurable_space α}
(μ : measure_theory.measure α)
[measure_theory.is_finite_measure μ] :
0 ≤ μ.to_signed_measure
theorem
measure_theory.measure.to_signed_measure_to_measure_of_zero_le
{α : Type u_1}
{m : measurable_space α}
(μ : measure_theory.measure α)
[measure_theory.is_finite_measure μ] :