# mathlibdocumentation

measure_theory.measure.outer_measure

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

• `outer_measure.bounded_by` is the greatest outer measure that is at most the given function. If you know that the given functions sends `∅` to `0`, then `outer_measure.of_function` is a special case.
• `caratheodory` is the Carathéodory-measurable space of an outer measure.
• `Inf_eq_of_function_Inf_gen` is a characterization of the infimum of outer measures.
• `induced_outer_measure` is the measure induced by a function on a subset of `set α`

## Tags #

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

structure measure_theory.outer_measure (α : Type u_1) :
Type u_1

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

@[protected, instance]
def measure_theory.outer_measure.has_coe_to_fun {α : Type u_1} :
(λ (_x : , set αℝ≥0∞)
Equations
@[simp]
@[simp]
theorem measure_theory.outer_measure.empty' {α : Type u_1}  :
m = 0
theorem measure_theory.outer_measure.mono' {α : Type u_1} {s₁ s₂ : set α} (h : s₁ s₂) :
m s₁ m s₂
theorem measure_theory.outer_measure.mono_null {α : Type u_1} {s t : set α} (h : s t) (ht : m t = 0) :
m s = 0
@[protected]
theorem measure_theory.outer_measure.Union {α : Type u_1} {β : Type u_2} [encodable β] (s : β → set α) :
m (⋃ (i : β), s i) ∑' (i : β), m (s i)
theorem measure_theory.outer_measure.Union_null {α : Type u_1} {β : Type u_2} [encodable β] {s : β → set α} (h : ∀ (i : β), m (s i) = 0) :
m (⋃ (i : β), s i) = 0
@[simp]
theorem measure_theory.outer_measure.Union_null_iff {α : Type u_1} {β : Type u_2} [encodable β] {s : β → set α} :
m (⋃ (i : β), s i) = 0 ∀ (i : β), m (s i) = 0
theorem measure_theory.outer_measure.bUnion_null_iff {α : Type u_1} {β : Type u_2} {s : set β} (hs : s.countable) {t : β → set α} :
m (⋃ (i : β) (H : i s), t i) = 0 ∀ (i : β), i sm (t i) = 0
theorem measure_theory.outer_measure.sUnion_null_iff {α : Type u_1} {S : set (set α)} (hS : S.countable) :
m (⋃₀S) = 0 ∀ (s : set α), s Sm s = 0
@[protected]
theorem measure_theory.outer_measure.Union_finset {α : Type u_1} {β : Type u_2} (s : β → set α) (t : finset β) :
m (⋃ (i : β) (H : i t), s i) ∑ (i : β) in t, m (s i)
@[protected]
theorem measure_theory.outer_measure.union {α : Type u_1} (s₁ s₂ : set α) :
m (s₁ s₂) m s₁ + m s₂
theorem measure_theory.outer_measure.null_of_locally_null {α : Type u_1} (s : set α) (hs : ∀ (x : α), x s(∃ (u : set α) (H : u 𝓝[s] x), 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 measure_theory.outer_measure.exists_mem_forall_mem_nhds_within_pos {α : Type u_1} {s : set α} (hs : m s 0) :
∃ (x : α) (H : x s), ∀ (t : set α), t 𝓝[s] x0 < m t

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

theorem measure_theory.outer_measure.Union_of_tendsto_zero {α : Type u_1} {ι : Type u_2} {s : ι → set α} (l : filter ι) [l.ne_bot] (h0 : filter.tendsto (λ (k : ι), m ((⋃ (n : ι), s n) \ s k)) l (𝓝 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 `at_top` on `ι = ℕ`), then `m S = ⨆ n, m (s n)`.

theorem measure_theory.outer_measure.Union_nat_of_monotone_of_tsum_ne_top {α : Type u_1} {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 measure_theory.outer_measure.le_inter_add_diff {α : Type u_1} {t : set α} (s : set α) :
m t m (t s) + m (t \ s)
theorem measure_theory.outer_measure.diff_null {α : Type u_1} (s : set α) {t : set α} (ht : m t = 0) :
m (s \ t) = m s
theorem measure_theory.outer_measure.union_null {α : Type u_1} {s₁ s₂ : set α} (h₁ : m s₁ = 0) (h₂ : m s₂ = 0) :
m (s₁ s₂) = 0
theorem measure_theory.outer_measure.coe_fn_injective {α : Type u_1} :
function.injective (λ (μ : (s : set α), μ s)
@[ext]
theorem measure_theory.outer_measure.ext {α : Type u_1} {μ₁ μ₂ : measure_theory.outer_measure α} (h : ∀ (s : set α), μ₁ s = μ₂ s) :
μ₁ = μ₂
theorem measure_theory.outer_measure.ext_nonempty {α : Type u_1} {μ₁ μ₂ : measure_theory.outer_measure α} (h : ∀ (s : set α), s.nonemptyμ₁ s = μ₂ s) :
μ₁ = μ₂

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

@[protected, instance]
def measure_theory.outer_measure.has_zero {α : Type u_1} :
Equations
@[simp]
theorem measure_theory.outer_measure.coe_zero {α : Type u_1} :
0 = 0
@[protected, instance]
Equations
@[protected, instance]
noncomputable def measure_theory.outer_measure.has_add {α : Type u_1} :
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
@[protected, instance]
noncomputable def measure_theory.outer_measure.add_comm_monoid {α : Type u_1} :
Equations
@[protected, instance]
noncomputable def measure_theory.outer_measure.has_scalar {α : Type u_1} :
Equations
@[simp]
theorem measure_theory.outer_measure.coe_smul {α : Type u_1} (c : ℝ≥0∞)  :
(c m) = c m
theorem measure_theory.outer_measure.smul_apply {α : Type u_1} (c : ℝ≥0∞) (s : set α) :
(c m) s = c * m s
@[protected, instance]
noncomputable def measure_theory.outer_measure.module {α : Type u_1} :
Equations
@[protected, instance]
def measure_theory.outer_measure.has_bot {α : Type u_1} :
Equations
@[simp]
theorem measure_theory.outer_measure.coe_bot {α : Type u_1} :
= 0
@[protected, instance]
Equations
@[protected, instance]
Equations
theorem measure_theory.outer_measure.univ_eq_zero_iff {α : Type u_1}  :
= 0 m = 0
@[protected, instance]
noncomputable def measure_theory.outer_measure.has_Sup {α : Type u_1} :
Equations
@[protected, instance]
noncomputable def measure_theory.outer_measure.complete_lattice {α : Type u_1} :
Equations
@[simp]
theorem measure_theory.outer_measure.Sup_apply {α : Type u_1} (ms : set ) (s : set α) :
(Sup ms) s = ⨆ (m : (H : m ms), m s
@[simp]
theorem measure_theory.outer_measure.supr_apply {α : Type u_1} {ι : Sort u_2} (f : ι → ) (s : set α) :
(⨆ (i : ι), f i) s = ⨆ (i : ι), (f i) s
@[norm_cast]
theorem measure_theory.outer_measure.coe_supr {α : Type u_1} {ι : Sort u_2} (f : ι → ) :
(⨆ (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
theorem measure_theory.outer_measure.smul_supr {α : Type u_1} {ι : Sort u_2} (f : ι → ) (c : ℝ≥0∞) :
(c ⨆ (i : ι), f i) = ⨆ (i : ι), c f i
theorem measure_theory.outer_measure.mono'' {α : Type u_1} {m₁ m₂ : measure_theory.outer_measure α} {s₁ s₂ : set α} (hm : m₁ m₂) (hs : s₁ s₂) :
m₁ s₁ m₂ s₂
noncomputable def measure_theory.outer_measure.map {α : Type u_1} {β : Type u_2} (f : α → β) :

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 : α → β) (s : set β) :
s = m (f ⁻¹' s)
@[simp]
theorem measure_theory.outer_measure.map_id {α : Type u_1}  :
@[simp]
theorem measure_theory.outer_measure.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ)  :
theorem measure_theory.outer_measure.map_mono {α : Type u_1} {β : Type u_2} (f : α → β) :
@[simp]
theorem measure_theory.outer_measure.map_sup {α : Type u_1} {β : Type u_2} (f : α → β) (m m' : measure_theory.outer_measure α) :
(m m') =
@[simp]
theorem measure_theory.outer_measure.map_supr {α : Type u_1} {β : Type u_2} {ι : Sort u_3} (f : α → β) (m : ι → ) :
(⨆ (i : ι), m i) = ⨆ (i : ι), (m i)
@[protected, instance]
noncomputable def measure_theory.outer_measure.functor  :
Equations
@[protected, instance]
noncomputable def measure_theory.outer_measure.dirac {α : Type u_1} (a : α) :

The dirac outer measure.

Equations
@[simp]
theorem measure_theory.outer_measure.dirac_apply {α : Type u_1} (a : α) (s : set α) :
= s.indicator (λ (_x : α), 1) a
noncomputable def measure_theory.outer_measure.sum {α : Type u_1} {ι : Type u_2} (f : ι → ) :

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 : ι → ) (s : set α) :
= ∑' (i : ι), (f i) s
theorem measure_theory.outer_measure.smul_dirac_apply {α : Type u_1} (a : ℝ≥0∞) (b : α) (s : set α) :
= s.indicator (λ (_x : α), a) b
noncomputable def measure_theory.outer_measure.comap {α : Type u_1} {β : Type u_2} (f : α → β) :

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 : α → β) (s : set α) :
s = m (f '' s)
theorem measure_theory.outer_measure.comap_mono {α : Type u_1} {β : Type u_2} (f : α → β) :
@[simp]
theorem measure_theory.outer_measure.comap_supr {α : Type u_1} {β : Type u_2} {ι : Sort u_3} (f : α → β) (m : ι → ) :
(⨆ (i : ι), m i) = ⨆ (i : ι), (m i)
noncomputable def measure_theory.outer_measure.restrict {α : Type u_1} (s : set α) :

Restrict an `outer_measure` to a set.

Equations
@[simp]
theorem measure_theory.outer_measure.restrict_apply {α : Type u_1} (s t : set α)  :
= m (t s)
theorem measure_theory.outer_measure.restrict_mono {α : Type u_1} {s t : set α} (h : s t) {m m' : measure_theory.outer_measure α} (hm : m m') :
@[simp]
theorem measure_theory.outer_measure.restrict_univ {α : Type u_1}  :
@[simp]
theorem measure_theory.outer_measure.restrict_empty {α : Type u_1}  :
@[simp]
theorem measure_theory.outer_measure.restrict_supr {α : Type u_1} {ι : Sort u_2} (s : set α) (m : ι → ) :
(⨆ (i : ι), m i) = ⨆ (i : ι),
theorem measure_theory.outer_measure.map_comap {α : Type u_1} {β : Type u_2} (f : α → β)  :
theorem measure_theory.outer_measure.map_comap_le {α : Type u_1} {β : Type u_2} (f : α → β)  :
theorem measure_theory.outer_measure.restrict_le_self {α : Type u_1} (s : set α) :
@[simp]
theorem measure_theory.outer_measure.map_le_restrict_range {α : Type u_1} {β : Type u_2} {ma : measure_theory.outer_measure α} {mb : measure_theory.outer_measure β} {f : α → β} :
mb
theorem measure_theory.outer_measure.map_comap_of_surjective {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.surjective f)  :
theorem measure_theory.outer_measure.le_comap_map {α : Type u_1} {β : Type u_2} (f : α → β)  :
theorem measure_theory.outer_measure.comap_map {α : Type u_1} {β : Type u_2} {f : α → β} (hf : function.injective f)  :
@[simp]
theorem measure_theory.outer_measure.top_apply {α : Type u_1} {s : set α} (h : s.nonempty) :
theorem measure_theory.outer_measure.top_apply' {α : Type u_1} (s : set α) :
s = ⨅ (h : s = ), 0
@[simp]
theorem measure_theory.outer_measure.comap_top {α : Type u_1} {β : Type u_2} (f : α → β) :
theorem measure_theory.outer_measure.map_top {α : Type u_1} {β : Type u_2} (f : α → β) :
theorem measure_theory.outer_measure.map_top_of_surjective {α : Type u_1} {β : Type u_2} (f : α → β) (hf : function.surjective f) :
@[protected]
noncomputable def measure_theory.outer_measure.of_function {α : Type u_1} (m : set αℝ≥0∞) (m_empty : m = 0) :

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 αℝ≥0∞) (m_empty : m = 0) (s : set α) :
m_empty) s = ⨅ (t : set α) (h : s , ∑' (n : ), m (t n)
theorem measure_theory.outer_measure.of_function_le {α : Type u_1} {m : set αℝ≥0∞} {m_empty : m = 0} (s : set α) :
m_empty) s m s
theorem measure_theory.outer_measure.of_function_eq {α : Type u_1} {m : set αℝ≥0∞} {m_empty : m = 0} (s : set α) (m_mono : ∀ ⦃t : set α⦄, s tm s m t) (m_subadd : ∀ (s : set α), m (⋃ (i : ), s i) ∑' (i : ), m (s i)) :
m_empty) s = m s
theorem measure_theory.outer_measure.le_of_function {α : Type u_1} {m : set αℝ≥0∞} {m_empty : m = 0}  :
μ ∀ (s : set α), μ s m s
theorem measure_theory.outer_measure.is_greatest_of_function {α : Type u_1} {m : set αℝ≥0∞} {m_empty : m = 0} :
is_greatest {μ : | ∀ (s : set α), μ s m s} m_empty)
theorem measure_theory.outer_measure.of_function_eq_Sup {α : Type u_1} {m : set αℝ≥0∞} {m_empty : m = 0} :
= Sup {μ : | ∀ (s : set α), μ s m s}
theorem measure_theory.outer_measure.of_function_union_of_top_of_nonempty_inter {α : Type u_1} {m : set αℝ≥0∞} {m_empty : m = 0} {s t : set α} (h : ∀ (u : set α), (s u).nonempty(t u).nonemptym u = ) :
m_empty) (s t) = m_empty) s + 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 `μ = measure_theory.outer_measure.of_function 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 measure_theory.outer_measure.comap_of_function {α : Type u_1} {m : set αℝ≥0∞} {m_empty : m = 0} {β : Type u_2} (f : β → α) (h : ) :
theorem measure_theory.outer_measure.map_of_function_le {α : Type u_1} {m : set αℝ≥0∞} {m_empty : m = 0} {β : Type u_2} (f : α → β) :
measure_theory.outer_measure.of_function (λ (s : set β), m (f ⁻¹' s)) m_empty
theorem measure_theory.outer_measure.map_of_function {α : Type u_1} {m : set αℝ≥0∞} {m_empty : m = 0} {β : Type u_2} {f : α → β} (hf : function.injective f) :
= measure_theory.outer_measure.of_function (λ (s : set β), m (f ⁻¹' s)) m_empty
theorem measure_theory.outer_measure.restrict_of_function {α : Type u_1} {m : set αℝ≥0∞} {m_empty : m = 0} (s : set α) (hm : monotone m) :
theorem measure_theory.outer_measure.smul_of_function {α : Type u_1} {m : set αℝ≥0∞} {m_empty : m = 0} {c : ℝ≥0∞} (hc : c ) :
c =
noncomputable def measure_theory.outer_measure.bounded_by {α : Type u_1} (m : set αℝ≥0∞) :

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 `outer_measure.of_function`, except that it doesn't require `m ∅ = 0`.

Equations
theorem measure_theory.outer_measure.bounded_by_le {α : Type u_1} {m : set αℝ≥0∞} (s : set α) :
theorem measure_theory.outer_measure.bounded_by_eq_of_function {α : Type u_1} {m : set αℝ≥0∞} (m_empty : m = 0) (s : set α) :
theorem measure_theory.outer_measure.bounded_by_apply {α : Type u_1} {m : set αℝ≥0∞} (s : set α) :
= ⨅ (t : set α) (h : s , ∑' (n : ), ⨆ (h : (t n).nonempty), m (t n)
theorem measure_theory.outer_measure.bounded_by_eq {α : Type u_1} {m : set αℝ≥0∞} (s : set α) (m_empty : m = 0) (m_mono : ∀ ⦃t : set α⦄, s tm s m t) (m_subadd : ∀ (s : set α), m (⋃ (i : ), s i) ∑' (i : ), m (s i)) :
@[simp]
theorem measure_theory.outer_measure.le_bounded_by {α : Type u_1} {m : set αℝ≥0∞}  :
∀ (s : set α), μ s m s
theorem measure_theory.outer_measure.le_bounded_by' {α : Type u_1} {m : set αℝ≥0∞}  :
∀ (s : set α), s.nonemptyμ s m s
theorem measure_theory.outer_measure.smul_bounded_by {α : Type u_1} {m : set αℝ≥0∞} {c : ℝ≥0∞} (hc : c ) :
theorem measure_theory.outer_measure.comap_bounded_by {α : Type u_1} {m : set αℝ≥0∞} {β : Type u_2} (f : β → α) (h : monotone (λ (s : {s // s.nonempty}), m s) ) :
theorem measure_theory.outer_measure.bounded_by_union_of_top_of_nonempty_inter {α : Type u_1} {m : set αℝ≥0∞} {s t : set α} (h : ∀ (u : set α), (s u).nonempty(t u).nonemptym u = ) :

If `m u = ∞` for any set `u` that has nonempty intersection both with `s` and `t`, then `μ (s ∪ t) = μ s + μ t`, where `μ = measure_theory.outer_measure.bounded_by 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 measure_theory.outer_measure.is_caratheodory {α : Type u} (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
theorem measure_theory.outer_measure.is_caratheodory_iff_le' {α : Type u} {s : set α} :
∀ (t : set α), m (t s) + m (t \ s) m t
@[simp]
theorem measure_theory.outer_measure.is_caratheodory_union {α : Type u} {s₁ s₂ : set α} (h₁ : m.is_caratheodory s₁) (h₂ : m.is_caratheodory s₂) :
m.is_caratheodory (s₁ s₂)
theorem measure_theory.outer_measure.measure_inter_union {α : Type u} {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} {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} {s₁ s₂ : set α} (h₁ : m.is_caratheodory s₁) (h₂ : m.is_caratheodory s₂) :
m.is_caratheodory (s₁ s₂)
theorem measure_theory.outer_measure.is_caratheodory_sum {α : Type u} {s : set α} (h : ∀ (i : ), m.is_caratheodory (s i)) (hd : pairwise (disjoint on s)) {t : set α} {n : } :
∑ (i : ) in , m (t s i) = m (t ⋃ (i : ) (H : i < n), s i)
theorem measure_theory.outer_measure.is_caratheodory_Union_nat {α : Type u} {s : set α} (h : ∀ (i : ), m.is_caratheodory (s i)) (hd : pairwise (disjoint on s)) :
m.is_caratheodory (⋃ (i : ), s i)
theorem measure_theory.outer_measure.f_Union {α : Type u} {s : set α} (h : ∀ (i : ), m.is_caratheodory (s i)) (hd : 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
@[protected]

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} {s : set α} :
∀ (t : set α), m t = m (t s) + m (t \ s)
theorem measure_theory.outer_measure.is_caratheodory_iff_le {α : Type u} {s : set α} :
∀ (t : set α), m (t s) + m (t \ s) m t
@[protected]
theorem measure_theory.outer_measure.Union_eq_of_caratheodory {α : Type u} {s : set α} (h : ∀ (i : ), m.caratheodory.measurable_set' (s i)) (hd : 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 αℝ≥0∞} {s : set α} {h₀ : m = 0} (hs : ∀ (t : set α), m (t s) + m (t \ s) m t) :
theorem measure_theory.outer_measure.bounded_by_caratheodory {α : Type u_1} {m : set αℝ≥0∞} {s : set α} (hs : ∀ (t : set α), m (t s) + m (t \ s) m t) :
@[simp]
theorem measure_theory.outer_measure.le_sum_caratheodory {α : Type u_1} {ι : Type u_2} (m : ι → ) :
(⨅ (i : ι), (m i).caratheodory)
@[simp]
theorem measure_theory.outer_measure.dirac_caratheodory {α : Type u_1} (a : α) :
noncomputable def measure_theory.outer_measure.Inf_gen {α : Type u_1} (m : set ) (s : set α) :

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

theorem measure_theory.outer_measure.Inf_apply' {α : Type u_1} {m : set } {s : set α} (h : s.nonempty) :
(Inf m) s = ⨅ (t : set α) (h2 : s , ∑' (n : ), ⨅ (μ : (h3 : μ 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 measure_theory.outer_measure.infi_apply {α : Type u_1} {ι : Sort u_2} [nonempty ι] (m : ι → ) (s : set α) :
(⨅ (i : ι), m i) s = ⨅ (t : set α) (h2 : s , ∑' (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 measure_theory.outer_measure.infi_apply' {α : Type u_1} {ι : Sort u_2} (m : ι → ) {s : set α} (hs : s.nonempty) :
(⨅ (i : ι), m i) s = ⨅ (t : set α) (h2 : s , ∑' (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 measure_theory.outer_measure.binfi_apply {α : Type u_1} {ι : Type u_2} {I : set ι} (hI : I.nonempty) (m : ι → ) (s : set α) :
(⨅ (i : ι) (H : i I), m i) s = ⨅ (t : set α) (h2 : s , ∑' (n : ), ⨅ (i : ι) (H : 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 measure_theory.outer_measure.binfi_apply' {α : Type u_1} {ι : Type u_2} (I : set ι) (m : ι → ) {s : set α} (hs : s.nonempty) :
(⨅ (i : ι) (H : i I), m i) s = ⨅ (t : set α) (h2 : s , ∑' (n : ), ⨅ (i : ι) (H : 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 measure_theory.outer_measure.map_infi_le {α : Type u_1} {ι : Sort u_2} {β : Type u_3} (f : α → β) (m : ι → ) :
(⨅ (i : ι), m i) ⨅ (i : ι), (m i)
theorem measure_theory.outer_measure.comap_infi {α : Type u_1} {ι : Sort u_2} {β : Type u_3} (f : α → β) (m : ι → ) :
(⨅ (i : ι), m i) = ⨅ (i : ι), (m i)
theorem measure_theory.outer_measure.map_infi {α : Type u_1} {ι : Sort u_2} {β : Type u_3} {f : α → β} (hf : function.injective f) (m : ι → ) :
(⨅ (i : ι), m i) = (⨅ (i : ι), (m i))
theorem measure_theory.outer_measure.map_infi_comap {α : Type u_1} {ι : Sort u_2} {β : Type u_3} [nonempty ι] {f : α → β} (m : ι → ) :
(⨅ (i : ι), (m i)) = ⨅ (i : ι),
theorem measure_theory.outer_measure.map_binfi_comap {α : Type u_1} {ι : Type u_2} {β : Type u_3} {I : set ι} (hI : I.nonempty) {f : α → β} (m : ι → ) :
(⨅ (i : ι) (H : i I), (m i)) = ⨅ (i : ι) (H : i I),
theorem measure_theory.outer_measure.restrict_infi_restrict {α : Type u_1} {ι : Sort u_2} (s : set α) (m : ι → ) :
(⨅ (i : ι), (m i)) = (⨅ (i : ι), m i)
theorem measure_theory.outer_measure.restrict_infi {α : Type u_1} {ι : Sort u_2} [nonempty ι] (s : set α) (m : ι → ) :
(⨅ (i : ι), m i) = ⨅ (i : ι),
theorem measure_theory.outer_measure.restrict_binfi {α : Type u_1} {ι : Type u_2} {I : set ι} (hI : I.nonempty) (s : set α) (m : ι → ) :
(⨅ (i : ι) (H : i I), m i) = ⨅ (i : ι) (H : i I),
theorem measure_theory.outer_measure.restrict_Inf_eq_Inf_restrict {α : Type u_1} (m : set ) {s : set α} (hm : m.nonempty) :

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 = measurable_set`). 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.

noncomputable def measure_theory.extend {α : Type u_1} {P : α → Prop} (m : Π (s : α), P sℝ≥0∞) (s : α) :

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
• = ⨅ (h : P s), m s h
theorem measure_theory.extend_eq {α : Type u_1} {P : α → Prop} (m : Π (s : α), P sℝ≥0∞) {s : α} (h : P s) :
= m s h
theorem measure_theory.extend_eq_top {α : Type u_1} {P : α → Prop} (m : Π (s : α), P sℝ≥0∞) {s : α} (h : ¬P s) :
theorem measure_theory.le_extend {α : Type u_1} {P : α → Prop} (m : Π (s : α), P sℝ≥0∞) {s : α} (h : P s) :
m s h
theorem measure_theory.extend_congr {α : Type u_1} {P : α → Prop} (m : Π (s : α), P sℝ≥0∞) {β : Type u_2} {Pb : β → Prop} {mb : Π (s : β), Pb sℝ≥0∞} {sa : α} {sb : β} (hP : P sa Pb sb) (hm : ∀ (ha : P sa) (hb : Pb sb), m sa ha = mb sb hb) :
=
theorem measure_theory.extend_empty {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P sℝ≥0∞} (P0 : P ) (m0 : m P0 = 0) :
theorem measure_theory.extend_Union_nat {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P sℝ≥0∞} (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) _) :
(⋃ (i : ), f i) = ∑' (i : ), (f i)
theorem measure_theory.extend_Union_le_tsum_nat' {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P sℝ≥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) _) (s : set α) :
(⋃ (i : ), s i) ∑' (i : ), (s i)
theorem measure_theory.extend_mono' {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P sℝ≥0∞} (m_mono : ∀ ⦃s₁ s₂ : set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ s₂m s₁ hs₁ m s₂ hs₂) ⦃s₁ s₂ : set α⦄ (h₁ : P s₁) (hs : s₁ s₂) :
theorem measure_theory.extend_Union {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P sℝ≥0∞} (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 α} (hd : pairwise (disjoint on f)) (hm : ∀ (i : β), P (f i)) :
(⋃ (i : β), f i) = ∑' (i : β), (f i)
theorem measure_theory.extend_union {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P sℝ≥0∞} (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 α} (hd : disjoint s₁ s₂) (h₁ : P s₁) (h₂ : P s₂) :
(s₁ s₂) =
noncomputable def measure_theory.induced_outer_measure {α : Type u_1} {P : set α → Prop} (m : Π (s : set α), P sℝ≥0∞) (P0 : P ) (m0 : m P0 = 0) :

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.le_induced_outer_measure {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P sℝ≥0∞} {P0 : P } {m0 : m P0 = 0}  :
∀ (s : set α) (hs : P s), μ s m s hs
theorem measure_theory.induced_outer_measure_union_of_false_of_nonempty_inter {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P sℝ≥0∞} {P0 : P } {m0 : m P0 = 0} {s t : set α} (h : ∀ (u : set α), (s u).nonempty(t u).nonempty¬P u) :
m0) (s t) = m0) s + 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 `μ = induced_outer_measure 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 measure_theory.induced_outer_measure_eq_extend' {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P sℝ≥0∞} {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) :
m0) s =
theorem measure_theory.induced_outer_measure_eq' {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P sℝ≥0∞} {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) :
m0) s = m s hs
theorem measure_theory.induced_outer_measure_eq_infi {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P sℝ≥0∞} {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 α) :
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 sℝ≥0∞} {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 α} :
m0) (f ⁻¹' A) = m0) A
theorem measure_theory.induced_outer_measure_exists_set {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P sℝ≥0∞} {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 : m0) s ) {ε : ℝ≥0∞} (hε : ε 0) :
∃ (t : set α) (ht : P t), s t m0) t m0) s + ε
theorem measure_theory.induced_outer_measure_caratheodory {α : Type u_1} {P : set α → Prop} {m : Π (s : set α), P sℝ≥0∞} {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 α) :
∀ (t : set α), P t m0) (t s) + m0) (t \ s) m0) t

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 `measurable_set` for some measurable space, then we can remove some hypotheses of the above lemmas.

theorem measure_theory.extend_mono {α : Type u_1} {m : Π (s : set α), } (m0 : = 0) (mU : ∀ ⦃f : set α⦄ (hm : ∀ (i : ), measurable_set (f i)), pairwise (disjoint on f)m (⋃ (i : ), f i) _ = ∑' (i : ), m (f i) _) {s₁ s₂ : set α} (h₁ : measurable_set s₁) (hs : s₁ s₂) :
theorem measure_theory.extend_Union_le_tsum_nat {α : Type u_1} {m : Π (s : set α), } (m0 : = 0) (mU : ∀ ⦃f : set α⦄ (hm : ∀ (i : ), measurable_set (f i)), pairwise (disjoint on f)m (⋃ (i : ), f i) _ = ∑' (i : ), m (f i) _) (s : set α) :
(⋃ (i : ), s i) ∑' (i : ), (s i)
theorem measure_theory.induced_outer_measure_eq_extend {α : Type u_1} {m : Π (s : set α), } (m0 : = 0) (mU : ∀ ⦃f : set α⦄ (hm : ∀ (i : ), measurable_set (f i)), pairwise (disjoint on f)m (⋃ (i : ), f i) _ = ∑' (i : ), m (f i) _) {s : set α} (hs : measurable_set s) :
theorem measure_theory.induced_outer_measure_eq {α : Type u_1} {m : Π (s : set α), } (m0 : = 0) (mU : ∀ ⦃f : set α⦄ (hm : ∀ (i : ), measurable_set (f i)), pairwise (disjoint on f)m (⋃ (i : ), f i) _ = ∑' (i : ), m (f i) _) {s : set α} (hs : measurable_set s) :
= m s hs
noncomputable def measure_theory.outer_measure.trim {α : Type u_1}  :

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.le_trim {α : Type u_1}  :
m m.trim
theorem measure_theory.outer_measure.trim_eq {α : Type u_1} {s : set α} (hs : measurable_set s) :
(m.trim) s = m s
theorem measure_theory.outer_measure.trim_congr {α : Type u_1} {m₁ m₂ : measure_theory.outer_measure α} (H : ∀ {s : set α}, m₁ s = m₂ s) :
m₁.trim = m₂.trim
theorem measure_theory.outer_measure.trim_mono {α : Type u_1}  :
theorem measure_theory.outer_measure.le_trim_iff {α : Type u_1} {m₁ m₂ : measure_theory.outer_measure α} :
m₁ m₂.trim ∀ (s : set α), m₁ s m₂ s
theorem measure_theory.outer_measure.trim_le_trim_iff {α : Type u_1} {m₁ m₂ : measure_theory.outer_measure α} :
m₁.trim m₂.trim ∀ (s : set α), m₁ s m₂ s
theorem measure_theory.outer_measure.trim_eq_trim_iff {α : Type u_1} {m₁ m₂ : measure_theory.outer_measure α} :
m₁.trim = m₂.trim ∀ (s : set α), m₁ s = m₂ s
theorem measure_theory.outer_measure.trim_eq_infi {α : Type u_1} (s : set α) :
(m.trim) s = ⨅ (t : set α) (st : s t) (ht : , m t
theorem measure_theory.outer_measure.trim_eq_infi' {α : Type u_1} (s : set α) :
(m.trim) s = ⨅ (t : {t // s t , m t
theorem measure_theory.outer_measure.trim_trim {α : Type u_1}  :
@[simp]
theorem measure_theory.outer_measure.trim_zero {α : Type u_1}  :
0.trim = 0
theorem measure_theory.outer_measure.trim_sum_ge {α : Type u_1} {ι : Type u_2} (m : ι → ) :
theorem measure_theory.outer_measure.exists_measurable_superset_eq_trim {α : Type u_1} (s : set α) :
∃ (t : set α), s t m t = (m.trim) s
theorem measure_theory.outer_measure.exists_measurable_superset_of_trim_eq_zero {α : Type u_1} {s : set α} (h : (m.trim) s = 0) :
∃ (t : set α), s t m t = 0
theorem measure_theory.outer_measure.exists_measurable_superset_forall_eq_trim {α : Type u_1} {ι : Type u_2} [encodable ι] (μ : ι → ) (s : set α) :
∃ (t : set α), s t ∀ (i : ι), (μ i) t = ((μ i).trim) 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 measure_theory.outer_measure.trim_binop {α : Type u_1} {m₁ m₂ m₃ : measure_theory.outer_measure α} {op : ℝ≥0∞} (h : ∀ (s : set α), m₁ s = op (m₂ s) (m₃ s)) (s : set α) :
(m₁.trim) s = op ((m₂.trim) s) ((m₃.trim) 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 measure_theory.outer_measure.trim_op {α : Type u_1} {m₁ m₂ : measure_theory.outer_measure α} {op : ℝ≥0∞ℝ≥0∞} (h : ∀ (s : set α), m₁ s = op (m₂ s)) (s : set α) :
(m₁.trim) s = op ((m₂.trim) s)

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

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

`trim` is additive.

theorem measure_theory.outer_measure.trim_smul {α : Type u_1} (c : ℝ≥0∞)  :
(c m).trim = c m.trim

`trim` respects scalar multiplication.

theorem measure_theory.outer_measure.trim_sup {α : Type u_1} (m₁ m₂ : measure_theory.outer_measure α) :
(m₁ m₂).trim = m₁.trim m₂.trim

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

theorem measure_theory.outer_measure.trim_supr {α : Type u_1} {ι : Type u_2} [encodable ι] (μ : ι → ) :
(⨆ (i : ι), μ i).trim = ⨆ (i : ι), (μ i).trim

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

theorem measure_theory.outer_measure.restrict_trim {α : Type u_1} {s : set α} (hs : measurable_set s) :

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.