Documentation

Mathlib.MeasureTheory.OuterMeasure.Operations

Operations on outer measures #

In this file we define algebraic operations (addition, scalar multiplication) on the type of outer measures on a type. We also show that outer measures on a type α form a complete lattice.

References #

Tags #

outer measure

Equations
  • MeasureTheory.OuterMeasure.instZero = { zero := { measureOf := fun (x : Set α) => 0, empty := , mono := , iUnion_nat := } }
@[simp]
theorem MeasureTheory.OuterMeasure.coe_zero {α : Type u_1} :
0 = 0
Equations
  • MeasureTheory.OuterMeasure.instInhabited = { default := 0 }
Equations
  • MeasureTheory.OuterMeasure.instAdd = { add := fun (m₁ m₂ : MeasureTheory.OuterMeasure α) => { measureOf := fun (s : Set α) => m₁ s + m₂ s, empty := , mono := , iUnion_nat := } }
@[simp]
theorem MeasureTheory.OuterMeasure.coe_add {α : Type u_1} (m₁ : MeasureTheory.OuterMeasure α) (m₂ : MeasureTheory.OuterMeasure α) :
(m₁ + m₂) = m₁ + m₂
theorem MeasureTheory.OuterMeasure.add_apply {α : Type u_1} (m₁ : MeasureTheory.OuterMeasure α) (m₂ : MeasureTheory.OuterMeasure α) (s : Set α) :
(m₁ + m₂) s = m₁ s + m₂ s
Equations
  • MeasureTheory.OuterMeasure.instSMul = { smul := fun (c : R) (m : MeasureTheory.OuterMeasure α) => { measureOf := fun (s : Set α) => c m s, empty := , mono := , iUnion_nat := } }
@[simp]
theorem MeasureTheory.OuterMeasure.coe_smul {α : Type u_1} {R : Type u_3} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (c : R) (m : MeasureTheory.OuterMeasure α) :
(c m) = c m
theorem MeasureTheory.OuterMeasure.smul_apply {α : Type u_1} {R : Type u_3} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (c : R) (m : MeasureTheory.OuterMeasure α) (s : Set α) :
(c m) s = c m s
Equations
Equations
@[simp]
theorem MeasureTheory.OuterMeasure.coeFnAddMonoidHom_apply {α : Type u_1} :
∀ (a : MeasureTheory.OuterMeasure α) (a_1 : Set α), MeasureTheory.OuterMeasure.coeFnAddMonoidHom a a_1 = a a_1

(⇑) as an AddMonoidHom.

Equations
  • MeasureTheory.OuterMeasure.coeFnAddMonoidHom = { toFun := DFunLike.coe, map_zero' := , map_add' := }
Instances For
    Equations
    Equations
    Equations
    • MeasureTheory.OuterMeasure.instBot = { bot := 0 }
    @[simp]
    Equations
    Equations
    Equations
    • One or more equations did not get rendered due to their size.
    Equations
    @[simp]
    theorem MeasureTheory.OuterMeasure.sSup_apply {α : Type u_1} (ms : Set (MeasureTheory.OuterMeasure α)) (s : Set α) :
    (sSup ms) s = mms, m s
    @[simp]
    theorem MeasureTheory.OuterMeasure.iSup_apply {α : Type u_1} {ι : Sort u_3} (f : ιMeasureTheory.OuterMeasure α) (s : Set α) :
    (⨆ (i : ι), f i) s = ⨆ (i : ι), (f i) s
    theorem MeasureTheory.OuterMeasure.coe_iSup {α : Type u_1} {ι : Sort u_3} (f : ιMeasureTheory.OuterMeasure α) :
    (⨆ (i : ι), f i) = ⨆ (i : ι), (f i)
    @[simp]
    theorem MeasureTheory.OuterMeasure.sup_apply {α : Type u_1} (m₁ : MeasureTheory.OuterMeasure α) (m₂ : MeasureTheory.OuterMeasure α) (s : Set α) :
    (m₁ m₂) s = m₁ s m₂ s
    theorem MeasureTheory.OuterMeasure.smul_iSup {α : Type u_1} {R : Type u_3} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] {ι : Sort u_4} (f : ιMeasureTheory.OuterMeasure α) (c : R) :
    c ⨆ (i : ι), f i = ⨆ (i : ι), c f i
    theorem MeasureTheory.OuterMeasure.mono'' {α : Type u_1} {m₁ : MeasureTheory.OuterMeasure α} {m₂ : MeasureTheory.OuterMeasure α} {s₁ : Set α} {s₂ : Set α} (hm : m₁ m₂) (hs : s₁ s₂) :
    m₁ s₁ m₂ s₂

    The pushforward of m along f. The outer measure on s is defined to be m (f ⁻¹' s).

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]
      theorem MeasureTheory.OuterMeasure.map_apply {α : Type u_1} {β : Type u_3} (f : αβ) (m : MeasureTheory.OuterMeasure α) (s : Set β) :
      @[simp]
      theorem MeasureTheory.OuterMeasure.map_map {α : Type u_1} {β : Type u_3} {γ : Type u_4} (f : αβ) (g : βγ) (m : MeasureTheory.OuterMeasure α) :
      theorem MeasureTheory.OuterMeasure.map_mono {α : Type u_1} {β : Type u_3} (f : αβ) :
      @[simp]
      theorem MeasureTheory.OuterMeasure.map_iSup {α : Type u_1} {β : Type u_3} {ι : Sort u_4} (f : αβ) (m : ιMeasureTheory.OuterMeasure α) :
      (MeasureTheory.OuterMeasure.map f) (⨆ (i : ι), m i) = ⨆ (i : ι), (MeasureTheory.OuterMeasure.map f) (m i)
      Equations
      • One or more equations did not get rendered due to their size.

      The dirac outer measure.

      Equations
      Instances For
        @[simp]
        theorem MeasureTheory.OuterMeasure.dirac_apply {α : Type u_1} (a : α) (s : Set α) :
        (MeasureTheory.OuterMeasure.dirac a) s = s.indicator (fun (x : α) => 1) a

        The sum of an (arbitrary) collection of outer measures.

        Equations
        Instances For
          @[simp]
          theorem MeasureTheory.OuterMeasure.sum_apply {α : Type u_1} {ι : Type u_3} (f : ιMeasureTheory.OuterMeasure α) (s : Set α) :
          (MeasureTheory.OuterMeasure.sum f) s = ∑' (i : ι), (f i) s
          theorem MeasureTheory.OuterMeasure.smul_dirac_apply {α : Type u_1} (a : ENNReal) (b : α) (s : Set α) :
          (a MeasureTheory.OuterMeasure.dirac b) s = s.indicator (fun (x : α) => a) b

          Pullback of an OuterMeasure: comap f μ s = μ (f '' s).

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem MeasureTheory.OuterMeasure.comap_apply {α : Type u_1} {β : Type u_3} (f : αβ) (m : MeasureTheory.OuterMeasure β) (s : Set α) :
            @[simp]
            theorem MeasureTheory.OuterMeasure.comap_iSup {α : Type u_1} {β : Type u_3} {ι : Sort u_4} (f : αβ) (m : ιMeasureTheory.OuterMeasure β) :
            (MeasureTheory.OuterMeasure.comap f) (⨆ (i : ι), m i) = ⨆ (i : ι), (MeasureTheory.OuterMeasure.comap f) (m i)
            @[simp]
            theorem MeasureTheory.OuterMeasure.restrict_iSup {α : Type u_1} {ι : Sort u_3} (s : Set α) (m : ιMeasureTheory.OuterMeasure α) :
            (MeasureTheory.OuterMeasure.restrict s) (⨆ (i : ι), m i) = ⨆ (i : ι), (MeasureTheory.OuterMeasure.restrict s) (m i)
            @[simp]
            theorem MeasureTheory.OuterMeasure.top_apply {α : Type u_1} {s : Set α} (h : s.Nonempty) :
            theorem MeasureTheory.OuterMeasure.top_apply' {α : Type u_1} (s : Set α) :
            s = ⨅ (_ : s = ), 0
            @[simp]
            theorem MeasureTheory.OuterMeasure.comap_top {α : Type u_1} {β : Type u_2} (f : αβ) :