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 MeasureTheory.OuterMeasure.instZero {α : Type u_1} : Zero (MeasureTheory.OuterMeasure α)

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

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

Equations

• MeasureTheory.OuterMeasure.instInhabited = { default := 0 }

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

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₁ m₂ : MeasureTheory.OuterMeasure α) : ⇑(m₁ + m₂) = ⇑m₁ + ⇑m₂

theorem MeasureTheory.OuterMeasure.add_apply {α : Type u_1} (m₁ m₂ : MeasureTheory.OuterMeasure α) (s : Set α) : (m₁ + m₂) s = m₁ s + m₂ s

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

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

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' (MeasureTheory.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' (MeasureTheory.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 (MeasureTheory.OuterMeasure α)

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

Equations

• MeasureTheory.OuterMeasure.instMulAction = Function.Injective.mulAction (fun (μ : MeasureTheory.OuterMeasure α) (s : Set α) => μ s) ⋯ ⋯

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

Equations

• MeasureTheory.OuterMeasure.addCommMonoid = Function.Injective.addCommMonoid (let_fun this := fun (μ : MeasureTheory.OuterMeasure α) (s : Set α) => μ s; this) ⋯ ⋯ ⋯ ⋯

def MeasureTheory.OuterMeasure.coeFnAddMonoidHom {α : Type u_1} : MeasureTheory.OuterMeasure α →+ Set α → ENNReal

(⇑) as an AddMonoidHom.

Equations

• MeasureTheory.OuterMeasure.coeFnAddMonoidHom = { toFun := DFunLike.coe, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem MeasureTheory.OuterMeasure.coeFnAddMonoidHom_apply {α : Type u_1} (a✝ : MeasureTheory.OuterMeasure α) (a : Set α) : MeasureTheory.OuterMeasure.coeFnAddMonoidHom a✝ a = a✝ a

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

Equations

• MeasureTheory.OuterMeasure.instDistribMulAction = Function.Injective.distribMulAction MeasureTheory.OuterMeasure.coeFnAddMonoidHom ⋯ ⋯

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

Equations

• MeasureTheory.OuterMeasure.instModule = Function.Injective.module R MeasureTheory.OuterMeasure.coeFnAddMonoidHom ⋯ ⋯

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

Equations

• MeasureTheory.OuterMeasure.instBot = { bot := 0 }

@[simp]

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

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

Equations

• MeasureTheory.OuterMeasure.instPartialOrder = PartialOrder.mk ⋯

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

Equations

• MeasureTheory.OuterMeasure.orderBot = OrderBot.mk ⋯

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

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• MeasureTheory.OuterMeasure.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem MeasureTheory.OuterMeasure.sSup_apply {α : Type u_1} (ms : Set (MeasureTheory.OuterMeasure α)) (s : Set α) : (sSup ms) s = ⨆ m ∈ ms, 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₁ 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₁ m₂ : MeasureTheory.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 : α → β) : MeasureTheory.OuterMeasure α →ₗ[ENNReal] MeasureTheory.OuterMeasure β

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.

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[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)

instance MeasureTheory.OuterMeasure.instFunctor : Functor MeasureTheory.OuterMeasure

Equations

• One or more equations did not get rendered due to their size.

instance MeasureTheory.OuterMeasure.instLawfulFunctor : LawfulFunctor MeasureTheory.OuterMeasure

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

The dirac outer measure.

Equations

• MeasureTheory.OuterMeasure.dirac a = { measureOf := fun (s : Set α) => s.indicator (fun (x : α) => 1) a, empty := ⋯, mono := ⋯, iUnion_nat := ⋯ }

@[simp]

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

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

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

Equations

• MeasureTheory.OuterMeasure.sum f = { measureOf := fun (s : Set α) => ∑' (i : ι), (f i) s, empty := ⋯, mono := ⋯, iUnion_nat := ⋯ }

@[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

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

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

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

@[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)

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

Restrict an OuterMeasure to a set.

Equations

• MeasureTheory.OuterMeasure.restrict s = MeasureTheory.OuterMeasure.map Subtype.val ∘ₗ MeasureTheory.OuterMeasure.comap Subtype.val

@[simp]

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

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

@[simp]

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

@[simp]

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

@[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)

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

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

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

@[simp]

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

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

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

theorem MeasureTheory.OuterMeasure.comap_map {α : Type u_1} {β : Type u_3} {f : α → β} (hf : Function.Injective f) (m : MeasureTheory.OuterMeasure α) : (MeasureTheory.OuterMeasure.comap f) ((MeasureTheory.OuterMeasure.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 : α → β) : (MeasureTheory.OuterMeasure.comap f) ⊤ = ⊤

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

@[simp]

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