Vector-valued measures

This file defines vector-valued measures, which are σ-additive functions from a set to an additive 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 SignedMeasure α. Similarly, when M = ℂ, we call the measure a complex measure and write ComplexMeasure α (defined in MeasureTheory/Measure/Complex).

Main definitions

• MeasureTheory.VectorMeasure is a vector-valued, σ-additive function that maps the empty and non-measurable sets to zero.
• MeasureTheory.VectorMeasure.map is the pushforward of a vector measure along a function.
• MeasureTheory.VectorMeasure.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 HasSum instead of tsum in the definition of vector measures in comparison to Measure since this provides summability.

Tags

vector measure, signed measure, complex measure

structure MeasureTheory.VectorMeasure (α : Type u_3) [MeasurableSpace α] (M : Type u_4) [AddCommMonoid M] [TopologicalSpace M] : Type (max u_3 u_4)

A vector measure on a measurable space α is a σ-additive M-valued function (for some M an additive monoid) such that the empty set and non-measurable sets are mapped to zero.

• measureOf' : Set α → M

  The measure of sets

• empty' : self.measureOf' ∅ = 0

  The empty set has measure zero

• not_measurable' ⦃i : Set α⦄ : ¬MeasurableSet i → self.measureOf' i = 0

  Non-measurable sets have measure zero

• m_iUnion' ⦃f : ℕ → Set α⦄ : (∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Function.onFun Disjoint f) → HasSum (fun (i : ℕ) => self.measureOf' (f i)) (self.measureOf' (⋃ (i : ℕ), f i))

  The measure is σ-additive

@[reducible, inline]

abbrev MeasureTheory.SignedMeasure (α : Type u_3) [MeasurableSpace α] : Type u_3

A SignedMeasure is an ℝ-vector measure.

Equations

• MeasureTheory.SignedMeasure α = MeasureTheory.VectorMeasure α ℝ

@[implicit_reducible]

instance MeasureTheory.VectorMeasure.instFunLikeSet {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] : FunLike (VectorMeasure α M) (Set α) M

Equations

• MeasureTheory.VectorMeasure.instFunLikeSet = { coe := MeasureTheory.VectorMeasure.measureOf', coe_injective := ⋯ }

@[simp]

theorem MeasureTheory.VectorMeasure.coe_mk {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : Set α → M) (h₁ : v ∅ = 0) (h₂ : ∀ ⦃i : Set α⦄, ¬MeasurableSet i → v i = 0) (h₃ : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Function.onFun Disjoint f) → HasSum (fun (i : ℕ) => v (f i)) (v (⋃ (i : ℕ), f i))) : ⇑{ measureOf' := v, empty' := h₁, not_measurable' := h₂, m_iUnion' := h₃ } = v

@[simp]

theorem MeasureTheory.VectorMeasure.empty {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : VectorMeasure α M) : v ∅ = 0

@[simp]

theorem MeasureTheory.VectorMeasure.not_measurable {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : VectorMeasure α M) {i : Set α} (hi : ¬MeasurableSet i) : v i = 0

theorem MeasureTheory.VectorMeasure.m_iUnion {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : VectorMeasure α M) {f : ℕ → Set α} (hf₁ : ∀ (i : ℕ), MeasurableSet (f i)) (hf₂ : Pairwise (Function.onFun Disjoint f)) : HasSum (fun (i : ℕ) => v (f i)) (v (⋃ (i : ℕ), f i))

@[deprecated DFunLike.coe_injective (since := "2026-06-10")]

theorem MeasureTheory.VectorMeasure.coe_injective {F : Sort u_1} {α : outParam (Sort u_2)} {β : outParam (α → Sort u_3)} [self : DFunLike F α β] : Function.Injective DFunLike.coe

Alias of DFunLike.coe_injective.

@[deprecated DFunLike.ext_iff (since := "2026-06-10")]

theorem MeasureTheory.VectorMeasure.ext_iff' {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] {f g : F} : f = g ↔ ∀ (x : α), f x = g x

Alias of DFunLike.ext_iff.

theorem MeasureTheory.VectorMeasure.ext_iff {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v w : VectorMeasure α M) : v = w ↔ ∀ (i : Set α), MeasurableSet i → v i = w i

theorem MeasureTheory.VectorMeasure.ext {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {s t : VectorMeasure α M} (h : ∀ (i : Set α), MeasurableSet i → s i = t i) : s = t

theorem MeasureTheory.VectorMeasure.hasSum_of_disjoint_iUnion {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [Countable β] {v : VectorMeasure α M} {f : β → Set α} (hm : ∀ (i : β), MeasurableSet (f i)) (hd : Pairwise (Function.onFun Disjoint f)) : HasSum (fun (i : β) => v (f i)) (v (⋃ (i : β), f i))

theorem MeasureTheory.VectorMeasure.of_disjoint_iUnion {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [Countable β] {v : VectorMeasure α M} {f : β → Set α} [T2Space M] (hm : ∀ (i : β), MeasurableSet (f i)) (hd : Pairwise (Function.onFun Disjoint f)) : v (⋃ (i : β), f i) = ∑' (i : β), v (f i)

theorem MeasureTheory.VectorMeasure.of_union {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {v : VectorMeasure α M} [T2Space M] {A B : Set α} (h : Disjoint A B) (hA : MeasurableSet A) (hB : MeasurableSet B) : v (A ∪ B) = v A + v B

theorem MeasureTheory.VectorMeasure.of_add_of_sdiff {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {v : VectorMeasure α M} [T2Space M] {A B : Set α} (hA : MeasurableSet A) (hB : MeasurableSet B) (h : A ⊆ B) : v A + v (B \ A) = v B

@[deprecated MeasureTheory.VectorMeasure.of_add_of_sdiff (since := "2026-06-03")]

theorem MeasureTheory.VectorMeasure.of_add_of_diff {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {v : VectorMeasure α M} [T2Space M] {A B : Set α} (hA : MeasurableSet A) (hB : MeasurableSet B) (h : A ⊆ B) : v A + v (B \ A) = v B

Alias of MeasureTheory.VectorMeasure.of_add_of_sdiff.

theorem MeasureTheory.VectorMeasure.of_sdiff {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [AddCommGroup M] [TopologicalSpace M] [T2Space M] {v : VectorMeasure α M} {A B : Set α} (hA : MeasurableSet A) (hB : MeasurableSet B) (h : A ⊆ B) : v (B \ A) = v B - v A

@[deprecated MeasureTheory.VectorMeasure.of_sdiff (since := "2026-06-03")]

theorem MeasureTheory.VectorMeasure.of_diff {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [AddCommGroup M] [TopologicalSpace M] [T2Space M] {v : VectorMeasure α M} {A B : Set α} (hA : MeasurableSet A) (hB : MeasurableSet B) (h : A ⊆ B) : v (B \ A) = v B - v A

Alias of MeasureTheory.VectorMeasure.of_sdiff.

theorem MeasureTheory.VectorMeasure.of_compl {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [AddCommGroup M] [TopologicalSpace M] [T2Space M] {v : VectorMeasure α M} {A : Set α} (hA : MeasurableSet A) : v Aᶜ = v Set.univ - v A

theorem MeasureTheory.VectorMeasure.of_sdiff_of_sdiff_eq_zero {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {v : VectorMeasure α M} [T2Space M] {A B : Set α} (hA : MeasurableSet A) (hB : MeasurableSet B) (h' : v (B \ A) = 0) : v (A \ B) + v B = v A

@[deprecated MeasureTheory.VectorMeasure.of_sdiff_of_sdiff_eq_zero (since := "2026-06-03")]

theorem MeasureTheory.VectorMeasure.of_diff_of_diff_eq_zero {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {v : VectorMeasure α M} [T2Space M] {A B : Set α} (hA : MeasurableSet A) (hB : MeasurableSet B) (h' : v (B \ A) = 0) : v (A \ B) + v B = v A

Alias of MeasureTheory.VectorMeasure.of_sdiff_of_sdiff_eq_zero.

theorem MeasureTheory.VectorMeasure.of_iUnion_nonneg {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [Countable β] {f : β → Set α} {M : Type u_4} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] [OrderClosedTopology M] {v : VectorMeasure α M} (hf₁ : ∀ (i : β), MeasurableSet (f i)) (hf₂ : Pairwise (Function.onFun Disjoint f)) (hf₃ : ∀ (i : β), 0 ≤ v (f i)) : 0 ≤ v (⋃ (i : β), f i)

theorem MeasureTheory.VectorMeasure.of_iUnion_nonpos {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [Countable β] {f : β → Set α} {M : Type u_4} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] [OrderClosedTopology M] {v : VectorMeasure α M} (hf₁ : ∀ (i : β), MeasurableSet (f i)) (hf₂ : Pairwise (Function.onFun Disjoint f)) (hf₃ : ∀ (i : β), v (f i) ≤ 0) : v (⋃ (i : β), f i) ≤ 0

theorem MeasureTheory.VectorMeasure.of_nonneg_disjoint_union_eq_zero {α : Type u_1} {m : MeasurableSpace α} {s : SignedMeasure α} {A B : Set α} (h : Disjoint A B) (hA₁ : MeasurableSet A) (hB₁ : MeasurableSet B) (hA₂ : 0 ≤ s A) (hB₂ : 0 ≤ s B) (hAB : s (A ∪ B) = 0) : s A = 0

theorem MeasureTheory.VectorMeasure.of_nonpos_disjoint_union_eq_zero {α : Type u_1} {m : MeasurableSpace α} {s : SignedMeasure α} {A B : Set α} (h : Disjoint A B) (hA₁ : MeasurableSet A) (hB₁ : MeasurableSet B) (hA₂ : s A ≤ 0) (hB₂ : s B ≤ 0) (hAB : s (A ∪ B) = 0) : s A = 0

theorem MeasureTheory.VectorMeasure.of_biUnion_finset {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {v : VectorMeasure α M} [T2Space M] {ι : Type u_4} {s : Finset ι} {f : ι → Set α} (hd : (↑s).PairwiseDisjoint f) (hm : ∀ b ∈ s, MeasurableSet (f b)) : v (⋃ b ∈ s, f b) = ∑ p ∈ s, v (f p)

theorem MeasureTheory.VectorMeasure.tendsto_vectorMeasure_iUnion_atTop_nat {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {v : VectorMeasure α M} [T2Space M] {s : ℕ → Set α} (hm : Monotone s) (hs : ∀ (i : ℕ), MeasurableSet (s i)) : Filter.Tendsto (fun (n : ℕ) => v (s n)) Filter.atTop (nhds (v (⋃ (n : ℕ), s n)))

theorem MeasureTheory.VectorMeasure.tendsto_vectorMeasure_iInter_atTop_nat {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [AddCommGroup M] [TopologicalSpace M] [T2Space M] [ContinuousSub M] {v : VectorMeasure α M} {s : ℕ → Set α} (hm : Antitone s) (hs : ∀ (i : ℕ), MeasurableSet (s i)) : Filter.Tendsto (fun (n : ℕ) => v (s n)) Filter.atTop (nhds (v (⋂ (n : ℕ), s n)))

@[implicit_reducible]

def MeasureTheory.VectorMeasure.smul {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {R : Type u_4} [Semiring R] [DistribMulAction R M] [ContinuousConstSMul R M] (r : R) (v : VectorMeasure α M) : VectorMeasure α M

Given a scalar r and a vector measure v, smul r v is the vector measure corresponding to the set function s : Set α => r • (v s).

Equations

• MeasureTheory.VectorMeasure.smul r v = { measureOf' := r • ⇑v, empty' := ⋯, not_measurable' := ⋯, m_iUnion' := ⋯ }

@[implicit_reducible]

instance MeasureTheory.VectorMeasure.instSMul {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {R : Type u_4} [Semiring R] [DistribMulAction R M] [ContinuousConstSMul R M] : SMul R (VectorMeasure α M)

Equations

• MeasureTheory.VectorMeasure.instSMul = { smul := MeasureTheory.VectorMeasure.smul }

instance MeasureTheory.VectorMeasure.instIsSMulApplySet {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {R : Type u_4} [Semiring R] [DistribMulAction R M] [ContinuousConstSMul R M] : IsSMulApply R (VectorMeasure α M) (Set α) M

@[deprecated FunLike.coe_smul (since := "2026-06-10")]

theorem MeasureTheory.VectorMeasure.coe_smul {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [FunLike F α β] [SMul M F] [SMul M β] [IsSMulApply M F α β] (n : M) (f : F) : ⇑(n • f) = n • ⇑f

Alias of FunLike.coe_smul.

@[deprecated smul_apply (since := "2026-06-10")]

theorem MeasureTheory.VectorMeasure.smul_apply {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst✝ : FunLike F α β} {inst✝¹ : SMul M β} {inst✝² : SMul M F} [self : IsSMulApply M F α β] (f : F) (r : M) (x : α) : (r • f) x = r • f x

Alias of smul_apply.

@[implicit_reducible]

instance MeasureTheory.VectorMeasure.instZero {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] : Zero (VectorMeasure α M)

Equations

• MeasureTheory.VectorMeasure.instZero = { zero := { measureOf' := 0, empty' := ⋯, not_measurable' := ⋯, m_iUnion' := ⋯ } }

instance MeasureTheory.VectorMeasure.instIsZeroApplySet {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] : IsZeroApply (VectorMeasure α M) (Set α) M

@[implicit_reducible]

instance MeasureTheory.VectorMeasure.instInhabited {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] : Inhabited (VectorMeasure α M)

Equations

• MeasureTheory.VectorMeasure.instInhabited = { default := 0 }

theorem MeasureTheory.VectorMeasure.apply_eq_zero_of_isEmpty {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [IsEmpty α] (μ : VectorMeasure α M) (s : Set α) : μ s = 0

instance MeasureTheory.VectorMeasure.instSubsingletonOfIsEmpty {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [IsEmpty α] : Subsingleton (VectorMeasure α M)

theorem MeasureTheory.VectorMeasure.eq_zero_of_isEmpty {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [IsEmpty α] (μ : VectorMeasure α M) : μ = 0

@[deprecated FunLike.coe_zero (since := "2026-06-10")]

theorem MeasureTheory.VectorMeasure.coe_zero {F : Type u_3} {α : Type u_5} {β : Type u_6} [FunLike F α β] [Zero F] [Zero β] [IsZeroApply F α β] : ⇑0 = 0

Alias of FunLike.coe_zero.

@[deprecated zero_apply (since := "2026-06-10")]

theorem MeasureTheory.VectorMeasure.zero_apply {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst✝ : FunLike F α β} {inst✝¹ : Zero β} {inst✝² : Zero F} [self : IsZeroApply F α β] (x : α) : 0 x = 0

Alias of zero_apply.

def MeasureTheory.VectorMeasure.add {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] (v w : VectorMeasure α M) : VectorMeasure α M

The sum of two vector measure is a vector measure.

Equations

• v.add w = { measureOf' := ⇑v + ⇑w, empty' := ⋯, not_measurable' := ⋯, m_iUnion' := ⋯ }

@[implicit_reducible]

instance MeasureTheory.VectorMeasure.instAdd {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] : Add (VectorMeasure α M)

Equations

• MeasureTheory.VectorMeasure.instAdd = { add := MeasureTheory.VectorMeasure.add }

instance MeasureTheory.VectorMeasure.instIsAddApplySet {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] : IsAddApply (VectorMeasure α M) (Set α) M

@[deprecated FunLike.coe_add (since := "2026-06-10")]

theorem MeasureTheory.VectorMeasure.coe_add {F : Type u_3} {α : Type u_5} {β : Type u_6} [FunLike F α β] [Add F] [Add β] [IsAddApply F α β] (f g : F) : ⇑(f + g) = ⇑f + ⇑g

Alias of FunLike.coe_add.

@[deprecated add_apply (since := "2026-06-10")]

theorem MeasureTheory.VectorMeasure.add_apply {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst✝ : FunLike F α β} {inst✝¹ : Add β} {inst✝² : Add F} [self : IsAddApply F α β] (f g : F) (x : α) : (f + g) x = f x + g x

Alias of add_apply.

@[implicit_reducible]

instance MeasureTheory.VectorMeasure.instAddCommMonoid {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] : AddCommMonoid (VectorMeasure α M)

Equations

• One or more equations did not get rendered due to their size.

@[deprecated FunLike.coeAddMonoidHom (since := "2026-06-10")]

def MeasureTheory.VectorMeasure.coeFnAddMonoidHom (F : Type u_1) (α : Type u_2) (β : Type u_3) [FunLike F α β] [AddZero F] [AddZeroClass β] [IsZeroApply F α β] [IsAddApply F α β] : F →+ α → β

Alias of FunLike.coeAddMonoidHom.

Equations

• MeasureTheory.VectorMeasure.coeFnAddMonoidHom = FunLike.coeAddMonoidHom

@[deprecated FunLike.coeAddMonoidHom_apply (since := "2026-06-10")]

theorem MeasureTheory.VectorMeasure.coeFnAddMonoidHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [AddZero F] [AddZeroClass β] [IsZeroApply F α β] [IsAddApply F α β] (f : F) : (FunLike.coeAddMonoidHom F α β) f = ⇑f

Alias of FunLike.coeAddMonoidHom_apply.

@[deprecated FunLike.coe_sum (since := "2026-06-10")]

theorem MeasureTheory.VectorMeasure.coe_finsetSum {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [FunLike F α β] [AddCommMonoid β] [AddCommMonoid F] [IsZeroApply F α β] [IsAddApply F α β] (s : Finset ι) (f : ι → F) : ⇑(∑ i ∈ s, f i) = ∑ i ∈ s, ⇑(f i)

Alias of FunLike.coe_sum.

def MeasureTheory.VectorMeasure.neg {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] (v : VectorMeasure α M) : VectorMeasure α M

The negative of a vector measure is a vector measure.

Equations

• v.neg = { measureOf' := -⇑v, empty' := ⋯, not_measurable' := ⋯, m_iUnion' := ⋯ }

@[implicit_reducible]

instance MeasureTheory.VectorMeasure.instNeg {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] : Neg (VectorMeasure α M)

Equations

• MeasureTheory.VectorMeasure.instNeg = { neg := MeasureTheory.VectorMeasure.neg }

instance MeasureTheory.VectorMeasure.instIsNegApplySet {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] : IsNegApply (VectorMeasure α M) (Set α) M

@[deprecated FunLike.coe_neg (since := "2026-06-10")]

theorem MeasureTheory.VectorMeasure.coe_neg {F : Type u_3} {α : Type u_5} {β : Type u_6} [FunLike F α β] [Neg F] [Neg β] [IsNegApply F α β] (f : F) : ⇑(-f) = -⇑f

Alias of FunLike.coe_neg.

@[deprecated neg_apply (since := "2026-06-10")]

theorem MeasureTheory.VectorMeasure.neg_apply {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst✝ : FunLike F α β} {inst✝¹ : Neg β} {inst✝² : Neg F} [self : IsNegApply F α β] (f : F) (x : α) : (-f) x = -f x

Alias of neg_apply.

def MeasureTheory.VectorMeasure.sub {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] (v w : VectorMeasure α M) : VectorMeasure α M

The difference of two vector measure is a vector measure.

Equations

• v.sub w = { measureOf' := ⇑v - ⇑w, empty' := ⋯, not_measurable' := ⋯, m_iUnion' := ⋯ }

@[implicit_reducible]

instance MeasureTheory.VectorMeasure.instSub {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] : Sub (VectorMeasure α M)

Equations

• MeasureTheory.VectorMeasure.instSub = { sub := MeasureTheory.VectorMeasure.sub }

instance MeasureTheory.VectorMeasure.instIsSubApplySet {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] : IsSubApply (VectorMeasure α M) (Set α) M

@[deprecated FunLike.coe_sub (since := "2026-06-10")]

theorem MeasureTheory.VectorMeasure.coe_sub {F : Type u_3} {α : Type u_5} {β : Type u_6} [FunLike F α β] [Sub F] [Sub β] [IsSubApply F α β] (f g : F) : ⇑(f - g) = ⇑f - ⇑g

Alias of FunLike.coe_sub.

@[deprecated sub_apply (since := "2026-06-10")]

theorem MeasureTheory.VectorMeasure.sub_apply {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst✝ : FunLike F α β} {inst✝¹ : Sub β} {inst✝² : Sub F} [self : IsSubApply F α β] (f g : F) (x : α) : (f - g) x = f x - g x

Alias of sub_apply.

@[implicit_reducible]

instance MeasureTheory.VectorMeasure.instAddCommGroup {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] : AddCommGroup (VectorMeasure α M)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance MeasureTheory.VectorMeasure.instDistribMulAction {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {R : Type u_4} [Semiring R] [DistribMulAction R M] [ContinuousConstSMul R M] [ContinuousAdd M] : DistribMulAction R (VectorMeasure α M)

Equations

• MeasureTheory.VectorMeasure.instDistribMulAction = { toSMul := MeasureTheory.VectorMeasure.instSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

@[implicit_reducible]

instance MeasureTheory.VectorMeasure.instModule {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {R : Type u_4} [Semiring R] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] : Module R (VectorMeasure α M)

Equations

• MeasureTheory.VectorMeasure.instModule = { toDistribMulAction := MeasureTheory.VectorMeasure.instDistribMulAction, add_smul := ⋯, zero_smul := ⋯ }

noncomputable def MeasureTheory.VectorMeasure.dirac {β : Type u_2} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [MeasurableSpace β] (x : β) (v : M) : VectorMeasure β M

The Dirac vector measure with mass v at a point x. It gives mass v to measurable sets containing x, and 0 otherwise.

Equations

• MeasureTheory.VectorMeasure.dirac x v = { measureOf' := fun (s : Set β) => if MeasurableSet s ∧ x ∈ s then v else 0, empty' := ⋯, not_measurable' := ⋯, m_iUnion' := ⋯ }

@[simp]

theorem MeasureTheory.VectorMeasure.dirac_apply_of_mem {β : Type u_2} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [MeasurableSpace β] {x : β} {v : M} {s : Set β} (hs : MeasurableSet s) (hx : x ∈ s) : (dirac x v) s = v

@[simp]

theorem MeasureTheory.VectorMeasure.dirac_apply_of_notMem {β : Type u_2} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [MeasurableSpace β] {x : β} {v : M} {s : Set β} (hx : x ∉ s) : (dirac x v) s = 0

@[simp]

theorem MeasureTheory.VectorMeasure.dirac_zero {β : Type u_2} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [MeasurableSpace β] {x : β} : dirac x 0 = 0

noncomputable def MeasureTheory.Measure.toSignedMeasure {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) [hμ : IsFiniteMeasure μ] : SignedMeasure α

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

Equations

• μ.toSignedMeasure = { measureOf' := fun (s : Set α) => if MeasurableSet s then μ.real s else 0, empty' := ⋯, not_measurable' := ⋯, m_iUnion' := ⋯ }

@[simp]

theorem MeasureTheory.Measure.toSignedMeasure_apply {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) [hμ : IsFiniteMeasure μ] (i : Set α) : μ.toSignedMeasure i = if MeasurableSet i then μ.real i else 0

theorem MeasureTheory.Measure.toSignedMeasure_apply_measurable {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] {i : Set α} (hi : MeasurableSet i) : μ.toSignedMeasure i = μ.real i

theorem MeasureTheory.Measure.toSignedMeasure_congr {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h : μ = ν) : μ.toSignedMeasure = ν.toSignedMeasure

theorem MeasureTheory.Measure.toSignedMeasure_eq_toSignedMeasure_iff {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} [IsFiniteMeasure μ] [IsFiniteMeasure ν] : μ.toSignedMeasure = ν.toSignedMeasure ↔ μ = ν

@[simp]

theorem MeasureTheory.Measure.toSignedMeasure_zero {α : Type u_1} {m : MeasurableSpace α} : toSignedMeasure 0 = 0

@[simp]

theorem MeasureTheory.Measure.toSignedMeasure_add {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] : (μ + ν).toSignedMeasure = μ.toSignedMeasure + ν.toSignedMeasure

@[simp]

theorem MeasureTheory.Measure.toSignedMeasure_smul {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] (r : NNReal) : (r • μ).toSignedMeasure = r • μ.toSignedMeasure

noncomputable def MeasureTheory.Measure.toENNRealVectorMeasure {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) : VectorMeasure α ENNReal

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

Equations

• μ.toENNRealVectorMeasure = { measureOf' := fun (i : Set α) => if MeasurableSet i then μ i else 0, empty' := ⋯, not_measurable' := ⋯, m_iUnion' := ⋯ }

@[simp]

theorem MeasureTheory.Measure.toENNRealVectorMeasure_apply {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) (i : Set α) : μ.toENNRealVectorMeasure i = if MeasurableSet i then μ i else 0

theorem MeasureTheory.Measure.toENNRealVectorMeasure_apply_measurable {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {i : Set α} (hi : MeasurableSet i) : μ.toENNRealVectorMeasure i = μ i

@[simp]

theorem MeasureTheory.Measure.toENNRealVectorMeasure_zero {α : Type u_1} {m : MeasurableSpace α} : toENNRealVectorMeasure 0 = 0

@[simp]

theorem MeasureTheory.Measure.toENNRealVectorMeasure_add {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) : (μ + ν).toENNRealVectorMeasure = μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure

theorem MeasureTheory.Measure.toSignedMeasure_sub_apply {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} [IsFiniteMeasure μ] [IsFiniteMeasure ν] {i : Set α} (hi : MeasurableSet i) : (μ.toSignedMeasure - ν.toSignedMeasure) i = μ.real i - ν.real i

noncomputable def MeasureTheory.VectorMeasure.ennrealToMeasure {α : Type u_1} {x✝ : MeasurableSpace α} (v : VectorMeasure α ENNReal) : Measure α

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

Equations

• v.ennrealToMeasure = MeasureTheory.Measure.ofMeasurable (fun (s : Set α) (x : MeasurableSet s) => v s) ⋯ ⋯

theorem MeasureTheory.VectorMeasure.ennrealToMeasure_apply {α : Type u_1} {m : MeasurableSpace α} {v : VectorMeasure α ENNReal} {s : Set α} (hs : MeasurableSet s) : v.ennrealToMeasure s = v s

@[simp]

theorem MeasureTheory.VectorMeasure.ennrealToMeasure_zero {α : Type u_1} {m : MeasurableSpace α} : ennrealToMeasure 0 = 0

@[simp]

theorem MeasureTheory.Measure.toENNRealVectorMeasure_ennrealToMeasure {α : Type u_1} {m : MeasurableSpace α} (μ : VectorMeasure α ENNReal) : μ.ennrealToMeasure.toENNRealVectorMeasure = μ

@[simp]

theorem MeasureTheory.VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) : μ.toENNRealVectorMeasure.ennrealToMeasure = μ

noncomputable def MeasureTheory.VectorMeasure.equivMeasure {α : Type u_1} [MeasurableSpace α] : VectorMeasure α ENNReal ≃ Measure α

The equiv between VectorMeasure α ℝ≥0∞ and Measure α formed by MeasureTheory.VectorMeasure.ennrealToMeasure and MeasureTheory.Measure.toENNRealVectorMeasure.

Equations

• MeasureTheory.VectorMeasure.equivMeasure = { toFun := MeasureTheory.VectorMeasure.ennrealToMeasure, invFun := MeasureTheory.Measure.toENNRealVectorMeasure, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem MeasureTheory.VectorMeasure.equivMeasure_symm_apply {α : Type u_1} [MeasurableSpace α] (μ : Measure α) : equivMeasure.symm μ = μ.toENNRealVectorMeasure

@[simp]

theorem MeasureTheory.VectorMeasure.equivMeasure_apply {α : Type u_1} [MeasurableSpace α] (v : VectorMeasure α ENNReal) : equivMeasure v = v.ennrealToMeasure

noncomputable def MeasureTheory.VectorMeasure.map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [MeasurableSpace β] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : VectorMeasure α M) (f : α → β) : VectorMeasure β M

The pushforward of a vector measure along a function.

Equations

• v.map f = if hf : Measurable f then { measureOf' := fun (s : Set β) => if MeasurableSet s then v (f ⁻¹' s) else 0, empty' := ⋯, not_measurable' := ⋯, m_iUnion' := ⋯ } else 0

theorem MeasureTheory.VectorMeasure.map_not_measurable {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [MeasurableSpace β] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : VectorMeasure α M) {f : α → β} (hf : ¬Measurable f) : v.map f = 0

theorem MeasureTheory.VectorMeasure.map_apply {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [MeasurableSpace β] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : VectorMeasure α M) {f : α → β} (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) : (v.map f) s = v (f ⁻¹' s)

@[simp]

theorem MeasureTheory.VectorMeasure.map_id {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : VectorMeasure α M) : v.map id = v

@[simp]

theorem MeasureTheory.VectorMeasure.map_zero {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [MeasurableSpace β] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (f : α → β) : map 0 f = 0

def MeasureTheory.VectorMeasure.mapRange {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {N : Type u_4} [AddCommMonoid N] [TopologicalSpace N] (v : VectorMeasure α M) (f : M →+ N) (hf : Continuous ⇑f) : VectorMeasure α N

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

Equations

• v.mapRange f hf = { measureOf' := fun (s : Set α) => f (v s), empty' := ⋯, not_measurable' := ⋯, m_iUnion' := ⋯ }

@[simp]

theorem MeasureTheory.VectorMeasure.mapRange_apply {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : VectorMeasure α M) {N : Type u_4} [AddCommMonoid N] [TopologicalSpace N] {f : M →+ N} (hf : Continuous ⇑f) {s : Set α} : (v.mapRange f hf) s = f (v s)

@[simp]

theorem MeasureTheory.VectorMeasure.mapRange_id {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : VectorMeasure α M) : v.mapRange (AddMonoidHom.id M) ⋯ = v

@[simp]

theorem MeasureTheory.VectorMeasure.mapRange_zero {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {N : Type u_4} [AddCommMonoid N] [TopologicalSpace N] {f : M →+ N} (hf : Continuous ⇑f) : mapRange 0 f hf = 0

@[simp]

theorem MeasureTheory.VectorMeasure.mapRange_add {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {N : Type u_4} [AddCommMonoid N] [TopologicalSpace N] [ContinuousAdd M] [ContinuousAdd N] {v w : VectorMeasure α M} {f : M →+ N} (hf : Continuous ⇑f) : (v + w).mapRange f hf = v.mapRange f hf + w.mapRange f hf

def MeasureTheory.VectorMeasure.mapRangeHom {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {N : Type u_4} [AddCommMonoid N] [TopologicalSpace N] [ContinuousAdd M] [ContinuousAdd N] {α : Type u_5} [MeasurableSpace α] (f : M →+ N) (hf : Continuous ⇑f) : VectorMeasure α M →+ VectorMeasure α N

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

Equations

• MeasureTheory.VectorMeasure.mapRangeHom f hf = { toFun := fun (v : MeasureTheory.VectorMeasure α M) => v.mapRange f hf, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem MeasureTheory.VectorMeasure.mapRange_smul {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {N : Type u_4} [AddCommMonoid N] [TopologicalSpace N] {R : Type u_5} [Semiring R] [Module R M] [Module R N] [ContinuousConstSMul R M] [ContinuousConstSMul R N] {v : VectorMeasure α M} {f : M →ₗ[R] N} (hf : Continuous ⇑f) {c : R} : (c • v).mapRange f.toAddMonoidHom hf = c • v.mapRange f.toAddMonoidHom hf

def MeasureTheory.VectorMeasure.mapRangeₗ {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {N : Type u_4} [AddCommMonoid N] [TopologicalSpace N] {R : Type u_5} [Semiring R] [Module R M] [Module R N] [ContinuousConstSMul R M] [ContinuousConstSMul R N] [ContinuousAdd M] [ContinuousAdd N] {α : Type u_6} [MeasurableSpace α] (f : M →ₗ[R] N) (hf : Continuous ⇑f) : VectorMeasure α M →ₗ[R] VectorMeasure α N

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

Equations

• MeasureTheory.VectorMeasure.mapRangeₗ f hf = { toFun := fun (v : MeasureTheory.VectorMeasure α M) => v.mapRange f.toAddMonoidHom hf, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def MeasureTheory.VectorMeasure.restrict {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : VectorMeasure α M) (i : Set α) : VectorMeasure α M

The restriction of a vector measure on some set.

Equations

• v.restrict i = if hi : MeasurableSet i then { measureOf' := fun (s : Set α) => if MeasurableSet s then v (s ∩ i) else 0, empty' := ⋯, not_measurable' := ⋯, m_iUnion' := ⋯ } else 0

theorem MeasureTheory.VectorMeasure.restrict_not_measurable {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : VectorMeasure α M) {i : Set α} (hi : ¬MeasurableSet i) : v.restrict i = 0

theorem MeasureTheory.VectorMeasure.restrict_apply {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : VectorMeasure α M) {i : Set α} (hi : MeasurableSet i) {j : Set α} (hj : MeasurableSet j) : (v.restrict i) j = v (j ∩ i)

theorem MeasureTheory.VectorMeasure.restrict_eq_self {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : VectorMeasure α M) {i : Set α} (hi : MeasurableSet i) {j : Set α} (hj : MeasurableSet j) (hij : j ⊆ i) : (v.restrict i) j = v j

@[simp]

theorem MeasureTheory.VectorMeasure.restrict_empty {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : VectorMeasure α M) : v.restrict ∅ = 0

@[simp]

theorem MeasureTheory.VectorMeasure.restrict_univ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : VectorMeasure α M) : v.restrict Set.univ = v

@[simp]

theorem MeasureTheory.VectorMeasure.restrict_zero {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {i : Set α} : restrict 0 i = 0

theorem MeasureTheory.VectorMeasure.restrict_dirac {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {s : Set α} {x : α} {m : M} (hs : MeasurableSet s) [Decidable (x ∈ s)] : (dirac x m).restrict s = if x ∈ s then dirac x m else 0

@[simp]

theorem MeasureTheory.VectorMeasure.restrict_dirac_of_mem {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {s : Set α} {x : α} {m : M} (hs : MeasurableSet s) (hx : x ∈ s) : (dirac x m).restrict s = dirac x m

@[simp]

theorem MeasureTheory.VectorMeasure.restrict_dirac_of_notMem {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {s : Set α} {x : α} {m : M} (hx : x ∉ s) : (dirac x m).restrict s = 0

@[simp]

theorem MeasureTheory.VectorMeasure.restrict_singleton {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : VectorMeasure α M) {a : α} : v.restrict {a} = dirac a (v {a})

theorem MeasureTheory.VectorMeasure.restrict_restrict {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : VectorMeasure α M) {s t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) : (v.restrict t).restrict s = v.restrict (s ∩ t)

theorem MeasureTheory.VectorMeasure.restrict_map {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [MeasurableSpace β] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : VectorMeasure α M) {f : α → β} (hf : Measurable f) {s : Set β} (hs : MeasurableSet s) : (v.map f).restrict s = (v.restrict (f ⁻¹' s)).map f

theorem MeasureTheory.VectorMeasure.restrict_toSignedMeasure {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] {s : Set α} (hs : MeasurableSet s) : restrict μ.toSignedMeasure s = (μ.restrict s).toSignedMeasure

theorem MeasureTheory.VectorMeasure.map_add {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} [MeasurableSpace β] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] (v w : VectorMeasure α M) (f : α → β) : (v + w).map f = v.map f + w.map f

noncomputable def MeasureTheory.VectorMeasure.mapGm {β : Type u_2} [MeasurableSpace β] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] {α : Type u_4} [MeasurableSpace α] (f : α → β) : VectorMeasure α M →+ VectorMeasure β M

VectorMeasure.map as an additive monoid homomorphism.

Equations

• MeasureTheory.VectorMeasure.mapGm f = { toFun := fun (v : MeasureTheory.VectorMeasure α M) => v.map f, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem MeasureTheory.VectorMeasure.mapGm_apply {β : Type u_2} [MeasurableSpace β] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] {α : Type u_4} [MeasurableSpace α] (f : α → β) (v : VectorMeasure α M) : (mapGm f) v = v.map f

@[simp]

theorem MeasureTheory.VectorMeasure.restrict_add {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] (v w : VectorMeasure α M) (i : Set α) : (v + w).restrict i = v.restrict i + w.restrict i

noncomputable def MeasureTheory.VectorMeasure.restrictGm {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] {α : Type u_4} [MeasurableSpace α] (i : Set α) : VectorMeasure α M →+ VectorMeasure α M

VectorMeasure.restrict as an additive monoid homomorphism.

Equations

• MeasureTheory.VectorMeasure.restrictGm i = { toFun := fun (v : MeasureTheory.VectorMeasure α M) => v.restrict i, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem MeasureTheory.VectorMeasure.restrictGm_apply {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] {α : Type u_4} [MeasurableSpace α] (i : Set α) (v : VectorMeasure α M) : (restrictGm i) v = v.restrict i

@[simp]

theorem MeasureTheory.VectorMeasure.restrict_add_restrict_compl {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_4} [TopologicalSpace M] [AddCommMonoid M] [T2Space M] [ContinuousAdd M] {v : VectorMeasure α M} {i : Set α} (hi : MeasurableSet i) : v.restrict i + v.restrict iᶜ = v

theorem MeasureTheory.VectorMeasure.restrict_inter_add_sdiff {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_4} [TopologicalSpace M] [AddCommMonoid M] [T2Space M] [ContinuousAdd M] {v : VectorMeasure α M} {s t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) : v.restrict (s ∩ t) + v.restrict (s \ t) = v.restrict s

@[deprecated MeasureTheory.VectorMeasure.restrict_inter_add_sdiff (since := "2026-06-03")]

theorem MeasureTheory.VectorMeasure.restrict_inter_add_diff {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_4} [TopologicalSpace M] [AddCommMonoid M] [T2Space M] [ContinuousAdd M] {v : VectorMeasure α M} {s t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) : v.restrict (s ∩ t) + v.restrict (s \ t) = v.restrict s

Alias of MeasureTheory.VectorMeasure.restrict_inter_add_sdiff.

theorem MeasureTheory.VectorMeasure.restrict_union_add_inter {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_4} [TopologicalSpace M] [AddCommMonoid M] [T2Space M] [ContinuousAdd M] {v : VectorMeasure α M} {s t : Set α} (hs : MeasurableSet s) (ht : MeasurableSet t) : v.restrict (s ∪ t) + v.restrict (s ∩ t) = v.restrict s + v.restrict t

theorem MeasureTheory.VectorMeasure.restrict_union {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_4} [TopologicalSpace M] [AddCommMonoid M] [T2Space M] [ContinuousAdd M] {v : VectorMeasure α M} {s t : Set α} (h : Disjoint s t) (hs : MeasurableSet s) (ht : MeasurableSet t) : v.restrict (s ∪ t) = v.restrict s + v.restrict t

@[simp]

theorem MeasureTheory.VectorMeasure.restrict_neg {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_4} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] (v : VectorMeasure α M) (i : Set α) : (-v).restrict i = -v.restrict i

@[simp]

theorem MeasureTheory.VectorMeasure.restrict_sub {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_4} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] (v w : VectorMeasure α M) (i : Set α) : (v - w).restrict i = v.restrict i - w.restrict i

@[simp]

theorem MeasureTheory.VectorMeasure.map_smul {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [MeasurableSpace β] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {R : Type u_4} [Semiring R] [DistribMulAction R M] [ContinuousConstSMul R M] {v : VectorMeasure α M} {f : α → β} (c : R) : (c • v).map f = c • v.map f

@[simp]

theorem MeasureTheory.VectorMeasure.restrict_smul {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {R : Type u_4} [Semiring R] [DistribMulAction R M] [ContinuousConstSMul R M] {v : VectorMeasure α M} {i : Set α} (c : R) : (c • v).restrict i = c • v.restrict i

noncomputable def MeasureTheory.VectorMeasure.mapₗ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [MeasurableSpace β] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {R : Type u_4} [Semiring R] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] (f : α → β) : VectorMeasure α M →ₗ[R] VectorMeasure β M

VectorMeasure.map as a linear map.

Equations

• MeasureTheory.VectorMeasure.mapₗ f = { toFun := fun (v : MeasureTheory.VectorMeasure α M) => v.map f, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem MeasureTheory.VectorMeasure.mapₗ_apply {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [MeasurableSpace β] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {R : Type u_4} [Semiring R] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] (f : α → β) (v : VectorMeasure α M) : (mapₗ f) v = v.map f

noncomputable def MeasureTheory.VectorMeasure.restrictₗ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {R : Type u_4} [Semiring R] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] (i : Set α) : VectorMeasure α M →ₗ[R] VectorMeasure α M

VectorMeasure.restrict as an additive monoid homomorphism.

Equations

• MeasureTheory.VectorMeasure.restrictₗ i = { toFun := fun (v : MeasureTheory.VectorMeasure α M) => v.restrict i, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem MeasureTheory.VectorMeasure.restrictₗ_apply {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {R : Type u_4} [Semiring R] [Module R M] [ContinuousConstSMul R M] [ContinuousAdd M] (i : Set α) (v : VectorMeasure α M) : (restrictₗ i) v = v.restrict i

@[implicit_reducible]

instance MeasureTheory.VectorMeasure.instPartialOrder {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] : PartialOrder (VectorMeasure α M)

Vector measures over a partially ordered monoid is partially ordered.

This definition is consistent with Measure.instPartialOrder.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.VectorMeasure.le_iff {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] {v w : VectorMeasure α M} : v ≤ w ↔ ∀ (i : Set α), MeasurableSet i → v i ≤ w i

theorem MeasureTheory.VectorMeasure.le_iff' {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] {v w : VectorMeasure α M} : v ≤ w ↔ ∀ (i : Set α), v i ≤ w i

def MeasureTheory.«term_≤[_]_» : Lean.TrailingParserDescr

v ≤[i] w is notation for v.restrict i ≤ w.restrict i.

Equations

• One or more equations did not get rendered due to their size.

theorem MeasureTheory.VectorMeasure.restrict_le_restrict_iff {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v w : VectorMeasure α M) {i : Set α} (hi : MeasurableSet i) : v.restrict i ≤ w.restrict i ↔ ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → v j ≤ w j

theorem MeasureTheory.VectorMeasure.subset_le_of_restrict_le_restrict {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v w : VectorMeasure α M) {i : Set α} (hi : MeasurableSet i) (hi₂ : v.restrict i ≤ w.restrict i) {j : Set α} (hj : j ⊆ i) : v j ≤ w j

theorem MeasureTheory.VectorMeasure.restrict_le_restrict_of_subset_le {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v w : VectorMeasure α M) {i : Set α} (h : ∀ ⦃j : Set α⦄, MeasurableSet j → j ⊆ i → v j ≤ w j) : v.restrict i ≤ w.restrict i

theorem MeasureTheory.VectorMeasure.restrict_le_restrict_subset {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v w : VectorMeasure α M) {i j : Set α} (hi₁ : MeasurableSet i) (hi₂ : v.restrict i ≤ w.restrict i) (hij : j ⊆ i) : v.restrict j ≤ w.restrict j

theorem MeasureTheory.VectorMeasure.le_restrict_empty {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v w : VectorMeasure α M) : v.restrict ∅ ≤ w.restrict ∅

theorem MeasureTheory.VectorMeasure.le_restrict_univ_iff_le {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v w : VectorMeasure α M) : v.restrict Set.univ ≤ w.restrict Set.univ ↔ v ≤ w

theorem MeasureTheory.VectorMeasure.neg_le_neg {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommGroup M] [PartialOrder M] [IsOrderedAddMonoid M] [IsTopologicalAddGroup M] (v w : VectorMeasure α M) {i : Set α} (hi : MeasurableSet i) (h : v.restrict i ≤ w.restrict i) : (-w).restrict i ≤ (-v).restrict i

theorem MeasureTheory.VectorMeasure.neg_le_neg_iff {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommGroup M] [PartialOrder M] [IsOrderedAddMonoid M] [IsTopologicalAddGroup M] (v w : VectorMeasure α M) {i : Set α} (hi : MeasurableSet i) : (-w).restrict i ≤ (-v).restrict i ↔ v.restrict i ≤ w.restrict i

theorem MeasureTheory.VectorMeasure.restrict_le_restrict_iUnion {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] [OrderClosedTopology M] (v w : VectorMeasure α M) {f : ℕ → Set α} (hf₁ : ∀ (n : ℕ), MeasurableSet (f n)) (hf₂ : ∀ (n : ℕ), v.restrict (f n) ≤ w.restrict (f n)) : v.restrict (⋃ (n : ℕ), f n) ≤ w.restrict (⋃ (n : ℕ), f n)

theorem MeasureTheory.VectorMeasure.restrict_le_restrict_countable_iUnion {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] [OrderClosedTopology M] (v w : VectorMeasure α M) [Countable β] {f : β → Set α} (hf₁ : ∀ (b : β), MeasurableSet (f b)) (hf₂ : ∀ (b : β), v.restrict (f b) ≤ w.restrict (f b)) : v.restrict (⋃ (b : β), f b) ≤ w.restrict (⋃ (b : β), f b)

theorem MeasureTheory.VectorMeasure.restrict_le_restrict_union {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] [OrderClosedTopology M] (v w : VectorMeasure α M) {i j : Set α} (hi₁ : MeasurableSet i) (hi₂ : v.restrict i ≤ w.restrict i) (hj₁ : MeasurableSet j) (hj₂ : v.restrict j ≤ w.restrict j) : v.restrict (i ∪ j) ≤ w.restrict (i ∪ j)

theorem MeasureTheory.VectorMeasure.nonneg_of_zero_le_restrict {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v : VectorMeasure α M) {i : Set α} (hi₂ : restrict 0 i ≤ v.restrict i) : 0 ≤ v i

theorem MeasureTheory.VectorMeasure.nonpos_of_restrict_le_zero {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v : VectorMeasure α M) {i : Set α} (hi₂ : v.restrict i ≤ restrict 0 i) : v i ≤ 0

theorem MeasureTheory.VectorMeasure.zero_le_restrict_not_measurable {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v : VectorMeasure α M) {i : Set α} (hi : ¬MeasurableSet i) : restrict 0 i ≤ v.restrict i

theorem MeasureTheory.VectorMeasure.restrict_le_zero_of_not_measurable {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v : VectorMeasure α M) {i : Set α} (hi : ¬MeasurableSet i) : v.restrict i ≤ restrict 0 i

theorem MeasureTheory.VectorMeasure.measurable_of_not_zero_le_restrict {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v : VectorMeasure α M) {i : Set α} (hi : ¬restrict 0 i ≤ v.restrict i) : MeasurableSet i

theorem MeasureTheory.VectorMeasure.measurable_of_not_restrict_le_zero {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v : VectorMeasure α M) {i : Set α} (hi : ¬v.restrict i ≤ restrict 0 i) : MeasurableSet i

theorem MeasureTheory.VectorMeasure.zero_le_restrict_subset {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v : VectorMeasure α M) {i j : Set α} (hi₁ : MeasurableSet i) (hij : j ⊆ i) (hi₂ : restrict 0 i ≤ v.restrict i) : restrict 0 j ≤ v.restrict j

theorem MeasureTheory.VectorMeasure.restrict_le_zero_subset {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v : VectorMeasure α M) {i j : Set α} (hi₁ : MeasurableSet i) (hij : j ⊆ i) (hi₂ : v.restrict i ≤ restrict 0 i) : v.restrict j ≤ restrict 0 j

theorem MeasureTheory.VectorMeasure.exists_pos_measure_of_not_restrict_le_zero {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [LinearOrder M] (v : VectorMeasure α M) {i : Set α} (hi : ¬v.restrict i ≤ restrict 0 i) : ∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ 0 < v j

instance MeasureTheory.VectorMeasure.instAddLeftMono {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] [AddLeftMono M] [ContinuousAdd M] : AddLeftMono (VectorMeasure α M)

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.

Equations

• v.AbsolutelyContinuous w = ∀ ⦃s : Set α⦄, w s = 0 → 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.

Equations

• MeasureTheory.«term_≪ᵥ_» = Lean.ParserDescr.trailingNode `MeasureTheory.«term_≪ᵥ_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≪ᵥ ") (Lean.ParserDescr.cat `term 51))

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.

Equations

• v.MutuallySingular w = ∃ (s : Set α), MeasurableSet s ∧ (∀ t ⊆ s, v t = 0) ∧ ∀ t ⊆ sᶜ, w t = 0

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.

Equations

• MeasureTheory.«term_⟂ᵥ_» = Lean.ParserDescr.trailingNode `MeasureTheory.«term_⟂ᵥ_» 60 60 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟂ᵥ ") (Lean.ParserDescr.cat `term 61))

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

noncomputable def MeasureTheory.VectorMeasure.trim {α : Type u_1} {M : Type u_4} [AddCommMonoid M] [TopologicalSpace M] {m n : MeasurableSpace α} (v : VectorMeasure α M) (hle : m ≤ n) : VectorMeasure α M

Restriction of a vector measure onto a sub-σ-algebra.

Equations

• v.trim hle = { measureOf' := fun (i : Set α) => if MeasurableSet i then v i else 0, empty' := ⋯, not_measurable' := ⋯, m_iUnion' := ⋯ }

@[simp]

theorem MeasureTheory.VectorMeasure.trim_apply {α : Type u_1} {M : Type u_4} [AddCommMonoid M] [TopologicalSpace M] {m n : MeasurableSpace α} (v : VectorMeasure α M) (hle : m ≤ n) (i : Set α) : (v.trim hle).measureOf' i = if MeasurableSet i then v i else 0

theorem MeasureTheory.VectorMeasure.trim_eq_self {α : Type u_1} {M : Type u_4} [AddCommMonoid M] [TopologicalSpace M] {n : MeasurableSpace α} {v : VectorMeasure α M} : v.trim ⋯ = v

@[simp]

theorem MeasureTheory.VectorMeasure.zero_trim {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [AddCommMonoid M] [TopologicalSpace M] {n : MeasurableSpace α} (hle : m ≤ n) : trim 0 hle = 0

theorem MeasureTheory.VectorMeasure.trim_measurableSet_eq {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [AddCommMonoid M] [TopologicalSpace M] {n : MeasurableSpace α} {v : VectorMeasure α M} (hle : m ≤ n) {i : Set α} (hi : MeasurableSet i) : (v.trim hle) i = v i

theorem MeasureTheory.VectorMeasure.restrict_trim {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [AddCommMonoid M] [TopologicalSpace M] {n : MeasurableSpace α} {v : VectorMeasure α M} (hle : m ≤ n) {i : Set α} (hi : MeasurableSet i) : (v.trim hle).restrict i = (v.restrict i).trim hle

noncomputable def MeasureTheory.SignedMeasure.toMeasureOfZeroLE' {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (i : Set α) (hi : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i) (j : Set α) (hj : MeasurableSet j) : ENNReal

The underlying function for SignedMeasure.toMeasureOfZeroLE.

Equations

• s.toMeasureOfZeroLE' i hi j hj = ↑(NNReal.mk ((MeasureTheory.VectorMeasure.restrict s i) j) ⋯)

noncomputable def MeasureTheory.SignedMeasure.toMeasureOfZeroLE {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (i : Set α) (hi₁ : MeasurableSet i) (hi₂ : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i) : Measure α

Given a signed measure s and a positive measurable set i, toMeasureOfZeroLE provides the measure, mapping measurable sets j to s (i ∩ j).

Equations

• s.toMeasureOfZeroLE i hi₁ hi₂ = MeasureTheory.Measure.ofMeasurable (s.toMeasureOfZeroLE' i hi₂) ⋯ ⋯

theorem MeasureTheory.SignedMeasure.toMeasureOfZeroLE_apply {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) {i j : Set α} (hi : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i) (hi₁ : MeasurableSet i) (hj₁ : MeasurableSet j) : (s.toMeasureOfZeroLE i hi₁ hi) j = ↑(NNReal.mk (s (i ∩ j)) ⋯)

theorem MeasureTheory.SignedMeasure.toMeasureOfZeroLE_real_apply {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) {i j : Set α} (hi : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i) (hi₁ : MeasurableSet i) (hj₁ : MeasurableSet j) : (s.toMeasureOfZeroLE i hi₁ hi).real j = s (i ∩ j)

noncomputable def MeasureTheory.SignedMeasure.toMeasureOfLEZero {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (i : Set α) (hi₁ : MeasurableSet i) (hi₂ : VectorMeasure.restrict s i ≤ VectorMeasure.restrict 0 i) : Measure α

Given a signed measure s and a negative measurable set i, toMeasureOfLEZero provides the measure, mapping measurable sets j to -s (i ∩ j).

Equations

• s.toMeasureOfLEZero i hi₁ hi₂ = (-s).toMeasureOfZeroLE i hi₁ ⋯

theorem MeasureTheory.SignedMeasure.toMeasureOfLEZero_apply {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) {i j : Set α} (hi : VectorMeasure.restrict s i ≤ VectorMeasure.restrict 0 i) (hi₁ : MeasurableSet i) (hj₁ : MeasurableSet j) : (s.toMeasureOfLEZero i hi₁ hi) j = ↑(NNReal.mk (-s (i ∩ j)) ⋯)

theorem MeasureTheory.SignedMeasure.toMeasureOfLEZero_real_apply {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) {i j : Set α} (hi : VectorMeasure.restrict s i ≤ VectorMeasure.restrict 0 i) (hi₁ : MeasurableSet i) (hj₁ : MeasurableSet j) : (s.toMeasureOfLEZero i hi₁ hi).real j = -s (i ∩ j)

instance MeasureTheory.SignedMeasure.toMeasureOfZeroLE_finite {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) {i : Set α} (hi : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i) (hi₁ : MeasurableSet i) : IsFiniteMeasure (s.toMeasureOfZeroLE i hi₁ hi)

SignedMeasure.toMeasureOfZeroLE is a finite measure.

instance MeasureTheory.SignedMeasure.toMeasureOfLEZero_finite {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) {i : Set α} (hi : VectorMeasure.restrict s i ≤ VectorMeasure.restrict 0 i) (hi₁ : MeasurableSet i) : IsFiniteMeasure (s.toMeasureOfLEZero i hi₁ hi)

SignedMeasure.toMeasureOfLEZero is a finite measure.

theorem MeasureTheory.SignedMeasure.toMeasureOfZeroLE_toSignedMeasure {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (hs : VectorMeasure.restrict 0 Set.univ ≤ VectorMeasure.restrict s Set.univ) : (s.toMeasureOfZeroLE Set.univ ⋯ hs).toSignedMeasure = s

theorem MeasureTheory.SignedMeasure.toMeasureOfLEZero_toSignedMeasure {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (hs : VectorMeasure.restrict s Set.univ ≤ VectorMeasure.restrict 0 Set.univ) : (s.toMeasureOfLEZero Set.univ ⋯ hs).toSignedMeasure = -s

theorem MeasureTheory.Measure.zero_le_toSignedMeasure {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] : 0 ≤ μ.toSignedMeasure

theorem MeasureTheory.Measure.toSignedMeasure_toMeasureOfZeroLE {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] : μ.toSignedMeasure.toMeasureOfZeroLE Set.univ ⋯ ⋯ = μ

theorem MeasureTheory.Measure.toSignedMeasure_restrict_eq_restrict_toSignedMeasure {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] (s : Set α) (hs : MeasurableSet s) : VectorMeasure.restrict μ.toSignedMeasure s = (μ.restrict s).toSignedMeasure

theorem MeasureTheory.Measure.toSignedMeasure_le_toSignedMeasure_iff {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] : μ.toSignedMeasure ≤ ν.toSignedMeasure ↔ μ ≤ ν