The complete lattice of measures

This file provides a complete lattice structure on the space of measures.

Tags

measure, complete lattice

@[instance_reducible]

instance MeasureTheory.Measure.instPartialOrder {α : Type u_1} {mα : MeasurableSpace α} : PartialOrder (Measure α)

Measures are partially ordered.

Equations

• MeasureTheory.Measure.instPartialOrder = { le := fun (m₁ m₂ : MeasureTheory.Measure α) => ∀ (s : Set α), m₁ s ≤ m₂ s, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

theorem MeasureTheory.Measure.toOuterMeasure_le {α : Type u_1} {mα : MeasurableSpace α} {μ₁ μ₂ : Measure α} : μ₁.toOuterMeasure ≤ μ₂.toOuterMeasure ↔ μ₁ ≤ μ₂

theorem MeasureTheory.Measure.le_iff {α : Type u_1} {mα : MeasurableSpace α} {μ₁ μ₂ : Measure α} : μ₁ ≤ μ₂ ↔ ∀ (s : Set α), MeasurableSet s → μ₁ s ≤ μ₂ s

theorem MeasureTheory.Measure.le_intro {α : Type u_1} {mα : MeasurableSpace α} {μ₁ μ₂ : Measure α} (h : ∀ (s : Set α), MeasurableSet s → s.Nonempty → μ₁ s ≤ μ₂ s) : μ₁ ≤ μ₂

theorem MeasureTheory.Measure.le_iff' {α : Type u_1} {mα : MeasurableSpace α} {μ₁ μ₂ : Measure α} : μ₁ ≤ μ₂ ↔ ∀ (s : Set α), μ₁ s ≤ μ₂ s

theorem MeasureTheory.Measure.measure_mono_left {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} (h : μ ≤ ν) (s : Set α) : μ s ≤ ν s

theorem MeasureTheory.Measure.measure_mono_both {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} {s t : Set α} (h₁ : μ ≤ ν) (h₂ : s ⊆ t) : μ s ≤ ν t

theorem MeasureTheory.Measure.lt_iff {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} : μ < ν ↔ μ ≤ ν ∧ ∃ (s : Set α), MeasurableSet s ∧ μ s < ν s

theorem MeasureTheory.Measure.lt_iff' {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} : μ < ν ↔ μ ≤ ν ∧ ∃ (s : Set α), μ s < ν s

instance MeasureTheory.Measure.instIsOrderedAddMonoid {α : Type u_1} {mα : MeasurableSpace α} : IsOrderedAddMonoid (Measure α)

theorem MeasureTheory.Measure.le_add_left {α : Type u_1} {mα : MeasurableSpace α} {μ ν ν' : Measure α} (h : μ ≤ ν) : μ ≤ ν' + ν

theorem MeasureTheory.Measure.le_add_right {α : Type u_1} {mα : MeasurableSpace α} {μ ν ν' : Measure α} (h : μ ≤ ν) : μ ≤ ν + ν'

instance MeasureTheory.Measure.instCovariantClassHSMulLeOfENNReal {α : Type u_1} {R : Type u_2} {mα : MeasurableSpace α} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] [CovariantClass R ENNReal (fun (x1 : R) (x2 : ENNReal) => x1 • x2) fun (x1 x2 : ENNReal) => x1 ≤ x2] : CovariantClass R (Measure α) (fun (x1 : R) (x2 : Measure α) => x1 • x2) fun (x1 x2 : Measure α) => x1 ≤ x2

instance MeasureTheory.Measure.instIsOrderedSMulOfENNReal {α : Type u_1} {R : Type u_2} {mα : MeasurableSpace α} [SMul R ENNReal] [LE R] [IsScalarTower R ENNReal ENNReal] [IsOrderedSMul R ENNReal] : IsOrderedSMul R (Measure α)

theorem MeasureTheory.Measure.sInf_caratheodory {α : Type u_1} {mα : MeasurableSpace α} {m : Set (Measure α)} (s : Set α) (hs : MeasurableSet s) : MeasurableSet s

@[instance_reducible]

noncomputable instance MeasureTheory.Measure.instInfSet {α : Type u_1} {mα : MeasurableSpace α} : InfSet (Measure α)

Equations

• MeasureTheory.Measure.instInfSet = { sInf := fun (m : Set (MeasureTheory.Measure α)) => (sInf (MeasureTheory.Measure.toOuterMeasure '' m)).toMeasure ⋯ }

theorem MeasureTheory.Measure.sInf_apply {α : Type u_1} {mα : MeasurableSpace α} {s : Set α} {m : Set (Measure α)} (hs : MeasurableSet s) : (sInf m) s = (sInf (toOuterMeasure '' m)) s

@[instance_reducible]

noncomputable instance MeasureTheory.Measure.instCompleteSemilatticeInf {α : Type u_1} {mα : MeasurableSpace α} : CompleteSemilatticeInf (Measure α)

Equations

• MeasureTheory.Measure.instCompleteSemilatticeInf = { toPartialOrder := MeasureTheory.Measure.instPartialOrder, toInfSet := MeasureTheory.Measure.instInfSet, isGLB_sInf := ⋯ }

@[instance_reducible]

noncomputable instance MeasureTheory.Measure.instCompleteLattice {α : Type u_1} {mα : MeasurableSpace α} : CompleteLattice (Measure α)

Equations

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

theorem MeasureTheory.Measure.inf_apply {α : Type u_1} {mα : MeasurableSpace α} {μ ν : Measure α} {s : Set α} (hs : MeasurableSet s) : (μ ⊓ ν) s = sInf {m : ENNReal | ∃ (t : Set α), m = μ (t ∩ s) + ν (tᶜ ∩ s)}

@[simp]

theorem MeasureTheory.OuterMeasure.toMeasure_top {α : Type u_1} {mα : MeasurableSpace α} : ⊤.toMeasure ⋯ = ⊤

@[simp]

theorem MeasureTheory.Measure.toOuterMeasure_top {α : Type u_1} {mα : MeasurableSpace α} : ⊤.toOuterMeasure = ⊤

@[simp]

theorem MeasureTheory.Measure.top_add {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} : ⊤ + μ = ⊤

@[simp]

theorem MeasureTheory.Measure.add_top {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} : μ + ⊤ = ⊤

theorem MeasureTheory.Measure.zero_le {α : Type u_1} {mα : MeasurableSpace α} (μ : Measure α) : 0 ≤ μ

theorem MeasureTheory.Measure.nonpos_iff_eq_zero' {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} : μ ≤ 0 ↔ μ = 0

@[simp]

theorem MeasureTheory.Measure.measure_univ_eq_zero {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} : μ Set.univ = 0 ↔ μ = 0

theorem MeasureTheory.Measure.measure_univ_ne_zero {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} : μ Set.univ ≠ 0 ↔ μ ≠ 0

instance MeasureTheory.Measure.instNeZeroENNRealCoeSetUniv {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} [NeZero μ] : NeZero (μ Set.univ)

@[simp]

theorem MeasureTheory.Measure.measure_univ_pos {α : Type u_1} {mα : MeasurableSpace α} {μ : Measure α} : 0 < μ Set.univ ↔ μ ≠ 0

theorem MeasureTheory.Measure.nonempty_of_neZero {α : Type u_1} {mα : MeasurableSpace α} (μ : Measure α) [NeZero μ] : Nonempty α