Basic API for vector measures

This file develops the basic consequences of countable additivity for vector measures, equips vector measures with their natural algebraic structures, and defines Dirac vector measures.

Main definitions

• VectorMeasure.of_disjoint_iUnion evaluates a vector measure on a disjoint countable union.
• The additive, scalar, and module structures on vector measures are defined pointwise.
• VectorMeasure.dirac is a Dirac vector measure.

@[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_if {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {v : VectorMeasure α M} {ι : Type u_4} {x : ι} {B : Set ι} {A : Set α} [Decidable (x ∈ B)] : v (if x ∈ B then A else ∅) = B.indicator (fun (x : ι) => v A) x

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_biUnion {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {v : VectorMeasure α M} [T2Space M] {ι : Type u_4} {s : Set ι} {f : ι → Set α} (hs : s.Countable) (hd : s.Pairwise (Function.onFun Disjoint f)) (h : ∀ b ∈ s, MeasurableSet (f b)) : v (⋃ b ∈ s, f b) = ∑' (p : ↑s), v (f ↑p)

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.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.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)))

theorem MeasureTheory.VectorMeasure.ext_of_generateFrom {M : Type u_4} [AddCommGroup M] [TopologicalSpace M] [T2Space M] {X : Type u_5} {mX : MeasurableSpace X} {μ ν : VectorMeasure X M} (C : Set (Set X)) (hμν : ∀ s ∈ C, μ s = ν s) (hA : mX = MeasurableSpace.generateFrom C) (hC : IsPiSystem C) (h_univ : μ Set.univ = ν Set.univ) : μ = ν

If two vector measures give the same mass to the whole space and coincide on a generating π-system, then they coincide.

@[instance_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' := ⋯ }

@[instance_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_2} {α : Type u_4} {β : Type u_5} [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.

@[instance_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

@[instance_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_2} {α : Type u_4} {β : Type u_5} [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' := ⋯ }

@[instance_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_2} {α : Type u_4} {β : Type u_5} [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.

@[instance_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' := ⋯ }

@[instance_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_2} {α : Type u_4} {β : Type u_5} [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' := ⋯ }

@[instance_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_2} {α : Type u_4} {β : Type u_5} [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.

@[instance_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.

@[instance_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 := ⋯ }

@[instance_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