Outer Measures

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.

The outer measures on a type α form a complete lattice.

Given an arbitrary function m : Set α → ℝ≥0∞ that sends ∅ to 0 we can define an outer measure on α that on s is defined to be the infimum of ∑ᵢ, m (sᵢ) for all collections of sets sᵢ that cover s. This is the unique maximal outer measure that is at most the given function. We also define this for functions m defined on a subset of Set α, by treating the function as having value ∞ outside its domain.

Given an outer measure m, the Carathéodory-measurable sets are the sets s such that for all sets t we have m t = m (t ∩ s) + m (t \ s). This forms a measurable space.

Main definitions and statements

• OuterMeasure.boundedBy is the greatest outer measure that is at most the given function. If you know that the given function sends ∅ to 0, then OuterMeasure.ofFunction is a special case.
• caratheodory is the Carathéodory-measurable space of an outer measure.
• sInf_eq_boundedBy_sInfGen is a characterization of the infimum of outer measures.
• inducedOuterMeasure is the measure induced by a function on a subset of Set α

References

Tags

outer measure, Carathéodory-measurable, Carathéodory's criterion

structure MeasureTheory.OuterMeasure (α : Type u_1) : Type u_1

An outer measure is a countably subadditive monotone function that sends ∅ to 0.

• measureOf : Set α → ENNReal
• empty : ↑self ∅ = 0
• mono : ∀ {s₁ s₂ : Set α}, s₁ ⊆ s₂ → ↑self s₁ ≤ ↑self s₂
• iUnion_nat : ∀ (s : ℕ → Set α), ↑self (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), ↑self (s i)

instance MeasureTheory.OuterMeasure.instCoeFun {α : Type u_1} : CoeFun (MeasureTheory.OuterMeasure α) fun (x : MeasureTheory.OuterMeasure α) => Set α → ENNReal

Equations

• MeasureTheory.OuterMeasure.instCoeFun = { coe := fun (m : MeasureTheory.OuterMeasure α) => ↑m }

@[simp]

theorem MeasureTheory.OuterMeasure.empty' {α : Type u_1} (m : MeasureTheory.OuterMeasure α) : ↑m ∅ = 0

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

theorem MeasureTheory.OuterMeasure.mono_null {α : Type u_1} (m : MeasureTheory.OuterMeasure α) {s : Set α} {t : Set α} (h : s ⊆ t) (ht : ↑m t = 0) : ↑m s = 0

theorem MeasureTheory.OuterMeasure.pos_of_subset_ne_zero {α : Type u_1} (m : MeasureTheory.OuterMeasure α) {a : Set α} {b : Set α} (hs : a ⊆ b) (hnz : ↑m a ≠ 0) : 0 < ↑m b

theorem MeasureTheory.OuterMeasure.iUnion {α : Type u_1} (m : MeasureTheory.OuterMeasure α) {β : Type u_5} [Countable β] (s : β → Set α) : ↑m (⋃ (i : β), s i) ≤ ∑' (i : β), ↑m (s i)

theorem MeasureTheory.OuterMeasure.biUnion_null_iff {α : Type u_1} {β : Type u_2} (m : MeasureTheory.OuterMeasure α) {s : Set β} (hs : Set.Countable s) {t : β → Set α} : ↑m (⋃ i ∈ s, t i) = 0 ↔ ∀ i ∈ s, ↑m (t i) = 0

theorem MeasureTheory.OuterMeasure.sUnion_null_iff {α : Type u_1} (m : MeasureTheory.OuterMeasure α) {S : Set (Set α)} (hS : Set.Countable S) : ↑m (⋃₀ S) = 0 ↔ ∀ s ∈ S, ↑m s = 0

@[simp]

theorem MeasureTheory.OuterMeasure.iUnion_null_iff {α : Type u_1} {ι : Sort u_5} [Countable ι] (m : MeasureTheory.OuterMeasure α) {s : ι → Set α} : ↑m (⋃ (i : ι), s i) = 0 ↔ ∀ (i : ι), ↑m (s i) = 0

theorem MeasureTheory.OuterMeasure.iUnion_null {α : Type u_1} {ι : Sort u_5} [Countable ι] (m : MeasureTheory.OuterMeasure α) {s : ι → Set α} : (∀ (i : ι), ↑m (s i) = 0) → ↑m (⋃ (i : ι), s i) = 0

Alias of the reverse direction of MeasureTheory.OuterMeasure.iUnion_null_iff.

@[deprecated]

theorem MeasureTheory.OuterMeasure.iUnion_null_iff' {α : Type u_1} (m : MeasureTheory.OuterMeasure α) {ι : Prop} {s : ι → Set α} : ↑m (⋃ (i : ι), s i) = 0 ↔ ∀ (i : ι), ↑m (s i) = 0

theorem MeasureTheory.OuterMeasure.iUnion_finset {α : Type u_1} {β : Type u_2} (m : MeasureTheory.OuterMeasure α) (s : β → Set α) (t : Finset β) : ↑m (⋃ i ∈ t, s i) ≤ Finset.sum t fun (i : β) => ↑m (s i)

theorem MeasureTheory.OuterMeasure.union {α : Type u_1} (m : MeasureTheory.OuterMeasure α) (s₁ : Set α) (s₂ : Set α) : ↑m (s₁ ∪ s₂) ≤ ↑m s₁ + ↑m s₂

theorem MeasureTheory.OuterMeasure.null_of_locally_null {α : Type u_1} [TopologicalSpace α] [SecondCountableTopology α] (m : MeasureTheory.OuterMeasure α) (s : Set α) (hs : ∀ x ∈ s, ∃ u ∈ nhdsWithin x s, ↑m u = 0) : ↑m s = 0

If a set has zero measure in a neighborhood of each of its points, then it has zero measure in a second-countable space.

theorem MeasureTheory.OuterMeasure.exists_mem_forall_mem_nhds_within_pos {α : Type u_1} [TopologicalSpace α] [SecondCountableTopology α] (m : MeasureTheory.OuterMeasure α) {s : Set α} (hs : ↑m s ≠ 0) : ∃ x ∈ s, ∀ t ∈ nhdsWithin x s, 0 < ↑m t

If m s ≠ 0, then for some point x ∈ s and any t ∈ 𝓝[s] x we have 0 < m t.

theorem MeasureTheory.OuterMeasure.iUnion_of_tendsto_zero {α : Type u_1} {ι : Type u_5} (m : MeasureTheory.OuterMeasure α) {s : ι → Set α} (l : Filter ι) [Filter.NeBot l] (h0 : Filter.Tendsto (fun (k : ι) => ↑m ((⋃ (n : ι), s n) \ s k)) l (nhds 0)) : ↑m (⋃ (n : ι), s n) = ⨆ (n : ι), ↑m (s n)

If s : ι → Set α is a sequence of sets, S = ⋃ n, s n, and m (S \ s n) tends to zero along some nontrivial filter (usually atTop on ι = ℕ), then m S = ⨆ n, m (s n).

theorem MeasureTheory.OuterMeasure.iUnion_nat_of_monotone_of_tsum_ne_top {α : Type u_1} (m : MeasureTheory.OuterMeasure α) {s : ℕ → Set α} (h_mono : ∀ (n : ℕ), s n ⊆ s (n + 1)) (h0 : ∑' (k : ℕ), ↑m (s (k + 1) \ s k) ≠ ⊤) : ↑m (⋃ (n : ℕ), s n) = ⨆ (n : ℕ), ↑m (s n)

If s : ℕ → Set α is a monotone sequence of sets such that ∑' k, m (s (k + 1) \ s k) ≠ ∞, then m (⋃ n, s n) = ⨆ n, m (s n).

theorem MeasureTheory.OuterMeasure.le_inter_add_diff {α : Type u_1} {m : MeasureTheory.OuterMeasure α} {t : Set α} (s : Set α) : ↑m t ≤ ↑m (t ∩ s) + ↑m (t \ s)

theorem MeasureTheory.OuterMeasure.diff_null {α : Type u_1} (m : MeasureTheory.OuterMeasure α) (s : Set α) {t : Set α} (ht : ↑m t = 0) : ↑m (s \ t) = ↑m s

theorem MeasureTheory.OuterMeasure.union_null {α : Type u_1} (m : MeasureTheory.OuterMeasure α) {s₁ : Set α} {s₂ : Set α} (h₁ : ↑m s₁ = 0) (h₂ : ↑m s₂ = 0) : ↑m (s₁ ∪ s₂) = 0

theorem MeasureTheory.OuterMeasure.coe_fn_injective {α : Type u_1} : Function.Injective fun (μ : MeasureTheory.OuterMeasure α) (s : Set α) => ↑μ s

theorem MeasureTheory.OuterMeasure.ext {α : Type u_1} {μ₁ : MeasureTheory.OuterMeasure α} {μ₂ : MeasureTheory.OuterMeasure α} (h : ∀ (s : Set α), ↑μ₁ s = ↑μ₂ s) : μ₁ = μ₂

theorem MeasureTheory.OuterMeasure.ext_nonempty {α : Type u_1} {μ₁ : MeasureTheory.OuterMeasure α} {μ₂ : MeasureTheory.OuterMeasure α} (h : ∀ (s : Set α), Set.Nonempty s → ↑μ₁ s = ↑μ₂ s) : μ₁ = μ₂

A version of MeasureTheory.OuterMeasure.ext that assumes μ₁ s = μ₂ s on all nonempty sets s, and gets μ₁ ∅ = μ₂ ∅ from MeasureTheory.OuterMeasure.empty'.

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

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

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

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

Equations

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

@[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} {R' : Type u_4} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] [SMul R' ENNReal] [IsScalarTower R' ENNReal ENNReal] [SMulCommClass R R' ENNReal] : SMulCommClass R R' (MeasureTheory.OuterMeasure α)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

@[simp]

theorem MeasureTheory.OuterMeasure.coeFnAddMonoidHom_apply {α : Type u_1} (self : MeasureTheory.OuterMeasure α) : ∀ (a : Set α), MeasureTheory.OuterMeasure.coeFnAddMonoidHom self a = ↑self a

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

(⇑) as an AddMonoidHom.

Equations

• MeasureTheory.OuterMeasure.coeFnAddMonoidHom = { toZeroHom := { toFun := MeasureTheory.OuterMeasure.measureOf, map_zero' := ⋯ }, map_add' := ⋯ }

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

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

@[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_5} (f : ι → MeasureTheory.OuterMeasure α) (s : Set α) : ↑(⨆ (i : ι), f i) s = ⨆ (i : ι), ↑(f i) s

theorem MeasureTheory.OuterMeasure.coe_iSup {α : Type u_1} {ι : Sort u_5} (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_5} (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₂

def MeasureTheory.OuterMeasure.map {α : Type u_1} {β : Type u_5} (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_5} (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_5} {γ : Type u_6} (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_5} (f : α → β) : Monotone ⇑(MeasureTheory.OuterMeasure.map f)

@[simp]

theorem MeasureTheory.OuterMeasure.map_sup {α : Type u_1} {β : Type u_5} (f : α → β) (m : MeasureTheory.OuterMeasure α) (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_5} {ι : Sort u_6} (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

Equations

• MeasureTheory.OuterMeasure.instLawfulFunctor = ⋯

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

The dirac outer measure.

Equations

• MeasureTheory.OuterMeasure.dirac a = { measureOf := fun (s : Set α) => Set.indicator s (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 = Set.indicator s (fun (x : α) => 1) a

def MeasureTheory.OuterMeasure.sum {α : Type u_1} {ι : Type u_5} (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_5} (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 = Set.indicator s (fun (x : α) => a) b

def MeasureTheory.OuterMeasure.comap {α : Type u_1} {β : Type u_5} (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_5} (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_5} (f : α → β) : Monotone ⇑(MeasureTheory.OuterMeasure.comap f)

@[simp]

theorem MeasureTheory.OuterMeasure.comap_iSup {α : Type u_1} {β : Type u_5} {ι : Sort u_6} (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 = LinearMap.comp (MeasureTheory.OuterMeasure.map Subtype.val) (MeasureTheory.OuterMeasure.comap Subtype.val)

@[simp]

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

theorem MeasureTheory.OuterMeasure.restrict_mono {α : Type u_1} {s : Set α} {t : Set α} (h : s ⊆ t) {m : MeasureTheory.OuterMeasure α} {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_5} (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_5} (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_5} (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_5} {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_5} {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_5} (f : α → β) (m : MeasureTheory.OuterMeasure α) : m ≤ (MeasureTheory.OuterMeasure.comap f) ((MeasureTheory.OuterMeasure.map f) m)

theorem MeasureTheory.OuterMeasure.comap_map {α : Type u_1} {β : Type u_5} {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 : Set.Nonempty s) : ↑⊤ 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) ⊤ = ⊤

def MeasureTheory.OuterMeasure.ofFunction {α : Type u_1} (m : Set α → ENNReal) (m_empty : m ∅ = 0) : MeasureTheory.OuterMeasure α

Given any function m assigning measures to sets satisying m ∅ = 0, there is a unique maximal outer measure μ satisfying μ s ≤ m s for all s : Set α.

Equations

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

theorem MeasureTheory.OuterMeasure.ofFunction_apply {α : Type u_1} (m : Set α → ENNReal) (m_empty : m ∅ = 0) (s : Set α) : ↑(MeasureTheory.OuterMeasure.ofFunction m m_empty) s = ⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), m (t n)

theorem MeasureTheory.OuterMeasure.ofFunction_le {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} (s : Set α) : ↑(MeasureTheory.OuterMeasure.ofFunction m m_empty) s ≤ m s

theorem MeasureTheory.OuterMeasure.ofFunction_eq {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} (s : Set α) (m_mono : ∀ ⦃t : Set α⦄, s ⊆ t → m s ≤ m t) (m_subadd : ∀ (s : ℕ → Set α), m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), m (s i)) : ↑(MeasureTheory.OuterMeasure.ofFunction m m_empty) s = m s

theorem MeasureTheory.OuterMeasure.le_ofFunction {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} {μ : MeasureTheory.OuterMeasure α} : μ ≤ MeasureTheory.OuterMeasure.ofFunction m m_empty ↔ ∀ (s : Set α), ↑μ s ≤ m s

theorem MeasureTheory.OuterMeasure.isGreatest_ofFunction {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} : IsGreatest {μ : MeasureTheory.OuterMeasure α | ∀ (s : Set α), ↑μ s ≤ m s} (MeasureTheory.OuterMeasure.ofFunction m m_empty)

theorem MeasureTheory.OuterMeasure.ofFunction_eq_sSup {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} : MeasureTheory.OuterMeasure.ofFunction m m_empty = sSup {μ : MeasureTheory.OuterMeasure α | ∀ (s : Set α), ↑μ s ≤ m s}

theorem MeasureTheory.OuterMeasure.ofFunction_union_of_top_of_nonempty_inter {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} {s : Set α} {t : Set α} (h : ∀ (u : Set α), Set.Nonempty (s ∩ u) → Set.Nonempty (t ∩ u) → m u = ⊤) : ↑(MeasureTheory.OuterMeasure.ofFunction m m_empty) (s ∪ t) = ↑(MeasureTheory.OuterMeasure.ofFunction m m_empty) s + ↑(MeasureTheory.OuterMeasure.ofFunction m m_empty) t

If m u = ∞ for any set u that has nonempty intersection both with s and t, then μ (s ∪ t) = μ s + μ t, where μ = MeasureTheory.OuterMeasure.ofFunction m m_empty.

E.g., if α is an (e)metric space and m u = ∞ on any set of diameter ≥ r, then this lemma implies that μ (s ∪ t) = μ s + μ t on any two sets such that r ≤ edist x y for all x ∈ s and y ∈ t.

theorem MeasureTheory.OuterMeasure.comap_ofFunction {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} {β : Type u_2} (f : β → α) (h : Monotone m ∨ Function.Surjective f) : (MeasureTheory.OuterMeasure.comap f) (MeasureTheory.OuterMeasure.ofFunction m m_empty) = MeasureTheory.OuterMeasure.ofFunction (fun (s : Set β) => m (f '' s)) ⋯

theorem MeasureTheory.OuterMeasure.map_ofFunction_le {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} {β : Type u_2} (f : α → β) : (MeasureTheory.OuterMeasure.map f) (MeasureTheory.OuterMeasure.ofFunction m m_empty) ≤ MeasureTheory.OuterMeasure.ofFunction (fun (s : Set β) => m (f ⁻¹' s)) m_empty

theorem MeasureTheory.OuterMeasure.map_ofFunction {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} {β : Type u_2} {f : α → β} (hf : Function.Injective f) : (MeasureTheory.OuterMeasure.map f) (MeasureTheory.OuterMeasure.ofFunction m m_empty) = MeasureTheory.OuterMeasure.ofFunction (fun (s : Set β) => m (f ⁻¹' s)) m_empty

theorem MeasureTheory.OuterMeasure.restrict_ofFunction {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} (s : Set α) (hm : Monotone m) : (MeasureTheory.OuterMeasure.restrict s) (MeasureTheory.OuterMeasure.ofFunction m m_empty) = MeasureTheory.OuterMeasure.ofFunction (fun (t : Set α) => m (t ∩ s)) ⋯

theorem MeasureTheory.OuterMeasure.smul_ofFunction {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} {c : ENNReal} (hc : c ≠ ⊤) : c • MeasureTheory.OuterMeasure.ofFunction m m_empty = MeasureTheory.OuterMeasure.ofFunction (c • m) ⋯

def MeasureTheory.OuterMeasure.boundedBy {α : Type u_1} (m : Set α → ENNReal) : MeasureTheory.OuterMeasure α

Given any function m assigning measures to sets, there is a unique maximal outer measure μ satisfying μ s ≤ m s for all s : Set α. This is the same as OuterMeasure.ofFunction, except that it doesn't require m ∅ = 0.

Equations

• MeasureTheory.OuterMeasure.boundedBy m = MeasureTheory.OuterMeasure.ofFunction (fun (s : Set α) => ⨆ (_ : Set.Nonempty s), m s) ⋯

theorem MeasureTheory.OuterMeasure.boundedBy_le {α : Type u_1} {m : Set α → ENNReal} (s : Set α) : ↑(MeasureTheory.OuterMeasure.boundedBy m) s ≤ m s

theorem MeasureTheory.OuterMeasure.boundedBy_eq_ofFunction {α : Type u_1} {m : Set α → ENNReal} (m_empty : m ∅ = 0) (s : Set α) : ↑(MeasureTheory.OuterMeasure.boundedBy m) s = ↑(MeasureTheory.OuterMeasure.ofFunction m m_empty) s

theorem MeasureTheory.OuterMeasure.boundedBy_apply {α : Type u_1} {m : Set α → ENNReal} (s : Set α) : ↑(MeasureTheory.OuterMeasure.boundedBy m) s = ⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨆ (_ : Set.Nonempty (t n)), m (t n)

theorem MeasureTheory.OuterMeasure.boundedBy_eq {α : Type u_1} {m : Set α → ENNReal} (s : Set α) (m_empty : m ∅ = 0) (m_mono : ∀ ⦃t : Set α⦄, s ⊆ t → m s ≤ m t) (m_subadd : ∀ (s : ℕ → Set α), m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), m (s i)) : ↑(MeasureTheory.OuterMeasure.boundedBy m) s = m s

@[simp]

theorem MeasureTheory.OuterMeasure.boundedBy_eq_self {α : Type u_1} (m : MeasureTheory.OuterMeasure α) : MeasureTheory.OuterMeasure.boundedBy ↑m = m

theorem MeasureTheory.OuterMeasure.le_boundedBy {α : Type u_1} {m : Set α → ENNReal} {μ : MeasureTheory.OuterMeasure α} : μ ≤ MeasureTheory.OuterMeasure.boundedBy m ↔ ∀ (s : Set α), ↑μ s ≤ m s

theorem MeasureTheory.OuterMeasure.le_boundedBy' {α : Type u_1} {m : Set α → ENNReal} {μ : MeasureTheory.OuterMeasure α} : μ ≤ MeasureTheory.OuterMeasure.boundedBy m ↔ ∀ (s : Set α), Set.Nonempty s → ↑μ s ≤ m s

@[simp]

theorem MeasureTheory.OuterMeasure.boundedBy_top {α : Type u_1} : MeasureTheory.OuterMeasure.boundedBy ⊤ = ⊤

@[simp]

theorem MeasureTheory.OuterMeasure.boundedBy_zero {α : Type u_1} : MeasureTheory.OuterMeasure.boundedBy 0 = 0

theorem MeasureTheory.OuterMeasure.smul_boundedBy {α : Type u_1} {m : Set α → ENNReal} {c : ENNReal} (hc : c ≠ ⊤) : c • MeasureTheory.OuterMeasure.boundedBy m = MeasureTheory.OuterMeasure.boundedBy (c • m)

theorem MeasureTheory.OuterMeasure.comap_boundedBy {α : Type u_1} {m : Set α → ENNReal} {β : Type u_2} (f : β → α) (h : (Monotone fun (s : { s : Set α // Set.Nonempty s }) => m ↑s) ∨ Function.Surjective f) : (MeasureTheory.OuterMeasure.comap f) (MeasureTheory.OuterMeasure.boundedBy m) = MeasureTheory.OuterMeasure.boundedBy fun (s : Set β) => m (f '' s)

theorem MeasureTheory.OuterMeasure.boundedBy_union_of_top_of_nonempty_inter {α : Type u_1} {m : Set α → ENNReal} {s : Set α} {t : Set α} (h : ∀ (u : Set α), Set.Nonempty (s ∩ u) → Set.Nonempty (t ∩ u) → m u = ⊤) : ↑(MeasureTheory.OuterMeasure.boundedBy m) (s ∪ t) = ↑(MeasureTheory.OuterMeasure.boundedBy m) s + ↑(MeasureTheory.OuterMeasure.boundedBy m) t

If m u = ∞ for any set u that has nonempty intersection both with s and t, then μ (s ∪ t) = μ s + μ t, where μ = MeasureTheory.OuterMeasure.boundedBy m.

E.g., if α is an (e)metric space and m u = ∞ on any set of diameter ≥ r, then this lemma implies that μ (s ∪ t) = μ s + μ t on any two sets such that r ≤ edist x y for all x ∈ s and y ∈ t.

def MeasureTheory.OuterMeasure.IsCaratheodory {α : Type u} (m : MeasureTheory.OuterMeasure α) (s : Set α) : Prop

A set s is Carathéodory-measurable for an outer measure m if for all sets t we have m t = m (t ∩ s) + m (t \ s).

Equations

• MeasureTheory.OuterMeasure.IsCaratheodory m s = ∀ (t : Set α), ↑m t = ↑m (t ∩ s) + ↑m (t \ s)

theorem MeasureTheory.OuterMeasure.isCaratheodory_iff_le' {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : Set α} : MeasureTheory.OuterMeasure.IsCaratheodory m s ↔ ∀ (t : Set α), ↑m (t ∩ s) + ↑m (t \ s) ≤ ↑m t

@[simp]

theorem MeasureTheory.OuterMeasure.isCaratheodory_empty {α : Type u} (m : MeasureTheory.OuterMeasure α) : MeasureTheory.OuterMeasure.IsCaratheodory m ∅

theorem MeasureTheory.OuterMeasure.isCaratheodory_compl {α : Type u} (m : MeasureTheory.OuterMeasure α) {s₁ : Set α} : MeasureTheory.OuterMeasure.IsCaratheodory m s₁ → MeasureTheory.OuterMeasure.IsCaratheodory m s₁ᶜ

@[simp]

theorem MeasureTheory.OuterMeasure.isCaratheodory_compl_iff {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : Set α} : MeasureTheory.OuterMeasure.IsCaratheodory m sᶜ ↔ MeasureTheory.OuterMeasure.IsCaratheodory m s

theorem MeasureTheory.OuterMeasure.isCaratheodory_union {α : Type u} (m : MeasureTheory.OuterMeasure α) {s₁ : Set α} {s₂ : Set α} (h₁ : MeasureTheory.OuterMeasure.IsCaratheodory m s₁) (h₂ : MeasureTheory.OuterMeasure.IsCaratheodory m s₂) : MeasureTheory.OuterMeasure.IsCaratheodory m (s₁ ∪ s₂)

theorem MeasureTheory.OuterMeasure.measure_inter_union {α : Type u} (m : MeasureTheory.OuterMeasure α) {s₁ : Set α} {s₂ : Set α} (h : s₁ ∩ s₂ ⊆ ∅) (h₁ : MeasureTheory.OuterMeasure.IsCaratheodory m s₁) {t : Set α} : ↑m (t ∩ (s₁ ∪ s₂)) = ↑m (t ∩ s₁) + ↑m (t ∩ s₂)

theorem MeasureTheory.OuterMeasure.isCaratheodory_iUnion_lt {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : ℕ → Set α} {n : ℕ} : (∀ i < n, MeasureTheory.OuterMeasure.IsCaratheodory m (s i)) → MeasureTheory.OuterMeasure.IsCaratheodory m (⋃ (i : ℕ), ⋃ (_ : i < n), s i)

theorem MeasureTheory.OuterMeasure.isCaratheodory_inter {α : Type u} (m : MeasureTheory.OuterMeasure α) {s₁ : Set α} {s₂ : Set α} (h₁ : MeasureTheory.OuterMeasure.IsCaratheodory m s₁) (h₂ : MeasureTheory.OuterMeasure.IsCaratheodory m s₂) : MeasureTheory.OuterMeasure.IsCaratheodory m (s₁ ∩ s₂)

theorem MeasureTheory.OuterMeasure.isCaratheodory_sum {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : ℕ → Set α} (h : ∀ (i : ℕ), MeasureTheory.OuterMeasure.IsCaratheodory m (s i)) (hd : Pairwise (Disjoint on s)) {t : Set α} {n : ℕ} : (Finset.sum (Finset.range n) fun (i : ℕ) => ↑m (t ∩ s i)) = ↑m (t ∩ ⋃ (i : ℕ), ⋃ (_ : i < n), s i)

theorem MeasureTheory.OuterMeasure.isCaratheodory_iUnion_nat {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : ℕ → Set α} (h : ∀ (i : ℕ), MeasureTheory.OuterMeasure.IsCaratheodory m (s i)) (hd : Pairwise (Disjoint on s)) : MeasureTheory.OuterMeasure.IsCaratheodory m (⋃ (i : ℕ), s i)

theorem MeasureTheory.OuterMeasure.f_iUnion {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : ℕ → Set α} (h : ∀ (i : ℕ), MeasureTheory.OuterMeasure.IsCaratheodory m (s i)) (hd : Pairwise (Disjoint on s)) : ↑m (⋃ (i : ℕ), s i) = ∑' (i : ℕ), ↑m (s i)

def MeasureTheory.OuterMeasure.caratheodoryDynkin {α : Type u} (m : MeasureTheory.OuterMeasure α) : MeasurableSpace.DynkinSystem α

The Carathéodory-measurable sets for an outer measure m form a Dynkin system.

Equations

• MeasureTheory.OuterMeasure.caratheodoryDynkin m = { Has := MeasureTheory.OuterMeasure.IsCaratheodory m, has_empty := ⋯, has_compl := ⋯, has_iUnion_nat := ⋯ }

def MeasureTheory.OuterMeasure.caratheodory {α : Type u} (m : MeasureTheory.OuterMeasure α) : MeasurableSpace α

Given an outer measure μ, the Carathéodory-measurable space is defined such that s is measurable if ∀t, μ t = μ (t ∩ s) + μ (t \ s).

Equations

• MeasureTheory.OuterMeasure.caratheodory m = MeasurableSpace.DynkinSystem.toMeasurableSpace (MeasureTheory.OuterMeasure.caratheodoryDynkin m) ⋯

theorem MeasureTheory.OuterMeasure.isCaratheodory_iff {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : Set α} : MeasurableSet s ↔ ∀ (t : Set α), ↑m t = ↑m (t ∩ s) + ↑m (t \ s)

theorem MeasureTheory.OuterMeasure.isCaratheodory_iff_le {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : Set α} : MeasurableSet s ↔ ∀ (t : Set α), ↑m (t ∩ s) + ↑m (t \ s) ≤ ↑m t

theorem MeasureTheory.OuterMeasure.iUnion_eq_of_caratheodory {α : Type u} (m : MeasureTheory.OuterMeasure α) {s : ℕ → Set α} (h : ∀ (i : ℕ), MeasurableSet (s i)) (hd : Pairwise (Disjoint on s)) : ↑m (⋃ (i : ℕ), s i) = ∑' (i : ℕ), ↑m (s i)

theorem MeasureTheory.OuterMeasure.ofFunction_caratheodory {α : Type u_1} {m : Set α → ENNReal} {s : Set α} {h₀ : m ∅ = 0} (hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t) : MeasurableSet s

theorem MeasureTheory.OuterMeasure.boundedBy_caratheodory {α : Type u_1} {m : Set α → ENNReal} {s : Set α} (hs : ∀ (t : Set α), m (t ∩ s) + m (t \ s) ≤ m t) : MeasurableSet s

@[simp]

theorem MeasureTheory.OuterMeasure.zero_caratheodory {α : Type u_1} : MeasureTheory.OuterMeasure.caratheodory 0 = ⊤

theorem MeasureTheory.OuterMeasure.top_caratheodory {α : Type u_1} : MeasureTheory.OuterMeasure.caratheodory ⊤ = ⊤

theorem MeasureTheory.OuterMeasure.le_add_caratheodory {α : Type u_1} (m₁ : MeasureTheory.OuterMeasure α) (m₂ : MeasureTheory.OuterMeasure α) : MeasureTheory.OuterMeasure.caratheodory m₁ ⊓ MeasureTheory.OuterMeasure.caratheodory m₂ ≤ MeasureTheory.OuterMeasure.caratheodory (m₁ + m₂)

theorem MeasureTheory.OuterMeasure.le_sum_caratheodory {α : Type u_1} {ι : Type u_2} (m : ι → MeasureTheory.OuterMeasure α) : ⨅ (i : ι), MeasureTheory.OuterMeasure.caratheodory (m i) ≤ MeasureTheory.OuterMeasure.caratheodory (MeasureTheory.OuterMeasure.sum m)

theorem MeasureTheory.OuterMeasure.le_smul_caratheodory {α : Type u_1} (a : ENNReal) (m : MeasureTheory.OuterMeasure α) : MeasureTheory.OuterMeasure.caratheodory m ≤ MeasureTheory.OuterMeasure.caratheodory (a • m)

@[simp]

theorem MeasureTheory.OuterMeasure.dirac_caratheodory {α : Type u_1} (a : α) : MeasureTheory.OuterMeasure.caratheodory (MeasureTheory.OuterMeasure.dirac a) = ⊤

def MeasureTheory.OuterMeasure.sInfGen {α : Type u_1} (m : Set (MeasureTheory.OuterMeasure α)) (s : Set α) : ENNReal

Given a set of outer measures, we define a new function that on a set s is defined to be the infimum of μ(s) for the outer measures μ in the collection. We ensure that this function is defined to be 0 on ∅, even if the collection of outer measures is empty. The outer measure generated by this function is the infimum of the given outer measures.

Equations

• MeasureTheory.OuterMeasure.sInfGen m s = ⨅ μ ∈ m, ↑μ s

theorem MeasureTheory.OuterMeasure.sInfGen_def {α : Type u_1} (m : Set (MeasureTheory.OuterMeasure α)) (t : Set α) : MeasureTheory.OuterMeasure.sInfGen m t = ⨅ μ ∈ m, ↑μ t

theorem MeasureTheory.OuterMeasure.sInf_eq_boundedBy_sInfGen {α : Type u_1} (m : Set (MeasureTheory.OuterMeasure α)) : sInf m = MeasureTheory.OuterMeasure.boundedBy (MeasureTheory.OuterMeasure.sInfGen m)

theorem MeasureTheory.OuterMeasure.iSup_sInfGen_nonempty {α : Type u_1} {m : Set (MeasureTheory.OuterMeasure α)} (h : Set.Nonempty m) (t : Set α) : ⨆ (_ : Set.Nonempty t), MeasureTheory.OuterMeasure.sInfGen m t = ⨅ μ ∈ m, ↑μ t

theorem MeasureTheory.OuterMeasure.sInf_apply {α : Type u_1} {m : Set (MeasureTheory.OuterMeasure α)} {s : Set α} (h : Set.Nonempty m) : ↑(sInf m) s = ⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ μ ∈ m, ↑μ (t n)

The value of the Infimum of a nonempty set of outer measures on a set is not simply the minimum value of a measure on that set: it is the infimum sum of measures of countable set of sets that covers that set, where a different measure can be used for each set in the cover.

theorem MeasureTheory.OuterMeasure.sInf_apply' {α : Type u_1} {m : Set (MeasureTheory.OuterMeasure α)} {s : Set α} (h : Set.Nonempty s) : ↑(sInf m) s = ⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ μ ∈ m, ↑μ (t n)

The value of the Infimum of a set of outer measures on a nonempty set is not simply the minimum value of a measure on that set: it is the infimum sum of measures of countable set of sets that covers that set, where a different measure can be used for each set in the cover.

theorem MeasureTheory.OuterMeasure.iInf_apply {α : Type u_1} {ι : Sort u_2} [Nonempty ι] (m : ι → MeasureTheory.OuterMeasure α) (s : Set α) : ↑(⨅ (i : ι), m i) s = ⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ (i : ι), ↑(m i) (t n)

The value of the Infimum of a nonempty family of outer measures on a set is not simply the minimum value of a measure on that set: it is the infimum sum of measures of countable set of sets that covers that set, where a different measure can be used for each set in the cover.

theorem MeasureTheory.OuterMeasure.iInf_apply' {α : Type u_1} {ι : Sort u_2} (m : ι → MeasureTheory.OuterMeasure α) {s : Set α} (hs : Set.Nonempty s) : ↑(⨅ (i : ι), m i) s = ⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ (i : ι), ↑(m i) (t n)

The value of the Infimum of a family of outer measures on a nonempty set is not simply the minimum value of a measure on that set: it is the infimum sum of measures of countable set of sets that covers that set, where a different measure can be used for each set in the cover.

theorem MeasureTheory.OuterMeasure.biInf_apply {α : Type u_1} {ι : Type u_2} {I : Set ι} (hI : Set.Nonempty I) (m : ι → MeasureTheory.OuterMeasure α) (s : Set α) : ↑(⨅ i ∈ I, m i) s = ⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ i ∈ I, ↑(m i) (t n)

The value of the Infimum of a nonempty family of outer measures on a set is not simply the minimum value of a measure on that set: it is the infimum sum of measures of countable set of sets that covers that set, where a different measure can be used for each set in the cover.

theorem MeasureTheory.OuterMeasure.biInf_apply' {α : Type u_1} {ι : Type u_2} (I : Set ι) (m : ι → MeasureTheory.OuterMeasure α) {s : Set α} (hs : Set.Nonempty s) : ↑(⨅ i ∈ I, m i) s = ⨅ (t : ℕ → Set α), ⨅ (_ : s ⊆ Set.iUnion t), ∑' (n : ℕ), ⨅ i ∈ I, ↑(m i) (t n)

The value of the Infimum of a nonempty family of outer measures on a set is not simply the minimum value of a measure on that set: it is the infimum sum of measures of countable set of sets that covers that set, where a different measure can be used for each set in the cover.

theorem MeasureTheory.OuterMeasure.map_iInf_le {α : Type u_1} {ι : Sort u_2} {β : Type u_3} (f : α → β) (m : ι → MeasureTheory.OuterMeasure α) : (MeasureTheory.OuterMeasure.map f) (⨅ (i : ι), m i) ≤ ⨅ (i : ι), (MeasureTheory.OuterMeasure.map f) (m i)

theorem MeasureTheory.OuterMeasure.comap_iInf {α : Type u_1} {ι : Sort u_2} {β : Type u_3} (f : α → β) (m : ι → MeasureTheory.OuterMeasure β) : (MeasureTheory.OuterMeasure.comap f) (⨅ (i : ι), m i) = ⨅ (i : ι), (MeasureTheory.OuterMeasure.comap f) (m i)

theorem MeasureTheory.OuterMeasure.map_iInf {α : Type u_1} {ι : Sort u_2} {β : Type u_3} {f : α → β} (hf : Function.Injective f) (m : ι → MeasureTheory.OuterMeasure α) : (MeasureTheory.OuterMeasure.map f) (⨅ (i : ι), m i) = (MeasureTheory.OuterMeasure.restrict (Set.range f)) (⨅ (i : ι), (MeasureTheory.OuterMeasure.map f) (m i))

theorem MeasureTheory.OuterMeasure.map_iInf_comap {α : Type u_1} {ι : Sort u_2} {β : Type u_3} [Nonempty ι] {f : α → β} (m : ι → MeasureTheory.OuterMeasure β) : (MeasureTheory.OuterMeasure.map f) (⨅ (i : ι), (MeasureTheory.OuterMeasure.comap f) (m i)) = ⨅ (i : ι), (MeasureTheory.OuterMeasure.map f) ((MeasureTheory.OuterMeasure.comap f) (m i))

theorem MeasureTheory.OuterMeasure.map_biInf_comap {α : Type u_1} {ι : Type u_2} {β : Type u_3} {I : Set ι} (hI : Set.Nonempty I) {f : α → β} (m : ι → MeasureTheory.OuterMeasure β) : (MeasureTheory.OuterMeasure.map f) (⨅ i ∈ I, (MeasureTheory.OuterMeasure.comap f) (m i)) = ⨅ i ∈ I, (MeasureTheory.OuterMeasure.map f) ((MeasureTheory.OuterMeasure.comap f) (m i))

theorem MeasureTheory.OuterMeasure.restrict_iInf_restrict {α : Type u_1} {ι : Sort u_2} (s : Set α) (m : ι → MeasureTheory.OuterMeasure α) : (MeasureTheory.OuterMeasure.restrict s) (⨅ (i : ι), (MeasureTheory.OuterMeasure.restrict s) (m i)) = (MeasureTheory.OuterMeasure.restrict s) (⨅ (i : ι), m i)

theorem MeasureTheory.OuterMeasure.restrict_iInf {α : Type u_1} {ι : Sort u_2} [Nonempty ι] (s : Set α) (m : ι → MeasureTheory.OuterMeasure α) : (MeasureTheory.OuterMeasure.restrict s) (⨅ (i : ι), m i) = ⨅ (i : ι), (MeasureTheory.OuterMeasure.restrict s) (m i)

theorem MeasureTheory.OuterMeasure.restrict_biInf {α : Type u_1} {ι : Type u_2} {I : Set ι} (hI : Set.Nonempty I) (s : Set α) (m : ι → MeasureTheory.OuterMeasure α) : (MeasureTheory.OuterMeasure.restrict s) (⨅ i ∈ I, m i) = ⨅ i ∈ I, (MeasureTheory.OuterMeasure.restrict s) (m i)

theorem MeasureTheory.OuterMeasure.restrict_sInf_eq_sInf_restrict {α : Type u_1} (m : Set (MeasureTheory.OuterMeasure α)) {s : Set α} (hm : Set.Nonempty m) : (MeasureTheory.OuterMeasure.restrict s) (sInf m) = sInf (⇑(MeasureTheory.OuterMeasure.restrict s) '' m)

This proves that Inf and restrict commute for outer measures, so long as the set of outer measures is nonempty.

Induced Outer Measure

We can extend a function defined on a subset of Set α to an outer measure. The underlying function is called extend, and the measure it induces is called inducedOuterMeasure.

Some lemmas below are proven twice, once in the general case, and one where the function m is only defined on measurable sets (i.e. when P = MeasurableSet). In the latter cases, we can remove some hypotheses in the statement. The general version has the same name, but with a prime at the end.

def MeasureTheory.extend {α : Type u_1} {P : α → Prop} (m : (s : α) → P s → ENNReal) (s : α) : ENNReal

We can trivially extend a function defined on a subclass of objects (with codomain ℝ≥0∞) to all objects by defining it to be ∞ on the objects not in the class.

Equations

• MeasureTheory.extend m s = ⨅ (h : P s), m s h

theorem MeasureTheory.extend_eq {α : Type u_1} {P : α → Prop} (m : (s : α) → P s → ENNReal) {s : α} (h : P s) : MeasureTheory.extend m s = m s h

theorem MeasureTheory.extend_eq_top {α : Type u_1} {P : α → Prop} (m : (s : α) → P s → ENNReal) {s : α} (h : ¬P s) : MeasureTheory.extend m s = ⊤

theorem MeasureTheory.smul_extend {α : Type u_1} {P : α → Prop} (m : (s : α) → P s → ENNReal) {R : Type u_2} [Zero R] [SMulWithZero R ENNReal] [IsScalarTower R ENNReal ENNReal] [NoZeroSMulDivisors R ENNReal] {c : R} (hc : c ≠ 0) : c • MeasureTheory.extend m = MeasureTheory.extend fun (s : α) (h : P s) => c • m s h

theorem MeasureTheory.le_extend {α : Type u_1} {P : α → Prop} (m : (s : α) → P s → ENNReal) {s : α} (h : P s) : m s h ≤ MeasureTheory.extend m s

theorem MeasureTheory.extend_congr {α : Type u_1} {P : α → Prop} (m : (s : α) → P s → ENNReal) {β : Type u_2} {Pb : β → Prop} {mb : (s : β) → Pb s → ENNReal} {sa : α} {sb : β} (hP : P sa ↔ Pb sb) (hm : ∀ (ha : P sa) (hb : Pb sb), m sa ha = mb sb hb) : MeasureTheory.extend m sa = MeasureTheory.extend mb sb

@[simp]

theorem MeasureTheory.extend_top {α : Type u_2} {P : α → Prop} : (MeasureTheory.extend fun (x : α) (x : P x) => ⊤) = ⊤

theorem MeasureTheory.extend_empty {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} (P0 : P ∅) (m0 : m ∅ P0 = 0) : MeasureTheory.extend m ∅ = 0

theorem MeasureTheory.extend_iUnion_nat {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) {f : ℕ → Set α} (hm : ∀ (i : ℕ), P (f i)) (mU : m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) : MeasureTheory.extend m (⋃ (i : ℕ), f i) = ∑' (i : ℕ), MeasureTheory.extend m (f i)

theorem MeasureTheory.extend_iUnion_le_tsum_nat' {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) (s : ℕ → Set α) : MeasureTheory.extend m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), MeasureTheory.extend m (s i)

theorem MeasureTheory.extend_mono' {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} (m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) ⦃s₁ : Set α⦄ ⦃s₂ : Set α⦄ (h₁ : P s₁) (hs : s₁ ⊆ s₂) : MeasureTheory.extend m s₁ ≤ MeasureTheory.extend m s₂

theorem MeasureTheory.extend_iUnion {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} (P0 : P ∅) (m0 : m ∅ P0 = 0) (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) {β : Type u_2} [Countable β] {f : β → Set α} (hd : Pairwise (Disjoint on f)) (hm : ∀ (i : β), P (f i)) : MeasureTheory.extend m (⋃ (i : β), f i) = ∑' (i : β), MeasureTheory.extend m (f i)

theorem MeasureTheory.extend_union {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} (P0 : P ∅) (m0 : m ∅ P0 = 0) (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) {s₁ : Set α} {s₂ : Set α} (hd : Disjoint s₁ s₂) (h₁ : P s₁) (h₂ : P s₂) : MeasureTheory.extend m (s₁ ∪ s₂) = MeasureTheory.extend m s₁ + MeasureTheory.extend m s₂

def MeasureTheory.inducedOuterMeasure {α : Type u_1} {P : Set α → Prop} (m : (s : Set α) → P s → ENNReal) (P0 : P ∅) (m0 : m ∅ P0 = 0) : MeasureTheory.OuterMeasure α

Given an arbitrary function on a subset of sets, we can define the outer measure corresponding to it (this is the unique maximal outer measure that is at most m on the domain of m).

Equations

• MeasureTheory.inducedOuterMeasure m P0 m0 = MeasureTheory.OuterMeasure.ofFunction (MeasureTheory.extend m) ⋯

theorem MeasureTheory.le_inducedOuterMeasure {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0} {μ : MeasureTheory.OuterMeasure α} : μ ≤ MeasureTheory.inducedOuterMeasure m P0 m0 ↔ ∀ (s : Set α) (hs : P s), ↑μ s ≤ m s hs

theorem MeasureTheory.inducedOuterMeasure_union_of_false_of_nonempty_inter {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0} {s : Set α} {t : Set α} (h : ∀ (u : Set α), Set.Nonempty (s ∩ u) → Set.Nonempty (t ∩ u) → ¬P u) : ↑(MeasureTheory.inducedOuterMeasure m P0 m0) (s ∪ t) = ↑(MeasureTheory.inducedOuterMeasure m P0 m0) s + ↑(MeasureTheory.inducedOuterMeasure m P0 m0) t

If P u is False for any set u that has nonempty intersection both with s and t, then μ (s ∪ t) = μ s + μ t, where μ = inducedOuterMeasure m P0 m0.

E.g., if α is an (e)metric space and P u = diam u < r, then this lemma implies that μ (s ∪ t) = μ s + μ t on any two sets such that r ≤ edist x y for all x ∈ s and y ∈ t.

theorem MeasureTheory.inducedOuterMeasure_eq_extend' {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0} (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) (m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) {s : Set α} (hs : P s) : ↑(MeasureTheory.inducedOuterMeasure m P0 m0) s = MeasureTheory.extend m s

theorem MeasureTheory.inducedOuterMeasure_eq' {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0} (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) (m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) {s : Set α} (hs : P s) : ↑(MeasureTheory.inducedOuterMeasure m P0 m0) s = m s hs

theorem MeasureTheory.inducedOuterMeasure_eq_iInf {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0} (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) (m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) (s : Set α) : ↑(MeasureTheory.inducedOuterMeasure m P0 m0) s = ⨅ (t : Set α), ⨅ (ht : P t), ⨅ (_ : s ⊆ t), m t ht

theorem MeasureTheory.inducedOuterMeasure_preimage {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0} (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) (m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) (f : α ≃ α) (Pm : ∀ (s : Set α), P (⇑f ⁻¹' s) ↔ P s) (mm : ∀ (s : Set α) (hs : P s), m (⇑f ⁻¹' s) ⋯ = m s hs) {A : Set α} : ↑(MeasureTheory.inducedOuterMeasure m P0 m0) (⇑f ⁻¹' A) = ↑(MeasureTheory.inducedOuterMeasure m P0 m0) A

theorem MeasureTheory.inducedOuterMeasure_exists_set {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0} (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) (m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) {s : Set α} (hs : ↑(MeasureTheory.inducedOuterMeasure m P0 m0) s ≠ ⊤) {ε : ENNReal} (hε : ε ≠ 0) : ∃ (t : Set α), P t ∧ s ⊆ t ∧ ↑(MeasureTheory.inducedOuterMeasure m P0 m0) t ≤ ↑(MeasureTheory.inducedOuterMeasure m P0 m0) s + ε

theorem MeasureTheory.inducedOuterMeasure_caratheodory {α : Type u_1} {P : Set α → Prop} {m : (s : Set α) → P s → ENNReal} {P0 : P ∅} {m0 : m ∅ P0 = 0} (PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ (i : ℕ), f i)) (msU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), P (f i)), m (⋃ (i : ℕ), f i) ⋯ ≤ ∑' (i : ℕ), m (f i) ⋯) (m_mono : ∀ ⦃s₁ s₂ : Set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂) (s : Set α) : MeasurableSet s ↔ ∀ (t : Set α), P t → ↑(MeasureTheory.inducedOuterMeasure m P0 m0) (t ∩ s) + ↑(MeasureTheory.inducedOuterMeasure m P0 m0) (t \ s) ≤ ↑(MeasureTheory.inducedOuterMeasure m P0 m0) t

To test whether s is Carathéodory-measurable we only need to check the sets t for which P t holds. See ofFunction_caratheodory for another way to show the Carathéodory-measurability of s.

If P is MeasurableSet for some measurable space, then we can remove some hypotheses of the above lemmas.

theorem MeasureTheory.extend_mono {α : Type u_1} [MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal} (m0 : m ∅ ⋯ = 0) (mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) {s₁ : Set α} {s₂ : Set α} (h₁ : MeasurableSet s₁) (hs : s₁ ⊆ s₂) : MeasureTheory.extend m s₁ ≤ MeasureTheory.extend m s₂

theorem MeasureTheory.extend_iUnion_le_tsum_nat {α : Type u_1} [MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal} (m0 : m ∅ ⋯ = 0) (mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) (s : ℕ → Set α) : MeasureTheory.extend m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), MeasureTheory.extend m (s i)

theorem MeasureTheory.inducedOuterMeasure_eq_extend {α : Type u_1} [MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal} (m0 : m ∅ ⋯ = 0) (mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) {s : Set α} (hs : MeasurableSet s) : ↑(MeasureTheory.inducedOuterMeasure m ⋯ m0) s = MeasureTheory.extend m s

theorem MeasureTheory.inducedOuterMeasure_eq {α : Type u_1} [MeasurableSpace α] {m : (s : Set α) → MeasurableSet s → ENNReal} (m0 : m ∅ ⋯ = 0) (mU : ∀ ⦃f : ℕ → Set α⦄ (hm : ∀ (i : ℕ), MeasurableSet (f i)), Pairwise (Disjoint on f) → m (⋃ (i : ℕ), f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯) {s : Set α} (hs : MeasurableSet s) : ↑(MeasureTheory.inducedOuterMeasure m ⋯ m0) s = m s hs

def MeasureTheory.OuterMeasure.trim {α : Type u_1} [MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) : MeasureTheory.OuterMeasure α

Given an outer measure m we can forget its value on non-measurable sets, and then consider m.trim, the unique maximal outer measure less than that function.

Equations

• MeasureTheory.OuterMeasure.trim m = MeasureTheory.inducedOuterMeasure (fun (s : Set α) (x : MeasurableSet s) => ↑m s) ⋯ ⋯

theorem MeasureTheory.OuterMeasure.le_trim {α : Type u_1} [MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) : m ≤ MeasureTheory.OuterMeasure.trim m

@[simp]

theorem MeasureTheory.OuterMeasure.trim_eq {α : Type u_1} [MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) {s : Set α} (hs : MeasurableSet s) : ↑(MeasureTheory.OuterMeasure.trim m) s = ↑m s

theorem MeasureTheory.OuterMeasure.trim_congr {α : Type u_1} [MeasurableSpace α] {m₁ : MeasureTheory.OuterMeasure α} {m₂ : MeasureTheory.OuterMeasure α} (H : ∀ {s : Set α}, MeasurableSet s → ↑m₁ s = ↑m₂ s) : MeasureTheory.OuterMeasure.trim m₁ = MeasureTheory.OuterMeasure.trim m₂

theorem MeasureTheory.OuterMeasure.trim_mono {α : Type u_1} [MeasurableSpace α] : Monotone MeasureTheory.OuterMeasure.trim

theorem MeasureTheory.OuterMeasure.le_trim_iff {α : Type u_1} [MeasurableSpace α] {m₁ : MeasureTheory.OuterMeasure α} {m₂ : MeasureTheory.OuterMeasure α} : m₁ ≤ MeasureTheory.OuterMeasure.trim m₂ ↔ ∀ (s : Set α), MeasurableSet s → ↑m₁ s ≤ ↑m₂ s

theorem MeasureTheory.OuterMeasure.trim_le_trim_iff {α : Type u_1} [MeasurableSpace α] {m₁ : MeasureTheory.OuterMeasure α} {m₂ : MeasureTheory.OuterMeasure α} : MeasureTheory.OuterMeasure.trim m₁ ≤ MeasureTheory.OuterMeasure.trim m₂ ↔ ∀ (s : Set α), MeasurableSet s → ↑m₁ s ≤ ↑m₂ s

theorem MeasureTheory.OuterMeasure.trim_eq_trim_iff {α : Type u_1} [MeasurableSpace α] {m₁ : MeasureTheory.OuterMeasure α} {m₂ : MeasureTheory.OuterMeasure α} : MeasureTheory.OuterMeasure.trim m₁ = MeasureTheory.OuterMeasure.trim m₂ ↔ ∀ (s : Set α), MeasurableSet s → ↑m₁ s = ↑m₂ s

theorem MeasureTheory.OuterMeasure.trim_eq_iInf {α : Type u_1} [MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) (s : Set α) : ↑(MeasureTheory.OuterMeasure.trim m) s = ⨅ (t : Set α), ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), ↑m t

theorem MeasureTheory.OuterMeasure.trim_eq_iInf' {α : Type u_1} [MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) (s : Set α) : ↑(MeasureTheory.OuterMeasure.trim m) s = ⨅ (t : { t : Set α // s ⊆ t ∧ MeasurableSet t }), ↑m ↑t

theorem MeasureTheory.OuterMeasure.trim_trim {α : Type u_1} [MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) : MeasureTheory.OuterMeasure.trim (MeasureTheory.OuterMeasure.trim m) = MeasureTheory.OuterMeasure.trim m

@[simp]

theorem MeasureTheory.OuterMeasure.trim_top {α : Type u_1} [MeasurableSpace α] : MeasureTheory.OuterMeasure.trim ⊤ = ⊤

@[simp]

theorem MeasureTheory.OuterMeasure.trim_zero {α : Type u_1} [MeasurableSpace α] : MeasureTheory.OuterMeasure.trim 0 = 0

theorem MeasureTheory.OuterMeasure.trim_sum_ge {α : Type u_1} [MeasurableSpace α] {ι : Type u_2} (m : ι → MeasureTheory.OuterMeasure α) : (MeasureTheory.OuterMeasure.sum fun (i : ι) => MeasureTheory.OuterMeasure.trim (m i)) ≤ MeasureTheory.OuterMeasure.trim (MeasureTheory.OuterMeasure.sum m)

theorem MeasureTheory.OuterMeasure.exists_measurable_superset_eq_trim {α : Type u_1} [MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) (s : Set α) : ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ ↑m t = ↑(MeasureTheory.OuterMeasure.trim m) s

theorem MeasureTheory.OuterMeasure.exists_measurable_superset_of_trim_eq_zero {α : Type u_1} [MeasurableSpace α] {m : MeasureTheory.OuterMeasure α} {s : Set α} (h : ↑(MeasureTheory.OuterMeasure.trim m) s = 0) : ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ ↑m t = 0

theorem MeasureTheory.OuterMeasure.exists_measurable_superset_forall_eq_trim {α : Type u_1} [MeasurableSpace α] {ι : Sort u_2} [Countable ι] (μ : ι → MeasureTheory.OuterMeasure α) (s : Set α) : ∃ (t : Set α), s ⊆ t ∧ MeasurableSet t ∧ ∀ (i : ι), ↑(μ i) t = ↑(MeasureTheory.OuterMeasure.trim (μ i)) s

If μ i is a countable family of outer measures, then for every set s there exists a measurable set t ⊇ s such that μ i t = (μ i).trim s for all i.

theorem MeasureTheory.OuterMeasure.trim_binop {α : Type u_1} [MeasurableSpace α] {m₁ : MeasureTheory.OuterMeasure α} {m₂ : MeasureTheory.OuterMeasure α} {m₃ : MeasureTheory.OuterMeasure α} {op : ENNReal → ENNReal → ENNReal} (h : ∀ (s : Set α), ↑m₁ s = op (↑m₂ s) (↑m₃ s)) (s : Set α) : ↑(MeasureTheory.OuterMeasure.trim m₁) s = op (↑(MeasureTheory.OuterMeasure.trim m₂) s) (↑(MeasureTheory.OuterMeasure.trim m₃) s)

If m₁ s = op (m₂ s) (m₃ s) for all s, then the same is true for m₁.trim, m₂.trim, and m₃ s.

theorem MeasureTheory.OuterMeasure.trim_op {α : Type u_1} [MeasurableSpace α] {m₁ : MeasureTheory.OuterMeasure α} {m₂ : MeasureTheory.OuterMeasure α} {op : ENNReal → ENNReal} (h : ∀ (s : Set α), ↑m₁ s = op (↑m₂ s)) (s : Set α) : ↑(MeasureTheory.OuterMeasure.trim m₁) s = op (↑(MeasureTheory.OuterMeasure.trim m₂) s)

If m₁ s = op (m₂ s) for all s, then the same is true for m₁.trim and m₂.trim.

theorem MeasureTheory.OuterMeasure.trim_add {α : Type u_1} [MeasurableSpace α] (m₁ : MeasureTheory.OuterMeasure α) (m₂ : MeasureTheory.OuterMeasure α) : MeasureTheory.OuterMeasure.trim (m₁ + m₂) = MeasureTheory.OuterMeasure.trim m₁ + MeasureTheory.OuterMeasure.trim m₂

trim is additive.

theorem MeasureTheory.OuterMeasure.trim_smul {α : Type u_1} [MeasurableSpace α] {R : Type u_2} [SMul R ENNReal] [IsScalarTower R ENNReal ENNReal] (c : R) (m : MeasureTheory.OuterMeasure α) : MeasureTheory.OuterMeasure.trim (c • m) = c • MeasureTheory.OuterMeasure.trim m

trim respects scalar multiplication.

theorem MeasureTheory.OuterMeasure.trim_sup {α : Type u_1} [MeasurableSpace α] (m₁ : MeasureTheory.OuterMeasure α) (m₂ : MeasureTheory.OuterMeasure α) : MeasureTheory.OuterMeasure.trim (m₁ ⊔ m₂) = MeasureTheory.OuterMeasure.trim m₁ ⊔ MeasureTheory.OuterMeasure.trim m₂

trim sends the supremum of two outer measures to the supremum of the trimmed measures.

theorem MeasureTheory.OuterMeasure.trim_iSup {α : Type u_1} [MeasurableSpace α] {ι : Sort u_2} [Countable ι] (μ : ι → MeasureTheory.OuterMeasure α) : MeasureTheory.OuterMeasure.trim (⨆ (i : ι), μ i) = ⨆ (i : ι), MeasureTheory.OuterMeasure.trim (μ i)

trim sends the supremum of a countable family of outer measures to the supremum of the trimmed measures.

theorem MeasureTheory.OuterMeasure.restrict_trim {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.OuterMeasure α} {s : Set α} (hs : MeasurableSet s) : MeasureTheory.OuterMeasure.trim ((MeasureTheory.OuterMeasure.restrict s) μ) = (MeasureTheory.OuterMeasure.restrict s) (MeasureTheory.OuterMeasure.trim μ)

The trimmed property of a measure μ states that μ.toOuterMeasure.trim = μ.toOuterMeasure. This theorem shows that a restricted trimmed outer measure is a trimmed outer measure.