Definitions of an outer measure and the corresponding FunLike class

In this file we define MeasureTheory.OuterMeasure α to be the type of outer measures on α.

An outer measure is a function μ : Set α → ℝ≥0∞, from the powerset of a type to the extended nonnegative real numbers that satisfies the following conditions:

1. μ ∅ = 0;
2. μ is monotone;
3. μ is countably subadditive. This means that the outer measure of a countable union is at most the sum of the outer measure on the individual sets.

Note that we do not need α to be measurable to define an outer measure.

We also define a typeclass MeasureTheory.OuterMeasureClass.

References

https://en.wikipedia.org/wiki/Outer_measure

Tags

outer measure

structure MeasureTheory.OuterMeasure (α : Type u_2) : Type u_2

An outer measure is a countably subadditive monotone function that sends ∅ to 0.

• measureOf : Set α → ENNReal

  Outer measure function. Use automatic coercion instead.

• empty : self.measureOf ∅ = 0
• mono : ∀ {s₁ s₂ : Set α}, s₁ ⊆ s₂ → self.measureOf s₁ ≤ self.measureOf s₂
• iUnion_nat : ∀ (s : ℕ → Set α), Pairwise (Disjoint on s) → self.measureOf (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), self.measureOf (s i)

theorem MeasureTheory.OuterMeasure.empty {α : Type u_2} (self : MeasureTheory.OuterMeasure α) : self.measureOf ∅ = 0

theorem MeasureTheory.OuterMeasure.mono {α : Type u_2} (self : MeasureTheory.OuterMeasure α) {s₁ : Set α} {s₂ : Set α} : s₁ ⊆ s₂ → self.measureOf s₁ ≤ self.measureOf s₂

theorem MeasureTheory.OuterMeasure.iUnion_nat {α : Type u_2} (self : MeasureTheory.OuterMeasure α) (s : ℕ → Set α) : Pairwise (Disjoint on s) → self.measureOf (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), self.measureOf (s i)

class MeasureTheory.OuterMeasureClass (F : Type u_2) (α : outParam (Type u_3)) [FunLike F (Set α) ENNReal] : Prop

A mixin class saying that elements μ : F are outer measures on α.

This typeclass is used to unify some API for outer measures and measures.

• measure_empty : ∀ (f : F), f ∅ = 0
• measure_mono : ∀ (f : F) {s t : Set α}, s ⊆ t → f s ≤ f t
• measure_iUnion_nat_le : ∀ (f : F) (s : ℕ → Set α), Pairwise (Disjoint on s) → f (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), f (s i)

theorem MeasureTheory.OuterMeasureClass.measure_empty {F : Type u_2} {α : outParam (Type u_3)} : ∀ {inst : FunLike F (Set α) ENNReal} [self : MeasureTheory.OuterMeasureClass F α] (f : F), f ∅ = 0

theorem MeasureTheory.OuterMeasureClass.measure_mono {F : Type u_2} {α : outParam (Type u_3)} : ∀ {inst : FunLike F (Set α) ENNReal} [self : MeasureTheory.OuterMeasureClass F α] (f : F) {s t : Set α}, s ⊆ t → f s ≤ f t

theorem MeasureTheory.OuterMeasureClass.measure_iUnion_nat_le {F : Type u_2} {α : outParam (Type u_3)} : ∀ {inst : FunLike F (Set α) ENNReal} [self : MeasureTheory.OuterMeasureClass F α] (f : F) (s : ℕ → Set α), Pairwise (Disjoint on s) → f (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), f (s i)

instance MeasureTheory.OuterMeasure.instFunLikeSetENNReal {α : Type u_1} : FunLike (MeasureTheory.OuterMeasure α) (Set α) ENNReal

Equations

• MeasureTheory.OuterMeasure.instFunLikeSetENNReal = { coe := fun (m : MeasureTheory.OuterMeasure α) => m.measureOf, coe_injective' := ⋯ }

@[simp]

theorem MeasureTheory.OuterMeasure.measureOf_eq_coe {α : Type u_1} (m : MeasureTheory.OuterMeasure α) : m.measureOf = ⇑m

instance MeasureTheory.OuterMeasure.instOuterMeasureClass {α : Type u_1} : MeasureTheory.OuterMeasureClass (MeasureTheory.OuterMeasure α) α

Equations

• ⋯ = ⋯