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 (Function.onFun Disjoint 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 (Function.onFun Disjoint s) → f (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), f (s i)

instance MeasureTheory.OuterMeasure.instFunLikeSetENNReal {α : Type u_1} : FunLike (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 : OuterMeasure α) : m.measureOf = ⇑m

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