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

• https://en.wikipedia.org/wiki/Outer_measure

Tags

outer measure

@[instance_reducible]

instance MeasureTheory.OuterMeasure.instZero {α : Type u_1} : Zero (OuterMeasure α)

instance MeasureTheory.OuterMeasure.instIsZeroApplySetENNReal {α : Type u_1} : IsZeroApply (OuterMeasure α)

@[deprecated FunLike.coe_zero (since := "2026-06-23")]

theorem MeasureTheory.OuterMeasure.coe_zero {F : Type u_2} {α : Type u_4} {β : Type u_5} [FunLike F α β] [Zero F] [Zero β] [IsZeroApply F] : ⇑0 = 0

Alias of FunLike.coe_zero.

@[instance_reducible]

instance MeasureTheory.OuterMeasure.instInhabited {α : Type u_1} : Inhabited (OuterMeasure α)

@[instance_reducible]

instance MeasureTheory.OuterMeasure.instAdd {α : Type u_1} : Add (OuterMeasure α)

instance MeasureTheory.OuterMeasure.instIsAddApplySetENNReal {α : Type u_1} : IsAddApply (OuterMeasure α)

@[deprecated FunLike.coe_add (since := "2026-06-23")]

theorem MeasureTheory.OuterMeasure.coe_add {F : Type u_2} {α : Type u_4} {β : Type u_5} [FunLike F α β] [Add F] [Add β] [IsAddApply F] (f g : F) : ⇑(f + g) = ⇑f + ⇑g

Alias of FunLike.coe_add.

@[deprecated add_apply (since := "2026-06-23")]

theorem MeasureTheory.OuterMeasure.add_apply {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst✝ : FunLike F α β} {inst✝¹ : Add β} {inst✝² : Add F} [self : IsAddApply F] (f g : F) (x : α) : (f + g) x = f x + g x

Alias of add_apply.

@[instance_reducible]

instance MeasureTheory.OuterMeasure.instSMul {α : Type u_1} {R : Type u_3} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] : SMul R (OuterMeasure α)

instance MeasureTheory.OuterMeasure.instIsSMulApplySetENNReal {α : Type u_1} {R : Type u_3} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] : IsSMulApply R (OuterMeasure α)

@[deprecated FunLike.coe_smul (since := "2026-06-23")]

theorem MeasureTheory.OuterMeasure.coe_smul {M : Type u_1} {F : Type u_2} {α : Type u_4} {β : Type u_5} [FunLike F α β] [SMul M F] [SMul M β] [IsSMulApply M F] (n : M) (f : F) : ⇑(n • f) = n • ⇑f

Alias of FunLike.coe_smul.

@[deprecated smul_apply (since := "2026-06-23")]

theorem MeasureTheory.OuterMeasure.smul_apply {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst✝ : FunLike F α β} {inst✝¹ : SMul M β} {inst✝² : SMul M F} [self : IsSMulApply M F] (f : F) (n : M) (x : α) : (n • f) x = n • f x

Alias of smul_apply.

instance MeasureTheory.OuterMeasure.instSMulCommClass {α : Type u_1} {R : Type u_3} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] {R' : Type u_4} [SMul R' ENNReal] [IsScalarTower R' ENNReal ENNReal] [SMulCommClass R R' ENNReal] : SMulCommClass R R' (OuterMeasure α)

instance MeasureTheory.OuterMeasure.instIsScalarTower {α : Type u_1} {R : Type u_3} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] {R' : Type u_4} [SMul R' ENNReal] [IsScalarTower R' ENNReal ENNReal] [SMul R R'] [IsScalarTower R R' ENNReal] : IsScalarTower R R' (OuterMeasure α)

instance MeasureTheory.OuterMeasure.instIsCentralScalar {α : Type u_1} {R : Type u_3} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] [SMul Rᵐᵒᵖ ENNReal] [IsCentralScalar R ENNReal] : IsCentralScalar R (OuterMeasure α)

@[instance_reducible]

instance MeasureTheory.OuterMeasure.instMulAction {α : Type u_1} {R : Type u_3} [Monoid R] [MulAction R ENNReal] [IsScalarTower R ENNReal ENNReal] : MulAction R (OuterMeasure α)

@[instance_reducible]

instance MeasureTheory.OuterMeasure.addCommMonoid {α : Type u_1} : AddCommMonoid (OuterMeasure α)

@[deprecated FunLike.coeAddMonoidHom (since := "2026-06-23")]

def MeasureTheory.OuterMeasure.coeFnAddMonoidHom (F : Type u_1) (α : Type u_2) (β : Type u_3) [FunLike F α β] [AddZero F] [AddZeroClass β] [IsZeroApply F] [IsAddApply F] : F →+ α → β

Alias of FunLike.coeAddMonoidHom.

@[deprecated FunLike.coeAddMonoidHom_apply (since := "2026-06-23")]

theorem MeasureTheory.OuterMeasure.coeFnAddMonoidHom_apply {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] [AddZero F] [AddZeroClass β] [IsZeroApply F] [IsAddApply F] (f : F) : (FunLike.coeAddMonoidHom F α β) f = ⇑f

Alias of FunLike.coeAddMonoidHom_apply.

@[instance_reducible]

instance MeasureTheory.OuterMeasure.instDistribMulAction {α : Type u_1} {R : Type u_3} [Monoid R] [DistribMulAction R ENNReal] [IsScalarTower R ENNReal ENNReal] : DistribMulAction R (OuterMeasure α)

@[instance_reducible]

instance MeasureTheory.OuterMeasure.instModule {α : Type u_1} {R : Type u_3} [Semiring R] [Module R ENNReal] [IsScalarTower R ENNReal ENNReal] : Module R (OuterMeasure α)

@[instance_reducible]

instance MeasureTheory.OuterMeasure.instBot {α : Type u_1} : Bot (OuterMeasure α)

@[simp]

theorem MeasureTheory.OuterMeasure.coe_bot {α : Type u_1} : ⊥ = 0

@[instance_reducible]

instance MeasureTheory.OuterMeasure.instPartialOrder {α : Type u_1} : PartialOrder (OuterMeasure α)

instance MeasureTheory.OuterMeasure.instIsOrderedAddMonoid {α : Type u_3} : IsOrderedAddMonoid (OuterMeasure α)

@[instance_reducible]

instance MeasureTheory.OuterMeasure.orderBot {α : Type u_1} : OrderBot (OuterMeasure α)

theorem MeasureTheory.OuterMeasure.univ_eq_zero_iff {α : Type u_1} (m : OuterMeasure α) : m Set.univ = 0 ↔ m = 0

@[instance_reducible]

noncomputable instance MeasureTheory.OuterMeasure.instSupSet {α : Type u_1} : SupSet (OuterMeasure α)

@[instance_reducible]

noncomputable instance MeasureTheory.OuterMeasure.instCompleteLattice {α : Type u_1} : CompleteLattice (OuterMeasure α)

@[simp]

theorem MeasureTheory.OuterMeasure.sSup_apply {α : Type u_1} (ms : Set (OuterMeasure α)) (s : Set α) : (sSup ms) s = ⨆ m ∈ ms, m s

@[simp]

theorem MeasureTheory.OuterMeasure.iSup_apply {α : Type u_1} {ι : Sort u_3} (f : ι → OuterMeasure α) (s : Set α) : (⨆ (i : ι), f i) s = ⨆ (i : ι), (f i) s

theorem MeasureTheory.OuterMeasure.coe_iSup {α : Type u_1} {ι : Sort u_3} (f : ι → OuterMeasure α) : ⇑(⨆ (i : ι), f i) = ⨆ (i : ι), ⇑(f i)

@[simp]

theorem MeasureTheory.OuterMeasure.sup_apply {α : Type u_1} (m₁ m₂ : OuterMeasure α) (s : Set α) : (m₁ ⊔ m₂) s = max (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 : ι → OuterMeasure α) (c : R) : c • ⨆ (i : ι), f i = ⨆ (i : ι), c • f i

theorem MeasureTheory.OuterMeasure.mono'' {α : Type u_1} {m₁ m₂ : OuterMeasure α} {s₁ s₂ : Set α} (hm : m₁ ≤ m₂) (hs : s₁ ⊆ s₂) : m₁ s₁ ≤ m₂ s₂

def MeasureTheory.OuterMeasure.map {α : Type u_1} {β : Type u_3} (f : α → β) : OuterMeasure α →ₗ[ENNReal] OuterMeasure β

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

@[simp]

theorem MeasureTheory.OuterMeasure.map_apply {α : Type u_1} {β : Type u_3} (f : α → β) (m : OuterMeasure α) (s : Set β) : ((map f) m) s = m (f ⁻¹' s)

@[simp]

theorem MeasureTheory.OuterMeasure.map_id {α : Type u_1} (m : OuterMeasure α) : (map id) m = m

@[simp]

theorem MeasureTheory.OuterMeasure.map_map {α : Type u_1} {β : Type u_3} {γ : Type u_4} (f : α → β) (g : β → γ) (m : OuterMeasure α) : (map g) ((map f) m) = (map (g ∘ f)) m

theorem MeasureTheory.OuterMeasure.map_mono {α : Type u_1} {β : Type u_3} (f : α → β) : Monotone ⇑(map f)

@[simp]

theorem MeasureTheory.OuterMeasure.map_sup {α : Type u_1} {β : Type u_3} (f : α → β) (m m' : OuterMeasure α) : (map f) (m ⊔ m') = (map f) m ⊔ (map f) m'

@[simp]

theorem MeasureTheory.OuterMeasure.map_iSup {α : Type u_1} {β : Type u_3} {ι : Sort u_4} (f : α → β) (m : ι → OuterMeasure α) : (map f) (⨆ (i : ι), m i) = ⨆ (i : ι), (map f) (m i)

@[instance_reducible]

instance MeasureTheory.OuterMeasure.instFunctor : Functor OuterMeasure

instance MeasureTheory.OuterMeasure.instLawfulFunctor : LawfulFunctor OuterMeasure

noncomputable def MeasureTheory.OuterMeasure.dirac {α : Type u_1} (a : α) : OuterMeasure α

The dirac outer measure.

@[simp]

theorem MeasureTheory.OuterMeasure.dirac_apply {α : Type u_1} (a : α) (s : Set α) : (dirac a) s = s.indicator (fun (x : α) => 1) a

noncomputable def MeasureTheory.OuterMeasure.sum {α : Type u_1} {ι : Type u_3} (f : ι → OuterMeasure α) : OuterMeasure α

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

@[simp]

theorem MeasureTheory.OuterMeasure.sum_apply {α : Type u_1} {ι : Type u_3} (f : ι → OuterMeasure α) (s : Set α) : (sum f) s = ∑' (i : ι), (f i) s

theorem MeasureTheory.OuterMeasure.smul_dirac_apply {α : Type u_1} (a : ENNReal) (b : α) (s : Set α) : (a • dirac b) s = s.indicator (fun (x : α) => a) b

def MeasureTheory.OuterMeasure.comap {α : Type u_1} {β : Type u_3} (f : α → β) : OuterMeasure β →ₗ[ENNReal] OuterMeasure α

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

@[simp]

theorem MeasureTheory.OuterMeasure.comap_apply {α : Type u_1} {β : Type u_3} (f : α → β) (m : OuterMeasure β) (s : Set α) : ((comap f) m) s = m (f '' s)

theorem MeasureTheory.OuterMeasure.comap_mono {α : Type u_1} {β : Type u_3} (f : α → β) : Monotone ⇑(comap f)

@[simp]

theorem MeasureTheory.OuterMeasure.comap_iSup {α : Type u_1} {β : Type u_3} {ι : Sort u_4} (f : α → β) (m : ι → OuterMeasure β) : (comap f) (⨆ (i : ι), m i) = ⨆ (i : ι), (comap f) (m i)

noncomputable def MeasureTheory.OuterMeasure.restrict {α : Type u_1} (s : Set α) : OuterMeasure α →ₗ[ENNReal] OuterMeasure α

Restrict an OuterMeasure to a set.

@[simp]

theorem MeasureTheory.OuterMeasure.restrict_apply {α : Type u_1} (s t : Set α) (m : OuterMeasure α) : ((restrict s) m) t = m (t ∩ s)

theorem MeasureTheory.OuterMeasure.restrict_mono {α : Type u_1} {s t : Set α} (h : s ⊆ t) {m m' : OuterMeasure α} (hm : m ≤ m') : (restrict s) m ≤ (restrict t) m'

@[simp]

theorem MeasureTheory.OuterMeasure.restrict_univ {α : Type u_1} (m : OuterMeasure α) : (restrict Set.univ) m = m

@[simp]

theorem MeasureTheory.OuterMeasure.restrict_empty {α : Type u_1} (m : OuterMeasure α) : (restrict ∅) m = 0

@[simp]

theorem MeasureTheory.OuterMeasure.restrict_iSup {α : Type u_1} {ι : Sort u_3} (s : Set α) (m : ι → OuterMeasure α) : (restrict s) (⨆ (i : ι), m i) = ⨆ (i : ι), (restrict s) (m i)

theorem MeasureTheory.OuterMeasure.map_comap {α : Type u_1} {β : Type u_3} (f : α → β) (m : OuterMeasure β) : (map f) ((comap f) m) = (restrict (Set.range f)) m

theorem MeasureTheory.OuterMeasure.map_comap_le {α : Type u_1} {β : Type u_3} (f : α → β) (m : OuterMeasure β) : (map f) ((comap f) m) ≤ m

theorem MeasureTheory.OuterMeasure.restrict_le_self {α : Type u_1} (m : OuterMeasure α) (s : Set α) : (restrict s) m ≤ m

@[simp]

theorem MeasureTheory.OuterMeasure.map_le_restrict_range {α : Type u_1} {β : Type u_3} {ma : OuterMeasure α} {mb : OuterMeasure β} {f : α → β} : (map f) ma ≤ (restrict (Set.range f)) mb ↔ (map f) ma ≤ mb

theorem MeasureTheory.OuterMeasure.map_comap_of_surjective {α : Type u_1} {β : Type u_3} {f : α → β} (hf : Function.Surjective f) (m : OuterMeasure β) : (map f) ((comap f) m) = m

theorem MeasureTheory.OuterMeasure.le_comap_map {α : Type u_1} {β : Type u_3} (f : α → β) (m : OuterMeasure α) : m ≤ (comap f) ((map f) m)

theorem MeasureTheory.OuterMeasure.comap_map {α : Type u_1} {β : Type u_3} {f : α → β} (hf : Function.Injective f) (m : OuterMeasure α) : (comap f) ((map f) m) = m

@[simp]

theorem MeasureTheory.OuterMeasure.top_apply {α : Type u_1} {s : Set α} (h : s.Nonempty) : ⊤ s = ⊤

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 : α → β) : (comap f) ⊤ = ⊤

theorem MeasureTheory.OuterMeasure.map_top {α : Type u_1} {β : Type u_2} (f : α → β) : (map f) ⊤ = (restrict (Set.range f)) ⊤

@[simp]

theorem MeasureTheory.OuterMeasure.map_top_of_surjective {α : Type u_1} {β : Type u_2} (f : α → β) (hf : Function.Surjective f) : (map f) ⊤ = ⊤