Documentation

Mathlib.MeasureTheory.VectorMeasure.Basic

Vector valued measures #

This file defines vector valued measures, which are σ-additive functions from a set to an add 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 set 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 add monoid) such that the empty set and non-measurable sets are mapped to zero.

measureOf' : Set α → M
empty' : ↑self ∅ = 0
not_measurable' ⦃i : Set α⦄ : ¬MeasurableSet i → ↑self i = 0
m_iUnion' ⦃f : ℕ → Set α⦄ : (∀ (i : ℕ), MeasurableSet (f i)) → Pairwise (Function.onFun Disjoint f) → HasSum (fun (i : ℕ) => ↑self (f i)) (↑self (⋃ (i : ℕ), f i))

Instances For

@[reducible, inline]

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

Type u_3

A SignedMeasure is an ℝ-vector measure.

Equations

MeasureTheory.SignedMeasure α = MeasureTheory.VectorMeasure α ℝ

instance MeasureTheory.VectorMeasure.instCoeFun {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] :

CoeFun (VectorMeasure α M) fun (x : VectorMeasure α M) => Set α → M

Equations

MeasureTheory.VectorMeasure.instCoeFun = { coe := MeasureTheory.VectorMeasure.measureOf' }

@[simp]

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

↑v ∅ = 0

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

theorem MeasureTheory.VectorMeasure.coe_injective {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] :

Function.Injective measureOf'

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 α), ↑v i = ↑w i

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)

@[deprecated MeasureTheory.VectorMeasure.of_disjoint_iUnion (since := "2024-09-15")]

theorem MeasureTheory.VectorMeasure.of_disjoint_iUnion_nat {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [T2Space M] (v : VectorMeasure α M) {f : ℕ → Set α} (hf₁ : ∀ (i : ℕ), MeasurableSet (f i)) (hf₂ : 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_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

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

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

theorem MeasureTheory.VectorMeasure.of_iUnion_nonneg {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [Countable β] {f : β → Set α} {M : Type u_4} [TopologicalSpace M] [OrderedAddCommMonoid 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] [OrderedAddCommMonoid 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

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 real number r and a signed measure s, smul r s is the signed measure corresponding to the function r • s.

Equations

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

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 }

@[simp]

theorem MeasureTheory.VectorMeasure.coe_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) :

↑(r • v) = r • ↑v

theorem MeasureTheory.VectorMeasure.smul_apply {α : 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) (i : Set α) :

↑(r • v) i = r • ↑v i

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.instInhabited {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] :

Inhabited (VectorMeasure α M)

Equations

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

@[simp]

theorem MeasureTheory.VectorMeasure.coe_zero {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] :

↑0 = 0

theorem MeasureTheory.VectorMeasure.zero_apply {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (i : Set α) :

↑0 i = 0

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 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 }

@[simp]

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

↑(v + w) = ↑v + ↑w

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

↑(v + w) i = ↑v i + ↑w i

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

AddCommMonoid (VectorMeasure α M)

Equations

MeasureTheory.VectorMeasure.instAddCommMonoid = Function.Injective.addCommMonoid MeasureTheory.VectorMeasure.measureOf' ⋯ ⋯ ⋯ ⋯

def MeasureTheory.VectorMeasure.coeFnAddMonoidHom {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] :

VectorMeasure α M →+ Set α → M

(⇑) is an AddMonoidHom.

Equations

MeasureTheory.VectorMeasure.coeFnAddMonoidHom = { toFun := MeasureTheory.VectorMeasure.measureOf', map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem MeasureTheory.VectorMeasure.coeFnAddMonoidHom_apply {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] (self : VectorMeasure α M) (a✝ : Set α) :

coeFnAddMonoidHom self a✝ = ↑self a✝

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 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 }

@[simp]

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

↑(-v) = -↑v

theorem MeasureTheory.VectorMeasure.neg_apply {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] (v : VectorMeasure α M) (i : Set α) :

↑(-v) i = -↑v i

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 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 }

@[simp]

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

↑(v - w) = ↑v - ↑w

theorem MeasureTheory.VectorMeasure.sub_apply {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] (v w : VectorMeasure α M) (i : Set α) :

↑(v - w) i = ↑v i - ↑w i

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

AddCommGroup (VectorMeasure α M)

Equations

MeasureTheory.VectorMeasure.instAddCommGroup = Function.Injective.addCommGroup MeasureTheory.VectorMeasure.measureOf' ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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 = Function.Injective.distribMulAction MeasureTheory.VectorMeasure.coeFnAddMonoidHom ⋯ ⋯

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 = Function.Injective.module R MeasureTheory.VectorMeasure.coeFnAddMonoidHom ⋯ ⋯

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 (μ s).toReal else 0, empty' := ⋯, not_measurable' := ⋯, m_iUnion' := ⋯ }

@[simp]

theorem MeasureTheory.Measure.toSignedMeasure_apply {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) [hμ : IsFiniteMeasure μ] (s : Set α) :

↑μ.toSignedMeasure s = if MeasurableSet s then (μ s).toReal else 0

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

↑μ.toSignedMeasure i = (μ i).toReal

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

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 = (μ i).toReal - (ν i).toReal

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

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.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 = μ

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

def MeasureTheory.VectorMeasure.map {α : Type u_1} {β : Type u_2} [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} [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} [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} [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} [MeasurableSpace α] [MeasurableSpace β] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (f : α → β) :

map 0 f = 0

def MeasureTheory.VectorMeasure.mapRange {α : Type u_1} [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} [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} [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} [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} [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 {α : Type u_1} [MeasurableSpace α] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {N : Type u_4} [AddCommMonoid N] [TopologicalSpace N] [ContinuousAdd M] [ContinuousAdd N] (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' := ⋯ }

def MeasureTheory.VectorMeasure.mapRangeₗ {α : Type u_1} [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] [ContinuousAdd M] [ContinuousAdd N] [ContinuousConstSMul R M] [ContinuousConstSMul R N] (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' := ⋯ }

def MeasureTheory.VectorMeasure.restrict {α : Type u_1} [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} [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} [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} [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} [MeasurableSpace α] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : VectorMeasure α M) :

v.restrict ∅ = 0

@[simp]

theorem MeasureTheory.VectorMeasure.restrict_univ {α : Type u_1} [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} [MeasurableSpace α] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {i : Set α} :

restrict 0 i = 0

theorem MeasureTheory.VectorMeasure.map_add {α : Type u_1} {β : Type u_2} [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

def MeasureTheory.VectorMeasure.mapGm {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] (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_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] (f : α → β) (v : VectorMeasure α M) :

(mapGm f) v = v.map f

theorem MeasureTheory.VectorMeasure.restrict_add {α : Type u_1} [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

def MeasureTheory.VectorMeasure.restrictGm {α : Type u_1} [MeasurableSpace α] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] (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 {α : Type u_1} [MeasurableSpace α] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] [ContinuousAdd M] (i : Set α) (v : VectorMeasure α M) :

(restrictGm i) v = v.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

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

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

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

MeasureTheory.VectorMeasure.instPartialOrder = PartialOrder.mk ⋯

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

Equations

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

def MeasureTheory.«term_≤[_]_».«delab_app.LE.le» :

Lean.PrettyPrinter.Delaborator.Delab

Pretty printer defined by notation3 command.

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] [OrderedAddCommGroup 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

@[simp]

theorem MeasureTheory.VectorMeasure.neg_le_neg_iff {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [OrderedAddCommGroup 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] [OrderedAddCommMonoid 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] [OrderedAddCommMonoid 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] [OrderedAddCommMonoid 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] [OrderedAddCommMonoid 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] [OrderedAddCommMonoid 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] [OrderedAddCommMonoid 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] [OrderedAddCommMonoid 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] [OrderedAddCommMonoid 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] [OrderedAddCommMonoid 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] [OrderedAddCommMonoid 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] [OrderedAddCommMonoid 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] [LinearOrderedAddCommMonoid 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) :

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

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

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

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

The underlying function for SignedMeasure.toMeasureOfZeroLE.

Equations

s.toMeasureOfZeroLE' i hi j hj = ↑⟨↑(MeasureTheory.VectorMeasure.restrict s i) j, ⋯⟩

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

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₂) ⋯ ⋯

Instances For

MeasureTheory.SignedMeasure.toMeasureOfZeroLE_finite

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 = ↑⟨↑s (i ∩ j), ⋯⟩

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

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₁ ⋯

Instances For

MeasureTheory.SignedMeasure.toMeasureOfLEZero_finite

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 = ↑⟨-↑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 ⋯ ⋯ = μ