Operations on vector measures

This file defines conversions between ordinary measures and vector measures, together with pushforwards, maps on the range, restrictions, and restriction to a sub-σ-algebra.

Main definitions

• Measure.toSignedMeasure, Measure.toENNRealVectorMeasure, and VectorMeasure.ennrealToMeasure convert between measures and vector measures.
• MeasureTheory.VectorMeasure.map is the pushforward of a vector measure along a function.
• VectorMeasure.mapRange composes a vector measure with a continuous additive homomorphism.
• MeasureTheory.VectorMeasure.restrict is the restriction of a vector measure on some set.
• VectorMeasure.trim restricts a vector measure to a smaller measurable space.

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_apply {α : Type u_1} [MeasurableSpace α] (v : VectorMeasure α ENNReal) : equivMeasure v = v.ennrealToMeasure

@[simp]

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

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.mapRangeL {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 →L[R] N) : VectorMeasure α M →ₗ[R] VectorMeasure α N

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

Equations

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

@[deprecated MeasureTheory.VectorMeasure.mapRangeL (since := "2026-08-14")]

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 →L[R] N) : VectorMeasure α M →ₗ[R] VectorMeasure α N

Alias of MeasureTheory.VectorMeasure.mapRangeL.

---

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

Equations

• @MeasureTheory.VectorMeasure.mapRangeₗ = @MeasureTheory.VectorMeasure.mapRangeL

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)

@[simp]

theorem MeasureTheory.VectorMeasure.restrict_apply_univ {α : Type u_1} {mα : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : VectorMeasure α M) {i : Set α} : (v.restrict i) Set.univ = v 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

noncomputable def MeasureTheory.VectorMeasure.trim {α : Type u_1} {M : Type u_3} [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_3} [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_3} [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_3} [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_3} [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_3} [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