Relations between vector measures #
This file defines absolute continuity and mutual singularity for vector measures and proves their basic compatibility properties with algebraic operations and pushforwards.
Main definitions #
VectorMeasure.AbsolutelyContinuous, writtenv ≪ᵥ w.VectorMeasure.MutuallySingular, writtenv ⟂ᵥ w.
def
MeasureTheory.VectorMeasure.AbsolutelyContinuous
{α : Type u_1}
{m : MeasurableSpace α}
{M : Type u_4}
{N : Type u_5}
[AddCommMonoid M]
[TopologicalSpace M]
[AddCommMonoid N]
[TopologicalSpace N]
(v : VectorMeasure α M)
(w : VectorMeasure α N)
:
A vector measure v is absolutely continuous with respect to a measure μ if for all sets
s, μ s = 0, we have v s = 0.
Equations
- v.AbsolutelyContinuous w = ∀ ⦃s : Set α⦄, w s = 0 → v s = 0
Instances For
A vector measure v is absolutely continuous with respect to a measure μ if for all sets
s, μ s = 0, we have v s = 0.
Equations
- MeasureTheory.«term_≪ᵥ_» = Lean.ParserDescr.trailingNode `MeasureTheory.«term_≪ᵥ_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≪ᵥ ") (Lean.ParserDescr.cat `term 51))
Instances For
theorem
MeasureTheory.VectorMeasure.AbsolutelyContinuous.mk
{α : Type u_1}
{m : MeasurableSpace α}
{M : Type u_4}
{N : Type u_5}
[AddCommMonoid M]
[TopologicalSpace M]
[AddCommMonoid N]
[TopologicalSpace N]
{v : VectorMeasure α M}
{w : VectorMeasure α N}
(h : ∀ ⦃s : Set α⦄, MeasurableSet s → w s = 0 → v s = 0)
:
theorem
MeasureTheory.VectorMeasure.AbsolutelyContinuous.eq
{α : Type u_1}
{m : MeasurableSpace α}
{M : Type u_4}
[AddCommMonoid M]
[TopologicalSpace M]
{v w : VectorMeasure α M}
(h : v = w)
:
theorem
MeasureTheory.VectorMeasure.AbsolutelyContinuous.refl
{α : Type u_1}
{m : MeasurableSpace α}
{M : Type u_4}
[AddCommMonoid M]
[TopologicalSpace M]
(v : VectorMeasure α M)
:
theorem
MeasureTheory.VectorMeasure.AbsolutelyContinuous.trans
{α : Type u_1}
{m : MeasurableSpace α}
{L : Type u_3}
{M : Type u_4}
{N : Type u_5}
[AddCommMonoid L]
[TopologicalSpace L]
[AddCommMonoid M]
[TopologicalSpace M]
[AddCommMonoid N]
[TopologicalSpace N]
{u : VectorMeasure α L}
{v : VectorMeasure α M}
{w : VectorMeasure α N}
(huv : u.AbsolutelyContinuous v)
(hvw : v.AbsolutelyContinuous w)
:
theorem
MeasureTheory.VectorMeasure.AbsolutelyContinuous.zero
{α : Type u_1}
{m : MeasurableSpace α}
{M : Type u_4}
{N : Type u_5}
[AddCommMonoid M]
[TopologicalSpace M]
[AddCommMonoid N]
[TopologicalSpace N]
(v : VectorMeasure α N)
:
theorem
MeasureTheory.VectorMeasure.AbsolutelyContinuous.neg_left
{α : Type u_1}
{m : MeasurableSpace α}
{N : Type u_5}
[AddCommMonoid N]
[TopologicalSpace N]
{M : Type u_6}
[AddCommGroup M]
[TopologicalSpace M]
[IsTopologicalAddGroup M]
{v : VectorMeasure α M}
{w : VectorMeasure α N}
(h : v.AbsolutelyContinuous w)
:
(-v).AbsolutelyContinuous w
theorem
MeasureTheory.VectorMeasure.AbsolutelyContinuous.neg_right
{α : Type u_1}
{m : MeasurableSpace α}
{M : Type u_4}
[AddCommMonoid M]
[TopologicalSpace M]
{N : Type u_6}
[AddCommGroup N]
[TopologicalSpace N]
[IsTopologicalAddGroup N]
{v : VectorMeasure α M}
{w : VectorMeasure α N}
(h : v.AbsolutelyContinuous w)
:
v.AbsolutelyContinuous (-w)
theorem
MeasureTheory.VectorMeasure.AbsolutelyContinuous.add
{α : Type u_1}
{m : MeasurableSpace α}
{M : Type u_4}
{N : Type u_5}
[AddCommMonoid M]
[TopologicalSpace M]
[AddCommMonoid N]
[TopologicalSpace N]
[ContinuousAdd M]
{v₁ v₂ : VectorMeasure α M}
{w : VectorMeasure α N}
(hv₁ : v₁.AbsolutelyContinuous w)
(hv₂ : v₂.AbsolutelyContinuous w)
:
(v₁ + v₂).AbsolutelyContinuous w
theorem
MeasureTheory.VectorMeasure.AbsolutelyContinuous.sub
{α : Type u_1}
{m : MeasurableSpace α}
{N : Type u_5}
[AddCommMonoid N]
[TopologicalSpace N]
{M : Type u_6}
[AddCommGroup M]
[TopologicalSpace M]
[IsTopologicalAddGroup M]
{v₁ v₂ : VectorMeasure α M}
{w : VectorMeasure α N}
(hv₁ : v₁.AbsolutelyContinuous w)
(hv₂ : v₂.AbsolutelyContinuous w)
:
(v₁ - v₂).AbsolutelyContinuous w
theorem
MeasureTheory.VectorMeasure.AbsolutelyContinuous.smul
{α : Type u_1}
{m : MeasurableSpace α}
{M : Type u_4}
{N : Type u_5}
[AddCommMonoid M]
[TopologicalSpace M]
[AddCommMonoid N]
[TopologicalSpace N]
{R : Type u_6}
[Semiring R]
[DistribMulAction R M]
[ContinuousConstSMul R M]
{r : R}
{v : VectorMeasure α M}
{w : VectorMeasure α N}
(h : v.AbsolutelyContinuous w)
:
(r • v).AbsolutelyContinuous w
theorem
MeasureTheory.VectorMeasure.AbsolutelyContinuous.map
{α : Type u_1}
{β : Type u_2}
{m : MeasurableSpace α}
{M : Type u_4}
{N : Type u_5}
[AddCommMonoid M]
[TopologicalSpace M]
[AddCommMonoid N]
[TopologicalSpace N]
{v : VectorMeasure α M}
{w : VectorMeasure α N}
[MeasureSpace β]
(h : v.AbsolutelyContinuous w)
(f : α → β)
:
(v.map f).AbsolutelyContinuous (w.map f)
theorem
MeasureTheory.VectorMeasure.AbsolutelyContinuous.ennrealToMeasure
{α : Type u_1}
{m : MeasurableSpace α}
{M : Type u_4}
[AddCommMonoid M]
[TopologicalSpace M]
{v : VectorMeasure α M}
{μ : VectorMeasure α ENNReal}
:
def
MeasureTheory.VectorMeasure.MutuallySingular
{α : Type u_1}
{m : MeasurableSpace α}
{M : Type u_4}
{N : Type u_5}
[AddCommMonoid M]
[TopologicalSpace M]
[AddCommMonoid N]
[TopologicalSpace N]
(v : VectorMeasure α M)
(w : VectorMeasure α N)
:
Two vector measures v and w are said to be mutually singular if there exists a measurable
set s, such that for all t ⊆ s, v t = 0 and for all t ⊆ sᶜ, w t = 0.
We note that we do not require the measurability of t in the definition since this makes it easier
to use. This is equivalent to the definition which requires measurability. To prove
MutuallySingular with the measurability condition, use
MeasureTheory.VectorMeasure.MutuallySingular.mk.
Equations
- v.MutuallySingular w = ∃ (s : Set α), MeasurableSet s ∧ (∀ t ⊆ s, v t = 0) ∧ ∀ t ⊆ sᶜ, w t = 0
Instances For
Two vector measures v and w are said to be mutually singular if there exists a measurable
set s, such that for all t ⊆ s, v t = 0 and for all t ⊆ sᶜ, w t = 0.
We note that we do not require the measurability of t in the definition since this makes it easier
to use. This is equivalent to the definition which requires measurability. To prove
MutuallySingular with the measurability condition, use
MeasureTheory.VectorMeasure.MutuallySingular.mk.
Equations
- MeasureTheory.«term_⟂ᵥ_» = Lean.ParserDescr.trailingNode `MeasureTheory.«term_⟂ᵥ_» 60 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟂ᵥ ") (Lean.ParserDescr.cat `term 61))
Instances For
theorem
MeasureTheory.VectorMeasure.MutuallySingular.mk
{α : Type u_1}
{m : MeasurableSpace α}
{M : Type u_4}
{N : Type u_5}
[AddCommMonoid M]
[TopologicalSpace M]
[AddCommMonoid N]
[TopologicalSpace N]
{v : VectorMeasure α M}
{w : VectorMeasure α N}
(s : Set α)
(hs : MeasurableSet s)
(h₁ : ∀ t ⊆ s, MeasurableSet t → v t = 0)
(h₂ : ∀ t ⊆ sᶜ, MeasurableSet t → w t = 0)
:
v.MutuallySingular w
theorem
MeasureTheory.VectorMeasure.MutuallySingular.symm
{α : Type u_1}
{m : MeasurableSpace α}
{M : Type u_4}
{N : Type u_5}
[AddCommMonoid M]
[TopologicalSpace M]
[AddCommMonoid N]
[TopologicalSpace N]
{v : VectorMeasure α M}
{w : VectorMeasure α N}
(h : v.MutuallySingular w)
:
w.MutuallySingular v
theorem
MeasureTheory.VectorMeasure.MutuallySingular.zero_right
{α : Type u_1}
{m : MeasurableSpace α}
{M : Type u_4}
{N : Type u_5}
[AddCommMonoid M]
[TopologicalSpace M]
[AddCommMonoid N]
[TopologicalSpace N]
{v : VectorMeasure α M}
:
v.MutuallySingular 0
theorem
MeasureTheory.VectorMeasure.MutuallySingular.zero_left
{α : Type u_1}
{m : MeasurableSpace α}
{M : Type u_4}
{N : Type u_5}
[AddCommMonoid M]
[TopologicalSpace M]
[AddCommMonoid N]
[TopologicalSpace N]
{w : VectorMeasure α N}
:
MutuallySingular 0 w
theorem
MeasureTheory.VectorMeasure.MutuallySingular.add_left
{α : Type u_1}
{m : MeasurableSpace α}
{M : Type u_4}
{N : Type u_5}
[AddCommMonoid M]
[TopologicalSpace M]
[AddCommMonoid N]
[TopologicalSpace N]
{v₁ v₂ : VectorMeasure α M}
{w : VectorMeasure α N}
[T2Space N]
[ContinuousAdd M]
(h₁ : v₁.MutuallySingular w)
(h₂ : v₂.MutuallySingular w)
:
(v₁ + v₂).MutuallySingular w
theorem
MeasureTheory.VectorMeasure.MutuallySingular.add_right
{α : Type u_1}
{m : MeasurableSpace α}
{M : Type u_4}
{N : Type u_5}
[AddCommMonoid M]
[TopologicalSpace M]
[AddCommMonoid N]
[TopologicalSpace N]
{v : VectorMeasure α M}
{w₁ w₂ : VectorMeasure α N}
[T2Space M]
[ContinuousAdd N]
(h₁ : v.MutuallySingular w₁)
(h₂ : v.MutuallySingular w₂)
:
v.MutuallySingular (w₁ + w₂)
theorem
MeasureTheory.VectorMeasure.MutuallySingular.smul_right
{α : Type u_1}
{m : MeasurableSpace α}
{M : Type u_4}
{N : Type u_5}
[AddCommMonoid M]
[TopologicalSpace M]
[AddCommMonoid N]
[TopologicalSpace N]
{v : VectorMeasure α M}
{w : VectorMeasure α N}
{R : Type u_6}
[Semiring R]
[DistribMulAction R N]
[ContinuousConstSMul R N]
(r : R)
(h : v.MutuallySingular w)
:
v.MutuallySingular (r • w)
theorem
MeasureTheory.VectorMeasure.MutuallySingular.smul_left
{α : Type u_1}
{m : MeasurableSpace α}
{M : Type u_4}
{N : Type u_5}
[AddCommMonoid M]
[TopologicalSpace M]
[AddCommMonoid N]
[TopologicalSpace N]
{v : VectorMeasure α M}
{w : VectorMeasure α N}
{R : Type u_6}
[Semiring R]
[DistribMulAction R M]
[ContinuousConstSMul R M]
(r : R)
(h : v.MutuallySingular w)
:
(r • v).MutuallySingular w
theorem
MeasureTheory.VectorMeasure.MutuallySingular.neg_left
{α : Type u_1}
{m : MeasurableSpace α}
{N : Type u_5}
[AddCommMonoid N]
[TopologicalSpace N]
{M : Type u_6}
[AddCommGroup M]
[TopologicalSpace M]
[IsTopologicalAddGroup M]
{v : VectorMeasure α M}
{w : VectorMeasure α N}
(h : v.MutuallySingular w)
:
(-v).MutuallySingular w
theorem
MeasureTheory.VectorMeasure.MutuallySingular.neg_right
{α : Type u_1}
{m : MeasurableSpace α}
{M : Type u_4}
[AddCommMonoid M]
[TopologicalSpace M]
{N : Type u_6}
[AddCommGroup N]
[TopologicalSpace N]
[IsTopologicalAddGroup N]
{v : VectorMeasure α M}
{w : VectorMeasure α N}
(h : v.MutuallySingular w)
:
v.MutuallySingular (-w)
@[simp]
theorem
MeasureTheory.VectorMeasure.MutuallySingular.neg_left_iff
{α : Type u_1}
{m : MeasurableSpace α}
{N : Type u_5}
[AddCommMonoid N]
[TopologicalSpace N]
{M : Type u_6}
[AddCommGroup M]
[TopologicalSpace M]
[IsTopologicalAddGroup M]
{v : VectorMeasure α M}
{w : VectorMeasure α N}
:
@[simp]
theorem
MeasureTheory.VectorMeasure.MutuallySingular.neg_right_iff
{α : Type u_1}
{m : MeasurableSpace α}
{M : Type u_4}
[AddCommMonoid M]
[TopologicalSpace M]
{N : Type u_6}
[AddCommGroup N]
[TopologicalSpace N]
[IsTopologicalAddGroup N]
{v : VectorMeasure α M}
{w : VectorMeasure α N}
: