# 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)
Instances For
theorem MeasureTheory.OuterMeasure.empty {α : Type u_2} (self : ) :
self.measureOf = 0
theorem MeasureTheory.OuterMeasure.mono {α : Type u_2} (self : ) {s₁ : Set α} {s₂ : Set α} :
s₁ s₂self.measureOf s₁ self.measureOf s₂
theorem MeasureTheory.OuterMeasure.iUnion_nat {α : Type u_2} (self : ) (s : Set α) :
Pairwise (Disjoint on s)self.measureOf (⋃ (i : ), s i) ∑' (i : ), self.measureOf (s i)

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 tf s f t
• measure_iUnion_nat_le : ∀ (f : F) (s : Set α), Pairwise (Disjoint on s)f (⋃ (i : ), s i) ∑' (i : ), f (s i)
Instances
theorem MeasureTheory.OuterMeasureClass.measure_empty {F : Type u_2} {α : outParam (Type u_3)} [FunLike F (Set α) ENNReal] [self : ] (f : F) :
f = 0
theorem MeasureTheory.OuterMeasureClass.measure_mono {F : Type u_2} {α : outParam (Type u_3)} [FunLike F (Set α) ENNReal] [self : ] (f : F) {s : Set α} {t : Set α} :
s tf s f t
theorem MeasureTheory.OuterMeasureClass.measure_iUnion_nat_le {F : Type u_2} {α : outParam (Type u_3)} [FunLike F (Set α) ENNReal] [self : ] (f : F) (s : Set α) :
Pairwise (Disjoint on s)f (⋃ (i : ), s i) ∑' (i : ), f (s i)
Equations
• MeasureTheory.OuterMeasure.instFunLikeSetENNReal = { coe := fun (m : ) => m.measureOf, coe_injective' := }
instance MeasureTheory.OuterMeasure.instCoeFun {α : Type u_1} :
CoeFun fun (x : ) => Set αENNReal
Equations
• MeasureTheory.OuterMeasure.instCoeFun = inferInstance
@[simp]
theorem MeasureTheory.OuterMeasure.measureOf_eq_coe {α : Type u_1} (m : ) :
m.measureOf = m
Equations
• =