# 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.

## 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₂ : ) => { measureOf := fun (s : Set α) => m₁ s + m₂ s, empty := , mono := , iUnion_nat := } }
@[simp]
theorem MeasureTheory.OuterMeasure.coe_add {α : Type u_1} (m₁ : ) (m₂ : ) :
(m₁ + m₂) = m₁ + m₂
theorem MeasureTheory.OuterMeasure.add_apply {α : Type u_1} (m₁ : ) (m₂ : ) (s : Set α) :
(m₁ + m₂) s = m₁ s + m₂ s
instance MeasureTheory.OuterMeasure.instSMul {α : Type u_1} {R : Type u_3} [] :
Equations
• MeasureTheory.OuterMeasure.instSMul = { smul := fun (c : R) (m : ) => { measureOf := fun (s : Set α) => c m s, empty := , mono := , iUnion_nat := } }
@[simp]
theorem MeasureTheory.OuterMeasure.coe_smul {α : Type u_1} {R : Type u_3} [] (c : R) (m : ) :
(c m) = c m
theorem MeasureTheory.OuterMeasure.smul_apply {α : Type u_1} {R : Type u_3} [] (c : R) (m : ) (s : Set α) :
(c m) s = c m s
instance MeasureTheory.OuterMeasure.instSMulCommClass {α : Type u_1} {R : Type u_3} [] {R' : Type u_4} [] [] [] :
Equations
• =
instance MeasureTheory.OuterMeasure.instIsScalarTower {α : Type u_1} {R : Type u_3} [] {R' : Type u_4} [] [] [SMul R R'] [] :
Equations
• =
instance MeasureTheory.OuterMeasure.instIsCentralScalar {α : Type u_1} {R : Type u_3} [] [] :
Equations
• =
instance MeasureTheory.OuterMeasure.instMulAction {α : Type u_1} {R : Type u_3} [] [] :
Equations
Equations
@[simp]
theorem MeasureTheory.OuterMeasure.coeFnAddMonoidHom_apply {α : Type u_1} :
∀ (a : ) (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
instance MeasureTheory.OuterMeasure.instDistribMulAction {α : Type u_1} {R : Type u_3} [] :
Equations
instance MeasureTheory.OuterMeasure.instModule {α : Type u_1} {R : Type u_3} [] [] :
Equations
Equations
• MeasureTheory.OuterMeasure.instBot = { bot := 0 }
@[simp]
Equations
• MeasureTheory.OuterMeasure.instPartialOrder =
Equations
• MeasureTheory.OuterMeasure.orderBot =
theorem MeasureTheory.OuterMeasure.univ_eq_zero_iff {α : Type u_1} (m : ) :
m Set.univ = 0 m = 0
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem MeasureTheory.OuterMeasure.sSup_apply {α : Type u_1} (ms : ) (s : Set α) :
(sSup ms) s = mms, m s
@[simp]
theorem MeasureTheory.OuterMeasure.iSup_apply {α : Type u_1} {ι : Sort u_3} (f : ) (s : Set α) :
(⨆ (i : ι), f i) s = ⨆ (i : ι), (f i) s
theorem MeasureTheory.OuterMeasure.coe_iSup {α : Type u_1} {ι : Sort u_3} (f : ) :
(⨆ (i : ι), f i) = ⨆ (i : ι), (f i)
@[simp]
theorem MeasureTheory.OuterMeasure.sup_apply {α : Type u_1} (m₁ : ) (m₂ : ) (s : Set α) :
(m₁ m₂) s = m₁ s m₂ s
theorem MeasureTheory.OuterMeasure.smul_iSup {α : Type u_1} {R : Type u_3} [] {ι : Sort u_4} (f : ) (c : R) :
c ⨆ (i : ι), f i = ⨆ (i : ι), c f i
theorem MeasureTheory.OuterMeasure.mono'' {α : Type u_1} {m₁ : } {m₂ : } {s₁ : Set α} {s₂ : Set α} (hm : m₁ m₂) (hs : s₁ s₂) :
m₁ s₁ m₂ s₂
def MeasureTheory.OuterMeasure.map {α : Type u_1} {β : Type u_3} (f : αβ) :

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 : ) (s : Set β) :
() s = m (f ⁻¹' s)
@[simp]
theorem MeasureTheory.OuterMeasure.map_id {α : Type u_1} (m : ) :
= m
@[simp]
theorem MeasureTheory.OuterMeasure.map_map {α : Type u_1} {β : Type u_3} {γ : Type u_4} (f : αβ) (g : βγ) (m : ) :
= () m
theorem MeasureTheory.OuterMeasure.map_mono {α : Type u_1} {β : Type u_3} (f : αβ) :
@[simp]
theorem MeasureTheory.OuterMeasure.map_sup {α : Type u_1} {β : Type u_3} (f : αβ) (m : ) (m' : ) :
(m m') =
@[simp]
theorem MeasureTheory.OuterMeasure.map_iSup {α : Type u_1} {β : Type u_3} {ι : Sort u_4} (f : αβ) (m : ) :
(⨆ (i : ι), m i) = ⨆ (i : ι), (m i)
Equations
• One or more equations did not get rendered due to their size.
def MeasureTheory.OuterMeasure.dirac {α : Type u_1} (a : α) :

The dirac outer measure.

Equations
• = { measureOf := fun (s : Set α) => s.indicator (fun (x : α) => 1) a, empty := , mono := , iUnion_nat := }
Instances For
@[simp]
theorem MeasureTheory.OuterMeasure.dirac_apply {α : Type u_1} (a : α) (s : Set α) :
= s.indicator (fun (x : α) => 1) a
def MeasureTheory.OuterMeasure.sum {α : Type u_1} {ι : Type u_3} (f : ) :

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

Equations
• = { measureOf := fun (s : Set α) => ∑' (i : ι), (f i) s, empty := , mono := , iUnion_nat := }
Instances For
@[simp]
theorem MeasureTheory.OuterMeasure.sum_apply {α : Type u_1} {ι : Type u_3} (f : ) (s : Set α) :
= ∑' (i : ι), (f i) s
theorem MeasureTheory.OuterMeasure.smul_dirac_apply {α : Type u_1} (a : ENNReal) (b : α) (s : Set α) :
= s.indicator (fun (x : α) => a) b
def MeasureTheory.OuterMeasure.comap {α : Type u_1} {β : Type u_3} (f : αβ) :

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 : ) (s : Set α) :
() s = m (f '' s)
theorem MeasureTheory.OuterMeasure.comap_mono {α : Type u_1} {β : Type u_3} (f : αβ) :
@[simp]
theorem MeasureTheory.OuterMeasure.comap_iSup {α : Type u_1} {β : Type u_3} {ι : Sort u_4} (f : αβ) (m : ) :
(⨆ (i : ι), m i) = ⨆ (i : ι), (m i)
def MeasureTheory.OuterMeasure.restrict {α : Type u_1} (s : Set α) :

Restrict an OuterMeasure to a set.

Equations
Instances For
@[simp]
theorem MeasureTheory.OuterMeasure.restrict_apply {α : Type u_1} (s : Set α) (t : Set α) (m : ) :
t = m (t s)
theorem MeasureTheory.OuterMeasure.restrict_mono {α : Type u_1} {s : Set α} {t : Set α} (h : s t) {m : } {m' : } (hm : m m') :
@[simp]
theorem MeasureTheory.OuterMeasure.restrict_univ {α : Type u_1} (m : ) :
() m = m
@[simp]
@[simp]
theorem MeasureTheory.OuterMeasure.restrict_iSup {α : Type u_1} {ι : Sort u_3} (s : Set α) (m : ) :
(⨆ (i : ι), m i) = ⨆ (i : ι), (m i)
theorem MeasureTheory.OuterMeasure.map_comap {α : Type u_1} {β : Type u_3} (f : αβ) (m : ) :
theorem MeasureTheory.OuterMeasure.map_comap_le {α : Type u_1} {β : Type u_3} (f : αβ) (m : ) :
theorem MeasureTheory.OuterMeasure.restrict_le_self {α : Type u_1} (m : ) (s : Set α) :
@[simp]
theorem MeasureTheory.OuterMeasure.map_le_restrict_range {α : Type u_1} {β : Type u_3} {ma : } {mb : } {f : αβ} :
mb
theorem MeasureTheory.OuterMeasure.map_comap_of_surjective {α : Type u_1} {β : Type u_3} {f : αβ} (hf : ) (m : ) :
theorem MeasureTheory.OuterMeasure.le_comap_map {α : Type u_1} {β : Type u_3} (f : αβ) (m : ) :
theorem MeasureTheory.OuterMeasure.comap_map {α : Type u_1} {β : Type u_3} {f : αβ} (hf : ) (m : ) :
@[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 : αβ) :
theorem MeasureTheory.OuterMeasure.map_top {α : Type u_1} {β : Type u_2} (f : αβ) :
@[simp]
theorem MeasureTheory.OuterMeasure.map_top_of_surjective {α : Type u_1} {β : Type u_2} (f : αβ) (hf : ) :