mathlib3 documentation

measure_theory.measure.outer_measure

Outer Measures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

References #

Tags #

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

theorem measure_theory.outer_measure.mono' {α : Type u_1} (m : measure_theory.outer_measure α) {s₁ s₂ : set α} (h : s₁ s₂) :
m s₁ m s₂
theorem measure_theory.outer_measure.mono_null {α : Type u_1} (m : measure_theory.outer_measure α) {s t : set α} (h : s t) (ht : m t = 0) :
m s = 0
theorem measure_theory.outer_measure.pos_of_subset_ne_zero {α : Type u_1} (m : measure_theory.outer_measure α) {a b : set α} (hs : a b) (hnz : m a 0) :
0 < m b
@[protected]
theorem measure_theory.outer_measure.Union {α : Type u_1} (m : measure_theory.outer_measure α) {β : Type u_2} [countable β] (s : β set α) :
m ( (i : β), s i) ∑' (i : β), m (s i)
theorem measure_theory.outer_measure.Union_null {α : Type u_1} {β : Type u_2} [countable β] (m : measure_theory.outer_measure α) {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} [countable β] (m : measure_theory.outer_measure α) {s : β set α} :
m ( (i : β), s i) = 0 (i : β), m (s i) = 0
@[simp]
theorem measure_theory.outer_measure.Union_null_iff' {α : Type u_1} (m : measure_theory.outer_measure α) {ι : Prop} {s : ι set α} :
m ( (i : ι), s i) = 0 (i : ι), m (s i) = 0

A version of Union_null_iff for unions indexed by Props. TODO: in the long run it would be better to combine this with Union_null_iff by generalising to Sort.

theorem measure_theory.outer_measure.bUnion_null_iff {α : Type u_1} {β : Type u_2} (m : measure_theory.outer_measure α) {s : set β} (hs : s.countable) {t : β set α} :
m ( (i : β) (H : i s), t i) = 0 (i : β), i s m (t i) = 0
theorem measure_theory.outer_measure.sUnion_null_iff {α : Type u_1} (m : measure_theory.outer_measure α) {S : set (set α)} (hS : S.countable) :
m (⋃₀ S) = 0 (s : set α), s S m s = 0
@[protected]
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) t.sum (λ (i : β), m (s i))
@[protected]
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.null_of_locally_null {α : Type u_1} [topological_space α] [topological_space.second_countable_topology α] (m : measure_theory.outer_measure α) (s : set α) (hs : (x : α), x s ( (u : set α) (H : u nhds_within 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.

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} (m : measure_theory.outer_measure α) {s : ι set α} (l : filter ι) [l.ne_bot] (h0 : filter.tendsto (λ (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 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} (m : measure_theory.outer_measure α) {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} {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 α} (ht : m t = 0) :
m (s \ t) = m s
theorem measure_theory.outer_measure.union_null {α : Type u_1} (m : measure_theory.outer_measure α) {s₁ s₂ : set α} (h₁ : m s₁ = 0) (h₂ : m s₂ = 0) :
m (s₁ s₂) = 0
@[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]
Equations
@[simp]
theorem measure_theory.outer_measure.coe_zero {α : Type u_1} :
0 = 0
@[protected, 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
@[protected, instance]
Equations
theorem measure_theory.outer_measure.smul_apply {α : Type u_1} {R : Type u_3} [has_smul R ennreal] [is_scalar_tower R ennreal ennreal] (c : R) (m : measure_theory.outer_measure α) (s : set α) :
(c m) s = c m s
@[protected, instance]
Equations
@[simp]
@[protected, instance]
Equations
@[protected, instance]
Equations
@[protected, instance]
Equations
@[simp]
@[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
@[norm_cast]
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
theorem measure_theory.outer_measure.smul_supr {α : Type u_1} {R : Type u_3} [has_smul R ennreal] [is_scalar_tower R ennreal ennreal] {ι : Sort u_2} (f : ι measure_theory.outer_measure α) (c : R) :
(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₂

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_supr {α : Type u_1} {β : Type u_2} {ι : Sort u_3} (f : α β) (m : ι measure_theory.outer_measure α) :
@[protected, instance]
Equations
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 α) :

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 α) :
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 α) :
@[simp]
theorem measure_theory.outer_measure.comap_supr {α : Type u_1} {β : Type u_2} {ι : Sort u_3} (f : α β) (m : ι measure_theory.outer_measure β) :
@[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]
@[protected]
noncomputable def measure_theory.outer_measure.of_function {α : Type u_1} (m : set α ennreal) (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 α 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 α) (m_mono : ⦃t : set α⦄, s t m s m t) (m_subadd : (s : set α), m ( (i : ), s i) ∑' (i : ), m (s i)) :
theorem measure_theory.outer_measure.le_of_function {α : Type u_1} {m : set α ennreal} {m_empty : m = 0} {μ : measure_theory.outer_measure α} :

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.

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_apply {α : Type u_1} {m : set α ennreal} (s : set α) :
(measure_theory.outer_measure.bounded_by m) s = (t : set α) (h : s set.Union t), ∑' (n : ), (h : (t n).nonempty), m (t n)
theorem measure_theory.outer_measure.bounded_by_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)) :

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.

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_union {α : Type u} (m : measure_theory.outer_measure α) {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} (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 < n m.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 α} (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} (m : measure_theory.outer_measure α) {s : set α} (h : (i : ), m.is_caratheodory (s i)) (hd : pairwise (disjoint on s)) {t : set α} {n : } :
(finset.range n).sum (λ (i : ), m (t s i)) = m (t (i : ) (H : i < n), s i)
theorem measure_theory.outer_measure.f_Union {α : Type u} (m : measure_theory.outer_measure α) {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
@[protected]
theorem measure_theory.outer_measure.Union_eq_of_caratheodory {α : Type u} (m : measure_theory.outer_measure α) {s : set α} (h : (i : ), 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 α ennreal} {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 α ennreal} {s : set α} (hs : (t : set α), m (t s) + m (t \ s) m t) :
noncomputable def measure_theory.outer_measure.Inf_gen {α : Type u_1} (m : set (measure_theory.outer_measure α)) (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
theorem measure_theory.outer_measure.Inf_apply {α : Type u_1} {m : set (measure_theory.outer_measure α)} {s : set α} (h : m.nonempty) :
(has_Inf.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.

theorem measure_theory.outer_measure.Inf_apply' {α : Type u_1} {m : set (measure_theory.outer_measure α)} {s : set α} (h : s.nonempty) :
(has_Inf.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 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 : ι measure_theory.outer_measure α) (s : set α) :
( (i : ι), m i) s = (t : set α) (h2 : s set.Union 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 measure_theory.outer_measure.infi_apply' {α : Type u_1} {ι : Sort u_2} (m : ι measure_theory.outer_measure α) {s : set α} (hs : s.nonempty) :
( (i : ι), m i) s = (t : set α) (h2 : s set.Union 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 measure_theory.outer_measure.binfi_apply {α : Type u_1} {ι : Type u_2} {I : set ι} (hI : I.nonempty) (m : ι measure_theory.outer_measure α) (s : set α) :
( (i : ι) (H : i I), m i) s = (t : set α) (h2 : s set.Union t), ∑' (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 : ι measure_theory.outer_measure α) {s : set α} (hs : s.nonempty) :
( (i : ι) (H : i I), m i) s = (t : set α) (h2 : s set.Union t), ∑' (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 : ι measure_theory.outer_measure α) :
theorem measure_theory.outer_measure.comap_infi {α : Type u_1} {ι : Sort u_2} {β : Type u_3} (f : α β) (m : ι measure_theory.outer_measure β) :
theorem measure_theory.outer_measure.restrict_binfi {α : Type u_1} {ι : Type u_2} {I : set ι} (hI : I.nonempty) (s : set α) (m : ι measure_theory.outer_measure α) :
(measure_theory.outer_measure.restrict s) ( (i : ι) (H : i I), m i) = (i : ι) (H : i I), (measure_theory.outer_measure.restrict s) (m i)

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 ennreal) (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
theorem measure_theory.smul_extend {α : Type u_1} {P : α Prop} (m : Π (s : α), P s ennreal) {R : Type u_2} [has_zero R] [smul_with_zero R ennreal] [is_scalar_tower R ennreal ennreal] [no_zero_smul_divisors R ennreal] {c : R} (hc : c 0) :
c measure_theory.extend m = measure_theory.extend (λ (s : α) (h : P s), c m s h)
theorem measure_theory.extend_eq {α : Type u_1} {P : α Prop} (m : Π (s : α), P s ennreal) {s : α} (h : P s) :
theorem measure_theory.extend_eq_top {α : Type u_1} {P : α Prop} (m : Π (s : α), P s ennreal) {s : α} (h : ¬P s) :
theorem measure_theory.le_extend {α : Type u_1} {P : α Prop} (m : Π (s : α), P s ennreal) {s : α} (h : P s) :
theorem measure_theory.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) :
@[simp]
theorem measure_theory.extend_top {α : Type u_1} {P : α Prop} :
measure_theory.extend (λ (s : α) (h : P s), ) =
theorem measure_theory.extend_empty {α : Type u_1} {P : set α Prop} {m : Π (s : set α), P s ennreal} (P0 : P ) (m0 : m P0 = 0) :
theorem measure_theory.extend_Union_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) _) :
theorem measure_theory.extend_Union_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 α) :
theorem measure_theory.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₁ s₂ : set α⦄ (h₁ : P s₁) (hs : s₁ s₂) :
theorem measure_theory.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) _) {β : Type u_2} [countable β] {f : β set α} (hd : pairwise (disjoint on f)) (hm : (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 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₁ s₂ : set α} (hd : disjoint s₁ s₂) (h₁ : P s₁) (h₂ : P s₂) :
noncomputable def measure_theory.induced_outer_measure {α : Type u_1} {P : set α Prop} (m : Π (s : set α), P s ennreal) (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 ennreal} {P0 : P } {m0 : m P0 = 0} {μ : measure_theory.outer_measure α} :
μ measure_theory.induced_outer_measure m P0 m0 (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 ennreal} {P0 : P } {m0 : m P0 = 0} {s t : set α} (h : (u : set α), (s u).nonempty (t u).nonempty ¬P u) :

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 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) :
theorem measure_theory.induced_outer_measure_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) :
theorem measure_theory.induced_outer_measure_eq_infi {α : 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 α) :
(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 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 α} :
theorem measure_theory.induced_outer_measure_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 : (measure_theory.induced_outer_measure m P0 m0) s ) {ε : ennreal} (hε : ε 0) :
theorem measure_theory.induced_outer_measure_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 α) :

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} [measurable_space α] {m : Π (s : set α), measurable_set s ennreal} (m0 : m measurable_set.empty = 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} [measurable_space α] {m : Π (s : set α), measurable_set s ennreal} (m0 : m measurable_set.empty = 0) (mU : ⦃f : set α⦄ (hm : (i : ), measurable_set (f i)), pairwise (disjoint on f) m ( (i : ), f i) _ = ∑' (i : ), m (f i) _) (s : set α) :
theorem measure_theory.induced_outer_measure_eq_extend {α : Type u_1} [measurable_space α] {m : Π (s : set α), measurable_set s ennreal} (m0 : m measurable_set.empty = 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} [measurable_space α] {m : Π (s : set α), measurable_set s ennreal} (m0 : m measurable_set.empty = 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) :

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 α} (H : {s : set α}, measurable_set s m₁ s = m₂ s) :
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 α), measurable_set s m₁ s m₂ s
theorem measure_theory.outer_measure.trim_eq_trim_iff {α : Type u_1} [measurable_space α] {m₁ m₂ : measure_theory.outer_measure α} :
m₁.trim = m₂.trim (s : set α), measurable_set s m₁ 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 : measurable_set t), m t
@[simp]
theorem measure_theory.outer_measure.exists_measurable_superset_forall_eq_trim {α : Type u_1} [measurable_space α] {ι : Sort u_2} [countable ι] (μ : ι measure_theory.outer_measure α) (s : set α) :
(t : set α), s t measurable_set 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} [measurable_space α] {m₁ m₂ m₃ : measure_theory.outer_measure α} {op : ennreal ennreal ennreal} (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} [measurable_space α] {m₁ m₂ : measure_theory.outer_measure α} {op : ennreal ennreal} (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} [measurable_space α] (m₁ m₂ : measure_theory.outer_measure α) :
(m₁ + m₂).trim = m₁.trim + m₂.trim

trim is additive.

trim respects scalar multiplication.

theorem measure_theory.outer_measure.trim_sup {α : Type u_1} [measurable_space α] (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} [measurable_space α] {ι : Sort u_2} [countable ι] (μ : ι measure_theory.outer_measure α) :
( (i : ι), μ i).trim = (i : ι), (μ i).trim

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

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.