mathlib documentation

measure_theory.outer_measure

Outer Measures

An outer measure is a function μ : set α → ennreal, 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 α → ennreal 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

References

Tags

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

structure measure_theory.outer_measure  :
Type u_1Type u_1

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

@[simp]

theorem measure_theory.outer_measure.mono' {α : Type u_1} (m : measure_theory.outer_measure α) {s₁ s₂ : set α} :
s₁ s₂m s₁ m s₂

theorem measure_theory.outer_measure.Union {α : Type u_1} (m : measure_theory.outer_measure α) {β : Type u_2} [encodable β] (s : β → set α) :
m (⋃ (i : β), s i) ∑' (i : β), m (s i)

theorem measure_theory.outer_measure.Union_null {α : Type u_1} (m : measure_theory.outer_measure α) {β : Type u_2} [encodable β] {s : β → set α} :
(∀ (i : β), m (s i) = 0)m (⋃ (i : β), s i) = 0

theorem measure_theory.outer_measure.Union_finset {α : Type u_1} {β : Type u_2} (m : measure_theory.outer_measure α) (s : β → set α) (t : finset β) :
m (⋃ (i : β) (H : i t), s i) ∑ (i : β) in t, m (s i)

theorem measure_theory.outer_measure.union {α : Type u_1} (m : measure_theory.outer_measure α) (s₁ s₂ : set α) :
m (s₁ s₂) m s₁ + m s₂

theorem measure_theory.outer_measure.le_inter_add_diff {α : Type u_1} {m : measure_theory.outer_measure α} {t : set α} (s : set α) :
m t m (t s) + m (t \ s)

theorem measure_theory.outer_measure.diff_null {α : Type u_1} (m : measure_theory.outer_measure α) (s : set α) {t : set α} :
m t = 0m (s \ t) = m s

theorem measure_theory.outer_measure.union_null {α : Type u_1} (m : measure_theory.outer_measure α) {s₁ s₂ : set α} :
m s₁ = 0m s₂ = 0m (s₁ s₂) = 0

@[ext]
theorem measure_theory.outer_measure.ext {α : Type u_1} {μ₁ μ₂ : measure_theory.outer_measure α} :
(∀ (s : set α), μ₁ s = μ₂ s)μ₁ = μ₂

@[instance]

Equations
@[simp]
theorem measure_theory.outer_measure.coe_zero {α : Type u_1} :
0 = 0

@[instance]

Equations
@[simp]
theorem measure_theory.outer_measure.coe_add {α : Type u_1} (m₁ m₂ : measure_theory.outer_measure α) :
(m₁ + m₂) = m₁ + m₂

theorem measure_theory.outer_measure.add_apply {α : Type u_1} (m₁ m₂ : measure_theory.outer_measure α) (s : set α) :
(m₁ + m₂) s = m₁ s + m₂ s

@[simp]
theorem measure_theory.outer_measure.coe_smul {α : Type u_1} (c : ennreal) (m : measure_theory.outer_measure α) :
(c m) = c m

theorem measure_theory.outer_measure.smul_apply {α : Type u_1} (c : ennreal) (m : measure_theory.outer_measure α) (s : set α) :
(c m) s = c * m s

@[instance]

Equations
@[instance]

Equations
@[simp]
theorem measure_theory.outer_measure.Sup_apply {α : Type u_1} (ms : set (measure_theory.outer_measure α)) (s : set α) :
(Sup ms) s = ⨆ (m : measure_theory.outer_measure α) (H : m ms), m s

@[simp]
theorem measure_theory.outer_measure.supr_apply {α : Type u_1} {ι : Sort u_2} (f : ι → measure_theory.outer_measure α) (s : set α) :
(⨆ (i : ι), f i) s = ⨆ (i : ι), (f i) s

theorem measure_theory.outer_measure.coe_supr {α : Type u_1} {ι : Sort u_2} (f : ι → measure_theory.outer_measure α) :
(⨆ (i : ι), f i) = ⨆ (i : ι), (f i)

@[simp]
theorem measure_theory.outer_measure.sup_apply {α : Type u_1} (m₁ m₂ : measure_theory.outer_measure α) (s : set α) :
(m₁ m₂) s = m₁ s m₂ s

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

Equations
@[simp]
theorem measure_theory.outer_measure.map_apply {α : Type u_1} {β : Type u_2} (f : α → β) (m : measure_theory.outer_measure α) (s : set β) :

@[simp]
theorem measure_theory.outer_measure.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ) (m : measure_theory.outer_measure α) :

@[instance]

Equations

The dirac outer measure.

Equations
@[simp]
theorem measure_theory.outer_measure.dirac_apply {α : Type u_1} (a : α) (s : set α) :

def measure_theory.outer_measure.sum {α : Type u_1} {ι : Type u_2} :

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

Equations
@[simp]
theorem measure_theory.outer_measure.sum_apply {α : Type u_1} {ι : Type u_2} (f : ι → measure_theory.outer_measure α) (s : set α) :
(measure_theory.outer_measure.sum f) s = ∑' (i : ι), (f i) s

theorem measure_theory.outer_measure.smul_dirac_apply {α : Type u_1} (a : ennreal) (b : α) (s : set α) :

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

Equations
@[simp]
theorem measure_theory.outer_measure.comap_apply {α : Type u_1} {β : Type u_2} (f : α → β) (m : measure_theory.outer_measure β) (s : set α) :

theorem measure_theory.outer_measure.top_apply {α : Type u_1} {s : set α} :

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
theorem measure_theory.outer_measure.of_function_apply {α : Type u_1} (m : set αennreal) (m_empty : m = 0) (s : set α) :
(measure_theory.outer_measure.of_function m m_empty) s = ⨅ (t : set α) (h : s set.Union t), ∑' (n : ), m (t n)

theorem measure_theory.outer_measure.of_function_le {α : Type u_1} {m : set αennreal} {m_empty : m = 0} (s : set α) :

theorem measure_theory.outer_measure.of_function_eq {α : Type u_1} {m : set αennreal} {m_empty : m = 0} (s : set α) :
(∀ ⦃t : set α⦄, s tm s m t)(∀ (s : set α), m (⋃ (i : ), s i) ∑' (i : ), m (s i))(measure_theory.outer_measure.of_function m m_empty) s = m s

theorem measure_theory.outer_measure.le_of_function {α : Type u_1} {m : set αennreal} {m_empty : m = 0} {μ : measure_theory.outer_measure α} :
μ measure_theory.outer_measure.of_function m m_empty ∀ (s : set α), μ s m s

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
theorem measure_theory.outer_measure.is_caratheodory_iff_le' {α : Type u} (m : measure_theory.outer_measure α) {s : set α} :
m.is_caratheodory s ∀ (t : set α), m (t s) + m (t \ s) m t

theorem measure_theory.outer_measure.is_caratheodory_union {α : Type u} (m : measure_theory.outer_measure α) {s₁ s₂ : set α} :
m.is_caratheodory s₁m.is_caratheodory s₂m.is_caratheodory (s₁ s₂)

theorem measure_theory.outer_measure.measure_inter_union {α : Type u} (m : measure_theory.outer_measure α) {s₁ s₂ : set α} (h : s₁ s₂ ) (h₁ : m.is_caratheodory s₁) {t : set α} :
m (t (s₁ s₂)) = m (t s₁) + m (t s₂)

theorem measure_theory.outer_measure.is_caratheodory_Union_lt {α : Type u} (m : measure_theory.outer_measure α) {s : set α} {n : } :
(∀ (i : ), i < nm.is_caratheodory (s i))m.is_caratheodory (⋃ (i : ) (H : i < n), s i)

theorem measure_theory.outer_measure.is_caratheodory_inter {α : Type u} (m : measure_theory.outer_measure α) {s₁ s₂ : set α} :
m.is_caratheodory s₁m.is_caratheodory s₂m.is_caratheodory (s₁ s₂)

theorem measure_theory.outer_measure.is_caratheodory_sum {α : Type u} (m : measure_theory.outer_measure α) {s : set α} (h : ∀ (i : ), m.is_caratheodory (s i)) (hd : pairwise (disjoint on s)) {t : set α} {n : } :
∑ (i : ) in finset.range n, m (t s i) = m (t ⋃ (i : ) (H : i < n), s i)

theorem measure_theory.outer_measure.is_caratheodory_Union_nat {α : Type u} (m : measure_theory.outer_measure α) {s : set α} :
(∀ (i : ), m.is_caratheodory (s i))pairwise (disjoint on s)m.is_caratheodory (⋃ (i : ), s i)

theorem measure_theory.outer_measure.f_Union {α : Type u} (m : measure_theory.outer_measure α) {s : set α} :
(∀ (i : ), m.is_caratheodory (s i))pairwise (disjoint on s)(m (⋃ (i : ), s i) = ∑' (i : ), m (s i))

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

Equations

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

Equations
theorem measure_theory.outer_measure.is_caratheodory_iff {α : Type u} (m : measure_theory.outer_measure α) {s : set α} :
m.caratheodory.is_measurable' s ∀ (t : set α), m t = m (t s) + m (t \ s)

theorem measure_theory.outer_measure.is_caratheodory_iff_le {α : Type u} (m : measure_theory.outer_measure α) {s : set α} :
m.caratheodory.is_measurable' s ∀ (t : set α), m (t s) + m (t \ s) m t

theorem measure_theory.outer_measure.Union_eq_of_caratheodory {α : Type u} (m : measure_theory.outer_measure α) {s : set α} :
(∀ (i : ), m.caratheodory.is_measurable' (s i))pairwise (disjoint on s)(m (⋃ (i : ), s i) = ∑' (i : ), m (s i))

theorem measure_theory.outer_measure.of_function_caratheodory {α : Type u_1} {m : set αennreal} {s : set α} {h₀ : m = 0} :
(∀ (t : set α), m (t s) + m (t \ s) m t)(measure_theory.outer_measure.of_function m h₀).caratheodory.is_measurable' s

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
theorem measure_theory.outer_measure.Inf_apply {α : Type u_1} {m : set (measure_theory.outer_measure α)} {s : set α} :
m.nonempty((Inf m) s = ⨅ (t : set α) (h2 : s set.Union t), ∑' (n : ), ⨅ (μ : measure_theory.outer_measure α) (h3 : μ 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.

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

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 = is_measurable). 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 measure_theory.extend {α : Type u_1} {P : α → Prop} :
(Π (s : α), P sennreal)α → ennreal

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

Equations
theorem measure_theory.extend_eq {α : Type u_1} {P : α → Prop} (m : Π (s : α), P sennreal) {s : α} (h : P s) :

theorem measure_theory.le_extend {α : Type u_1} {P : α → Prop} (m : Π (s : α), P sennreal) {s : α} (h : P s) :

theorem measure_theory.extend_empty {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P sennreal} (P0 : P ) :

theorem measure_theory.extend_Union_nat {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P sennreal} (PU : ∀ ⦃f : set α⦄, (∀ (i : ), P (f i))P (⋃ (i : ), f i)) {f : set α} (hm : ∀ (i : ), P (f i)) :
(m (⋃ (i : ), f i) _ = ∑' (i : ), m (f i) _)(measure_theory.extend m (⋃ (i : ), f i) = ∑' (i : ), measure_theory.extend m (f i))

theorem measure_theory.extend_Union_le_tsum_nat' {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P sennreal} (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 α) :
measure_theory.extend m (⋃ (i : ), s i) ∑' (i : ), measure_theory.extend m (s i)

theorem measure_theory.extend_mono' {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P sennreal} (m_mono : ∀ ⦃s₁ s₂ : set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ s₂m s₁ hs₁ m s₂ hs₂) ⦃s₁ s₂ : set α⦄ :
P s₁s₁ s₂measure_theory.extend m s₁ measure_theory.extend m s₂

theorem measure_theory.extend_Union {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P sennreal} (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} [encodable β] {f : β → set α} :
pairwise (disjoint on f)(∀ (i : β), P (f i))(measure_theory.extend m (⋃ (i : β), f i) = ∑' (i : β), measure_theory.extend m (f i))

theorem measure_theory.extend_union {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P sennreal} (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₁ s₂ : set α} :
disjoint s₁ s₂P s₁P s₂measure_theory.extend m (s₁ s₂) = measure_theory.extend m s₁ + measure_theory.extend m s₂

def measure_theory.induced_outer_measure {α : Type u_1} {P : set α → Prop} (m : Π (s : set α), P sennreal) (P0 : P ) :

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
theorem measure_theory.induced_outer_measure_eq_extend' {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P sennreal} {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 α} :

theorem measure_theory.induced_outer_measure_eq' {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P sennreal} {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) :

theorem measure_theory.induced_outer_measure_eq_infi {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P sennreal} {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 α) :
(measure_theory.induced_outer_measure m P0 m0) s = ⨅ (t : set α) (ht : P t) (h : s t), m t ht

theorem measure_theory.induced_outer_measure_preimage {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P sennreal} {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 α} :

theorem measure_theory.induced_outer_measure_exists_set {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P sennreal} {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 : (measure_theory.induced_outer_measure m P0 m0) s < ) {ε : ℝ≥0} :
0 < ε(∃ (t : set α) (ht : P t), s t (measure_theory.induced_outer_measure m P0 m0) t (measure_theory.induced_outer_measure m P0 m0) s + ε)

theorem measure_theory.induced_outer_measure_caratheodory {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P sennreal} {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 α) :

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

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

theorem measure_theory.extend_mono {α : Type u_1} [measurable_space α] {m : Π (s : set α), is_measurable sennreal} (m0 : m is_measurable.empty = 0) (mU : ∀ ⦃f : set α⦄ (hm : ∀ (i : ), is_measurable (f i)), pairwise (disjoint on f)(m (⋃ (i : ), f i) _ = ∑' (i : ), m (f i) _)) {s₁ s₂ : set α} :
is_measurable s₁s₁ s₂measure_theory.extend m s₁ measure_theory.extend m s₂

theorem measure_theory.extend_Union_le_tsum_nat {α : Type u_1} [measurable_space α] {m : Π (s : set α), is_measurable sennreal} (m0 : m is_measurable.empty = 0) (mU : ∀ ⦃f : set α⦄ (hm : ∀ (i : ), is_measurable (f i)), pairwise (disjoint on f)(m (⋃ (i : ), f i) _ = ∑' (i : ), m (f i) _)) (s : set α) :
measure_theory.extend m (⋃ (i : ), s i) ∑' (i : ), measure_theory.extend m (s i)

theorem measure_theory.induced_outer_measure_eq_extend {α : Type u_1} [measurable_space α] {m : Π (s : set α), is_measurable sennreal} (m0 : m is_measurable.empty = 0) (mU : ∀ ⦃f : set α⦄ (hm : ∀ (i : ), is_measurable (f i)), pairwise (disjoint on f)(m (⋃ (i : ), f i) _ = ∑' (i : ), m (f i) _)) {s : set α} :

theorem measure_theory.induced_outer_measure_eq {α : Type u_1} [measurable_space α] {m : Π (s : set α), is_measurable sennreal} (m0 : m is_measurable.empty = 0) (mU : ∀ ⦃f : set α⦄ (hm : ∀ (i : ), is_measurable (f i)), pairwise (disjoint on f)(m (⋃ (i : ), f i) _ = ∑' (i : ), m (f i) _)) {s : set α} (hs : is_measurable s) :

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
theorem measure_theory.outer_measure.trim_congr {α : Type u_1} [measurable_space α] {m₁ m₂ : measure_theory.outer_measure α} :
(∀ {s : set α}, is_measurable sm₁ s = m₂ s)m₁.trim = m₂.trim

theorem measure_theory.outer_measure.trim_le_trim {α : Type u_1} [measurable_space α] {m₁ m₂ : measure_theory.outer_measure α} :
m₁ m₂m₁.trim m₂.trim

theorem measure_theory.outer_measure.le_trim_iff {α : Type u_1} [measurable_space α] {m₁ m₂ : measure_theory.outer_measure α} :
m₁ m₂.trim ∀ (s : set α), is_measurable sm₁ s m₂ s

theorem measure_theory.outer_measure.trim_eq_infi {α : Type u_1} [measurable_space α] (m : measure_theory.outer_measure α) (s : set α) :
(m.trim) s = ⨅ (t : set α) (st : s t) (ht : is_measurable t), m t

theorem measure_theory.outer_measure.trim_eq_infi' {α : Type u_1} [measurable_space α] (m : measure_theory.outer_measure α) (s : set α) :
(m.trim) s = ⨅ (t : {t // s t is_measurable t}), m t

@[simp]
theorem measure_theory.outer_measure.trim_zero {α : Type u_1} [measurable_space α] :
0.trim = 0

theorem measure_theory.outer_measure.trim_add {α : Type u_1} [measurable_space α] (m₁ m₂ : measure_theory.outer_measure α) :
(m₁ + m₂).trim = m₁.trim + m₂.trim

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