Documentation

Mathlib.MeasureTheory.OuterMeasure.Defs

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

    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)} :
      ∀ {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 tf 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)
      Equations
      • MeasureTheory.OuterMeasure.instFunLikeSetENNReal = { coe := fun (m : MeasureTheory.OuterMeasure α) => m.measureOf, coe_injective' := }
      Equations
      • MeasureTheory.OuterMeasure.instCoeFun = inferInstance
      @[simp]