# Vector-valued measures #

This file defines vector-valued measures, which are σ-additive functions from a set to an additive monoid `M` such that it maps the empty set and non-measurable sets to zero. In the case that `M = ℝ`, we called the vector measure a signed measure and write `SignedMeasure α`. Similarly, when `M = ℂ`, we call the measure a complex measure and write `ComplexMeasure α` (defined in `MeasureTheory/Measure/Complex`).

## Main definitions #

- `MeasureTheory.VectorMeasure` is a vector-valued, σ-additive function that maps the empty and non-measurable 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

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

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

- measureOf' : Set α → M

  The measure of sets

- empty' : ↑self ∅ = 0

  The empty set has measure zero

- not_measurable' ⦃i : Set α⦄ : ¬MeasurableSet i → ↑self i = 0

  Non-measurable sets have measure zero

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

  The measure is σ-additive

Instances For

source
@[reducible, inline]
abbrev MeasureTheory.SignedMeasure (α : Type u_3) [MeasurableSpace α] :
Type u_3

A `SignedMeasure` is an `ℝ`-vector measure.

Equations

- MeasureTheory.SignedMeasure α = MeasureTheory.VectorMeasure α ℝ

Instances For

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

source
@[simp]
theorem MeasureTheory.VectorMeasure.empty {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : VectorMeasure α M) :
↑v ∅ = 0
source
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
source
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))
source
theorem MeasureTheory.VectorMeasure.coe_injective {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] :
Function.Injective measureOf'
source
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
source
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
source
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
source
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))
source
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)
source
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
source
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
source
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
source
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
source
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)
source
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
source
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
source
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
source
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' := ⋯ }

Instances For

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

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

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

source
@[simp]
theorem MeasureTheory.VectorMeasure.coe_zero {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] :
↑0 = 0
source
theorem MeasureTheory.VectorMeasure.zero_apply {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (i : Set α) :
↑0 i = 0
source
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' := ⋯ }

Instances For

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

source
@[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
source
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
source
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' ⋯ ⋯ ⋯ ⋯

source
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' := ⋯ }

Instances For

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

Instances For

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

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

Instances For

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

source
@[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
source
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
source
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' ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

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

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

source
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' := ⋯ }

Instances For

source
@[simp]
theorem MeasureTheory.Measure.toSignedMeasure_apply {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) [hμ : IsFiniteMeasure μ] (s : Set α) :
↑μ.toSignedMeasure s = if MeasurableSet s then μ.real s else 0
source
theorem MeasureTheory.Measure.toSignedMeasure_apply_measurable {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} [IsFiniteMeasure μ] {i : Set α} (hi : MeasurableSet i) :
↑μ.toSignedMeasure i = μ.real i
source
theorem MeasureTheory.Measure.toSignedMeasure_congr {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h : μ = ν) :
μ.toSignedMeasure = ν.toSignedMeasure
source
theorem MeasureTheory.Measure.toSignedMeasure_eq_toSignedMeasure_iff {α : Type u_1} {m : MeasurableSpace α} {μ ν : Measure α} [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
μ.toSignedMeasure = ν.toSignedMeasure ↔ μ = ν
source
@[simp]
theorem MeasureTheory.Measure.toSignedMeasure_zero {α : Type u_1} {m : MeasurableSpace α} :
toSignedMeasure 0 = 0
source
@[simp]
theorem MeasureTheory.Measure.toSignedMeasure_add {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
(μ + ν).toSignedMeasure = μ.toSignedMeasure + ν.toSignedMeasure
source
@[simp]
theorem MeasureTheory.Measure.toSignedMeasure_smul {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] (r : NNReal) :
(r • μ).toSignedMeasure = r • μ.toSignedMeasure
source
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' := ⋯ }

Instances For

source
@[simp]
theorem MeasureTheory.Measure.toENNRealVectorMeasure_apply {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) (i : Set α) :
↑μ.toENNRealVectorMeasure i = if MeasurableSet i then μ i else 0
source
theorem MeasureTheory.Measure.toENNRealVectorMeasure_apply_measurable {α : Type u_1} {m : MeasurableSpace α} {μ : Measure α} {i : Set α} (hi : MeasurableSet i) :
↑μ.toENNRealVectorMeasure i = μ i
source
@[simp]
theorem MeasureTheory.Measure.toENNRealVectorMeasure_zero {α : Type u_1} {m : MeasurableSpace α} :
toENNRealVectorMeasure 0 = 0
source
@[simp]
theorem MeasureTheory.Measure.toENNRealVectorMeasure_add {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) :
(μ + ν).toENNRealVectorMeasure = μ.toENNRealVectorMeasure + ν.toENNRealVectorMeasure
source
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
source
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) ⋯ ⋯

Instances For

source
theorem MeasureTheory.VectorMeasure.ennrealToMeasure_apply {α : Type u_1} {m : MeasurableSpace α} {v : VectorMeasure α ENNReal} {s : Set α} (hs : MeasurableSet s) :
v.ennrealToMeasure s = ↑v s
source
@[simp]
theorem MeasureTheory.Measure.toENNRealVectorMeasure_ennrealToMeasure {α : Type u_1} {m : MeasurableSpace α} (μ : VectorMeasure α ENNReal) :
μ.ennrealToMeasure.toENNRealVectorMeasure = μ
source
@[simp]
theorem MeasureTheory.VectorMeasure.ennrealToMeasure_toENNRealVectorMeasure {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) :
μ.toENNRealVectorMeasure.ennrealToMeasure = μ
source
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 := ⋯ }

Instances For

source
@[simp]
theorem MeasureTheory.VectorMeasure.equivMeasure_apply {α : Type u_1} [MeasurableSpace α] (v : VectorMeasure α ENNReal) :
equivMeasure v = v.ennrealToMeasure
source
@[simp]
theorem MeasureTheory.VectorMeasure.equivMeasure_symm_apply {α : Type u_1} [MeasurableSpace α] (μ : Measure α) :
equivMeasure.symm μ = μ.toENNRealVectorMeasure
source
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

Instances For

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

Instances For

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

Instances For

source
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' := ⋯ }

Instances For

source
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

Instances For

source
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
source
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)
source
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
source
@[simp]
theorem MeasureTheory.VectorMeasure.restrict_empty {α : Type u_1} [MeasurableSpace α] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] (v : VectorMeasure α M) :
v.restrict ∅ = 0
source
@[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
source
@[simp]
theorem MeasureTheory.VectorMeasure.restrict_zero {α : Type u_1} [MeasurableSpace α] {M : Type u_3} [AddCommMonoid M] [TopologicalSpace M] {i : Set α} :
restrict 0 i = 0
source
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
source
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' := ⋯ }

Instances For

source
@[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
source
@[simp]
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
source
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' := ⋯ }

Instances For

source
@[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
source
@[simp]
theorem MeasureTheory.VectorMeasure.restrict_add_restrict_compl {α : Type u_1} [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
source
@[simp]
theorem MeasureTheory.VectorMeasure.restrict_neg {α : Type u_1} [MeasurableSpace α] {M : Type u_4} [AddCommGroup M] [TopologicalSpace M] [IsTopologicalAddGroup M] (v : VectorMeasure α M) (i : Set α) :
(-v).restrict i = -v.restrict i
source
@[simp]
theorem MeasureTheory.VectorMeasure.restrict_sub {α : Type u_1} [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
source
@[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
source
@[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
source
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' := ⋯ }

Instances For

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

Instances For

source
@[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
source
instance MeasureTheory.VectorMeasure.instPartialOrder {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] :
PartialOrder (VectorMeasure α M)

Vector measures over a partially ordered monoid is partially ordered.

This definition is consistent with `Measure.instPartialOrder`.

Equations

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

source
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
source
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
source
def MeasureTheory.«term_≤[_]_» :
Lean.TrailingParserDescr

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

Equations

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

Instances For

source
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
source
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
source
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
source
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
source
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 ∅
source
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
source
theorem MeasureTheory.VectorMeasure.neg_le_neg {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommGroup M] [PartialOrder M] [IsOrderedAddMonoid M] [IsTopologicalAddGroup M] (v w : VectorMeasure α M) {i : Set α} (hi : MeasurableSet i) (h : v.restrict i ≤ w.restrict i) :
(-w).restrict i ≤ (-v).restrict i
source
theorem MeasureTheory.VectorMeasure.neg_le_neg_iff {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommGroup M] [PartialOrder M] [IsOrderedAddMonoid M] [IsTopologicalAddGroup M] (v w : VectorMeasure α M) {i : Set α} (hi : MeasurableSet i) :
(-w).restrict i ≤ (-v).restrict i ↔ v.restrict i ≤ w.restrict i
source
theorem MeasureTheory.VectorMeasure.restrict_le_restrict_iUnion {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] [OrderClosedTopology M] (v w : VectorMeasure α M) {f : ℕ → Set α} (hf₁ : ∀ (n : ℕ), MeasurableSet (f n)) (hf₂ : ∀ (n : ℕ), v.restrict (f n) ≤ w.restrict (f n)) :
v.restrict (⋃ (n : ℕ), f n) ≤ w.restrict (⋃ (n : ℕ), f n)
source
theorem MeasureTheory.VectorMeasure.restrict_le_restrict_countable_iUnion {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] [OrderClosedTopology M] (v w : VectorMeasure α M) [Countable β] {f : β → Set α} (hf₁ : ∀ (b : β), MeasurableSet (f b)) (hf₂ : ∀ (b : β), v.restrict (f b) ≤ w.restrict (f b)) :
v.restrict (⋃ (b : β), f b) ≤ w.restrict (⋃ (b : β), f b)
source
theorem MeasureTheory.VectorMeasure.restrict_le_restrict_union {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] [OrderClosedTopology M] (v w : VectorMeasure α M) {i j : Set α} (hi₁ : MeasurableSet i) (hi₂ : v.restrict i ≤ w.restrict i) (hj₁ : MeasurableSet j) (hj₂ : v.restrict j ≤ w.restrict j) :
v.restrict (i ∪ j) ≤ w.restrict (i ∪ j)
source
theorem MeasureTheory.VectorMeasure.nonneg_of_zero_le_restrict {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v : VectorMeasure α M) {i : Set α} (hi₂ : restrict 0 i ≤ v.restrict i) :
0 ≤ ↑v i
source
theorem MeasureTheory.VectorMeasure.nonpos_of_restrict_le_zero {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v : VectorMeasure α M) {i : Set α} (hi₂ : v.restrict i ≤ restrict 0 i) :
↑v i ≤ 0
source
theorem MeasureTheory.VectorMeasure.zero_le_restrict_not_measurable {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v : VectorMeasure α M) {i : Set α} (hi : ¬MeasurableSet i) :
restrict 0 i ≤ v.restrict i
source
theorem MeasureTheory.VectorMeasure.restrict_le_zero_of_not_measurable {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v : VectorMeasure α M) {i : Set α} (hi : ¬MeasurableSet i) :
v.restrict i ≤ restrict 0 i
source
theorem MeasureTheory.VectorMeasure.measurable_of_not_zero_le_restrict {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v : VectorMeasure α M) {i : Set α} (hi : ¬restrict 0 i ≤ v.restrict i) :
MeasurableSet i
source
theorem MeasureTheory.VectorMeasure.measurable_of_not_restrict_le_zero {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v : VectorMeasure α M) {i : Set α} (hi : ¬v.restrict i ≤ restrict 0 i) :
MeasurableSet i
source
theorem MeasureTheory.VectorMeasure.zero_le_restrict_subset {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v : VectorMeasure α M) {i j : Set α} (hi₁ : MeasurableSet i) (hij : j ⊆ i) (hi₂ : restrict 0 i ≤ v.restrict i) :
restrict 0 j ≤ v.restrict j
source
theorem MeasureTheory.VectorMeasure.restrict_le_zero_subset {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [PartialOrder M] (v : VectorMeasure α M) {i j : Set α} (hi₁ : MeasurableSet i) (hij : j ⊆ i) (hi₂ : v.restrict i ≤ restrict 0 i) :
v.restrict j ≤ restrict 0 j
source
theorem MeasureTheory.VectorMeasure.exists_pos_measure_of_not_restrict_le_zero {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [TopologicalSpace M] [AddCommMonoid M] [LinearOrder M] (v : VectorMeasure α M) {i : Set α} (hi : ¬v.restrict i ≤ restrict 0 i) :
∃ (j : Set α), MeasurableSet j ∧ j ⊆ i ∧ 0 < ↑v j
source
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)
source
def MeasureTheory.VectorMeasure.AbsolutelyContinuous {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] (v : VectorMeasure α M) (w : VectorMeasure α N) :
Prop

A vector measure `v` is absolutely continuous with respect to a measure `μ` if for all sets `s`, `μ s = 0`, we have `v s = 0`.

Equations

- v.AbsolutelyContinuous w = ∀ ⦃s : Set α⦄, ↑w s = 0 → ↑v s = 0

Instances For

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

Instances For

source
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
source
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
source
theorem MeasureTheory.VectorMeasure.AbsolutelyContinuous.refl {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [AddCommMonoid M] [TopologicalSpace M] (v : VectorMeasure α M) :
v.AbsolutelyContinuous v
source
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
source
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
source
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
source
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)
source
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
source
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
source
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
source
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)
source
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 μ
source
def MeasureTheory.VectorMeasure.MutuallySingular {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [AddCommMonoid M] [TopologicalSpace M] [AddCommMonoid N] [TopologicalSpace N] (v : VectorMeasure α M) (w : VectorMeasure α N) :
Prop

Two vector measures `v` and `w` are said to be mutually singular if there exists a measurable set `s`, such that for all `t ⊆ s`, `v t = 0` and for all `t ⊆ sᶜ`, `w t = 0`.

We note that we do not require the measurability of `t` in the definition since this makes it easier to use. This is equivalent to the definition which requires measurability. To prove `MutuallySingular` with the measurability condition, use `MeasureTheory.VectorMeasure.MutuallySingular.mk`.

Equations

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

Instances For

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

Instances For

source
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
source
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
source
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
source
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
source
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
source
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₂)
source
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)
source
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
source
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
source
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)
source
@[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
source
@[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
source
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' := ⋯ }

Instances For

source
@[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
source
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
source
@[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
source
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
source
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
source
def MeasureTheory.SignedMeasure.toMeasureOfZeroLE' {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (i : Set α) (hi : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i) (j : Set α) (hj : MeasurableSet j) :
ENNReal

The underlying function for `SignedMeasure.toMeasureOfZeroLE`.

Equations

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

Instances For

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

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

Equations

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

Instances For

source
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), ⋯⟩
source
theorem MeasureTheory.SignedMeasure.toMeasureOfZeroLE_real_apply {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) {i j : Set α} (hi : VectorMeasure.restrict 0 i ≤ VectorMeasure.restrict s i) (hi₁ : MeasurableSet i) (hj₁ : MeasurableSet j) :
(s.toMeasureOfZeroLE i hi₁ hi).real j = ↑s (i ∩ j)
source
def MeasureTheory.SignedMeasure.toMeasureOfLEZero {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) (i : Set α) (hi₁ : MeasurableSet i) (hi₂ : VectorMeasure.restrict s i ≤ VectorMeasure.restrict 0 i) :
Measure α

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

Equations

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

Instances For

source
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), ⋯⟩
source
theorem MeasureTheory.SignedMeasure.toMeasureOfLEZero_real_apply {α : Type u_1} {m : MeasurableSpace α} (s : SignedMeasure α) {i j : Set α} (hi : VectorMeasure.restrict s i ≤ VectorMeasure.restrict 0 i) (hi₁ : MeasurableSet i) (hj₁ : MeasurableSet j) :
(s.toMeasureOfLEZero i hi₁ hi).real j = -↑s (i ∩ j)
source
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.

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

source
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
source
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
source
theorem MeasureTheory.Measure.zero_le_toSignedMeasure {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] :
0 ≤ μ.toSignedMeasure
source
theorem MeasureTheory.Measure.toSignedMeasure_toMeasureOfZeroLE {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] :
μ.toSignedMeasure.toMeasureOfZeroLE Set.univ ⋯ ⋯ = μ
source
theorem MeasureTheory.Measure.toSignedMeasure_restrict_eq_restrict_toSignedMeasure {α : Type u_1} {m : MeasurableSpace α} (μ : Measure α) [IsFiniteMeasure μ] (s : Set α) (hs : MeasurableSet s) :
VectorMeasure.restrict μ.toSignedMeasure s = (μ.restrict s).toSignedMeasure
source
theorem MeasureTheory.Measure.toSignedMeasure_le_toSignedMeasure_iff {α : Type u_1} {m : MeasurableSpace α} (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
μ.toSignedMeasure ≤ ν.toSignedMeasure ↔ μ ≤ ν