# 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

source
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)

Instances For

source
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)

Instances

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

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

source
@[simp]
theorem MeasureTheory.OuterMeasure.measureOf_eq_coe {α : Type u_1} (m : OuterMeasure α) :
m.measureOf = ⇑m
source
instance MeasureTheory.OuterMeasure.instOuterMeasureClass {α : Type u_1} :
OuterMeasureClass (OuterMeasure α) α