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, written v ≪ᵥ w.
• VectorMeasure.MutuallySingular, written v ⟂ᵥ 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) : 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.

def MeasureTheory.«term_≪ᵥ_» : Lean.TrailingParserDescr

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 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) : v.AbsolutelyContinuous w

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) : v.AbsolutelyContinuous w

theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.refl {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [AddCommMonoid M] [TopologicalSpace M] (v : VectorMeasure α M) : v.AbsolutelyContinuous v

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) : u.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) : AbsolutelyContinuous 0 v

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} : (∀ ⦃s : Set α⦄, μ.ennrealToMeasure s = 0 → v s = 0) ↔ v.AbsolutelyContinuous μ

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) : 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 MutuallySingular with the measurability condition, use MeasureTheory.VectorMeasure.MutuallySingular.mk.

def MeasureTheory.«term_⟂ᵥ_» : Lean.TrailingParserDescr

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.

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} : (-v).MutuallySingular w ↔ v.MutuallySingular w

@[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} : v.MutuallySingular (-w) ↔ v.MutuallySingular w