Order structure on vector measures

This file defines the pointwise order on vector measures, comparison after restriction to a set, and the conversion of nonnegative or nonpositive parts of signed measures to ordinary measures.

Main definitions

• VectorMeasure.instPartialOrder is the pointwise partial order on vector measures.
• v ≤[i] w means that v.restrict i ≤ w.restrict i.
• SignedMeasure.toMeasureOfZeroLE and SignedMeasure.toMeasureOfLEZero turn positive and negative restrictions of signed measures into ordinary measures.

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.

@[instance_reducible]

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

Vector measures over a partially ordered monoid is partially ordered.

This definition is consistent with Measure.instPartialOrder.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

The underlying function for SignedMeasure.toMeasureOfZeroLE.

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

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

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

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

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

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

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

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

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

SignedMeasure.toMeasureOfZeroLE is a finite measure.

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

SignedMeasure.toMeasureOfLEZero is a finite measure.

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

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

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

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

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

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