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:
μ ∅ = 0;μis monotone;μ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_byis the greatest outer measure that is at most the given function. If you know that the given functions sends∅to0, thenouter_measure.of_functionis a special case.caratheodoryis the Carathéodory-measurable space of an outer measure.Inf_eq_of_function_Inf_genis a characterization of the infimum of outer measures.induced_outer_measureis the measure induced by a function on a subset ofset α
References #
- https://en.wikipedia.org/wiki/Outer_measure
- https://en.wikipedia.org/wiki/Carath%C3%A9odory%27s_criterion
Tags #
outer measure, Carathéodory-measurable, Carathéodory's criterion
- measure_of : set α → ℝ≥0∞
- empty : c.measure_of ∅ = 0
- mono : ∀ {s₁ s₂ : set α}, s₁ ⊆ s₂ → c.measure_of s₁ ≤ c.measure_of s₂
- Union_nat : ∀ (s : ℕ → set α), c.measure_of (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), c.measure_of (s i)
An outer measure is a countably subadditive monotone function that sends ∅ to 0.
@[instance]
Equations
- measure_theory.outer_measure.has_coe_to_fun = {F := λ (m : measure_theory.outer_measure α), set α → ℝ≥0∞, coe := λ (m : measure_theory.outer_measure α), m.measure_of}
@[simp]
theorem
measure_theory.outer_measure.measure_of_eq_coe
{α : Type u_1}
(m : measure_theory.outer_measure α) :
m.measure_of = ⇑m
@[simp]
theorem
measure_theory.outer_measure.mono'
{α : Type u_1}
(m : measure_theory.outer_measure α)
{s₁ s₂ : set α}
(h : s₁ ⊆ s₂) :
theorem
measure_theory.outer_measure.Union
{α : Type u_1}
(m : measure_theory.outer_measure α)
{β : Type u_2}
[encodable β]
(s : β → set α) :
theorem
measure_theory.outer_measure.Union_null
{α : Type u_1}
(m : measure_theory.outer_measure α)
{β : Type u_2}
[encodable β]
{s : β → set α}
(h : ∀ (i : β), ⇑m (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 β) :
theorem
measure_theory.outer_measure.union
{α : Type u_1}
(m : measure_theory.outer_measure α)
(s₁ s₂ : set α) :
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 (𝓝 0)) :
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) ≠ ⊤) :
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.coe_fn_injective
{α : Type u_1} :
function.injective (λ (μ : measure_theory.outer_measure α) (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'.
@[instance]
Equations
- measure_theory.outer_measure.has_zero = {zero := {measure_of := λ (_x : set α), 0, empty := measure_theory.outer_measure.has_zero._proof_1, mono := _, Union_nat := _}}
@[instance]
Equations
- measure_theory.outer_measure.has_add = {add := λ (m₁ m₂ : measure_theory.outer_measure α), {measure_of := λ (s : set α), ⇑m₁ s + ⇑m₂ s, empty := _, mono := _, Union_nat := _}}
@[simp]
theorem
measure_theory.outer_measure.coe_add
{α : Type u_1}
(m₁ m₂ : measure_theory.outer_measure α) :
theorem
measure_theory.outer_measure.add_apply
{α : Type u_1}
(m₁ m₂ : measure_theory.outer_measure α)
(s : set α) :
@[instance]
Equations
- measure_theory.outer_measure.add_comm_monoid = {add := has_add.add measure_theory.outer_measure.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := add_comm_monoid.nsmul (function.injective.add_comm_monoid (show measure_theory.outer_measure α → set α → ℝ≥0∞, from coe_fn) measure_theory.outer_measure.coe_fn_injective measure_theory.outer_measure.add_comm_monoid._proof_4 measure_theory.outer_measure.add_comm_monoid._proof_5), nsmul_zero' := _, nsmul_succ' := _, add_comm := _}
@[instance]
Equations
- measure_theory.outer_measure.has_scalar = {smul := λ (c : ℝ≥0∞) (m : measure_theory.outer_measure α), {measure_of := λ (s : set α), c * ⇑m s, empty := _, mono := _, Union_nat := _}}
@[simp]
theorem
measure_theory.outer_measure.coe_smul
{α : Type u_1}
(c : ℝ≥0∞)
(m : measure_theory.outer_measure α) :
theorem
measure_theory.outer_measure.smul_apply
{α : Type u_1}
(c : ℝ≥0∞)
(m : measure_theory.outer_measure α)
(s : set α) :
@[instance]
Equations
- measure_theory.outer_measure.semimodule = {to_distrib_mul_action := {to_mul_action := {to_has_scalar := {smul := has_scalar.smul measure_theory.outer_measure.has_scalar}, one_smul := _, mul_smul := _}, smul_add := _, smul_zero := _}, add_smul := _, zero_smul := _}
@[instance]
Equations
@[instance]
Equations
- measure_theory.outer_measure.outer_measure.order_bot = {bot := 0, le := λ (m₁ m₂ : measure_theory.outer_measure α), ∀ (s : set α), ⇑m₁ s ≤ ⇑m₂ s, lt := partial_order.lt._default (λ (m₁ m₂ : measure_theory.outer_measure α), ∀ (s : set α), ⇑m₁ s ≤ ⇑m₂ s), le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, bot_le := _}
@[instance]
Equations
- measure_theory.outer_measure.has_Sup = {Sup := λ (ms : set (measure_theory.outer_measure α)), {measure_of := λ (s : set α), ⨆ (m : measure_theory.outer_measure α) (H : m ∈ ms), ⇑m s, empty := _, mono := _, Union_nat := _}}
@[instance]
Equations
- measure_theory.outer_measure.complete_lattice = {sup := complete_lattice.sup (complete_lattice_of_Sup (measure_theory.outer_measure α) measure_theory.outer_measure.complete_lattice._proof_1), le := order_bot.le measure_theory.outer_measure.outer_measure.order_bot, lt := order_bot.lt measure_theory.outer_measure.outer_measure.order_bot, le_refl := _, le_trans := _, lt_iff_le_not_le := _, le_antisymm := _, le_sup_left := _, le_sup_right := _, sup_le := _, inf := complete_lattice.inf (complete_lattice_of_Sup (measure_theory.outer_measure α) measure_theory.outer_measure.complete_lattice._proof_1), inf_le_left := _, inf_le_right := _, le_inf := _, top := complete_lattice.top (complete_lattice_of_Sup (measure_theory.outer_measure α) measure_theory.outer_measure.complete_lattice._proof_1), le_top := _, bot := order_bot.bot measure_theory.outer_measure.outer_measure.order_bot, bot_le := _, Sup := complete_lattice.Sup (complete_lattice_of_Sup (measure_theory.outer_measure α) measure_theory.outer_measure.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf := complete_lattice.Inf (complete_lattice_of_Sup (measure_theory.outer_measure α) measure_theory.outer_measure.complete_lattice._proof_1), Inf_le := _, le_Inf := _}
@[simp]
theorem
measure_theory.outer_measure.Sup_apply
{α : Type u_1}
(ms : set (measure_theory.outer_measure α))
(s : set α) :
@[simp]
theorem
measure_theory.outer_measure.supr_apply
{α : Type u_1}
{ι : Sort u_2}
(f : ι → measure_theory.outer_measure α)
(s : set α) :
theorem
measure_theory.outer_measure.coe_supr
{α : Type u_1}
{ι : Sort u_2}
(f : ι → measure_theory.outer_measure α) :
@[simp]
theorem
measure_theory.outer_measure.sup_apply
{α : Type u_1}
(m₁ m₂ : measure_theory.outer_measure α)
(s : set α) :
theorem
measure_theory.outer_measure.smul_supr
{α : Type u_1}
{ι : Sort u_2}
(f : ι → measure_theory.outer_measure α)
(c : ℝ≥0∞) :
theorem
measure_theory.outer_measure.mono''
{α : Type u_1}
{m₁ m₂ : measure_theory.outer_measure α}
{s₁ s₂ : set α}
(hm : m₁ ≤ m₂)
(hs : s₁ ⊆ s₂) :
The pushforward of m along f. The outer measure on s is defined to be m (f ⁻¹' s).
Equations
- measure_theory.outer_measure.map f = {to_fun := λ (m : measure_theory.outer_measure α), {measure_of := λ (s : set β), ⇑m (f ⁻¹' s), empty := _, mono := _, Union_nat := _}, map_add' := _, map_smul' := _}
@[simp]
theorem
measure_theory.outer_measure.map_apply
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(m : measure_theory.outer_measure α)
(s : set β) :
@[simp]
@[simp]
theorem
measure_theory.outer_measure.map_map
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
(f : α → β)
(g : β → γ)
(m : measure_theory.outer_measure α) :
⇑(measure_theory.outer_measure.map g) (⇑(measure_theory.outer_measure.map f) m) = ⇑(measure_theory.outer_measure.map (g ∘ f)) m
@[simp]
theorem
measure_theory.outer_measure.map_sup
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(m m' : measure_theory.outer_measure α) :
⇑(measure_theory.outer_measure.map f) (m ⊔ m') = ⇑(measure_theory.outer_measure.map f) m ⊔ ⇑(measure_theory.outer_measure.map f) m'
@[simp]
theorem
measure_theory.outer_measure.map_supr
{α : Type u_1}
{β : Type u_2}
{ι : Sort u_3}
(f : α → β)
(m : ι → measure_theory.outer_measure α) :
⇑(measure_theory.outer_measure.map f) (⨆ (i : ι), m i) = ⨆ (i : ι), ⇑(measure_theory.outer_measure.map f) (m i)
@[instance]
Equations
- measure_theory.outer_measure.functor = {map := λ (α β : Type u_1) (f : α → β), ⇑(measure_theory.outer_measure.map f), map_const := λ (α β : Type u_1), (λ (f : β → α), ⇑(measure_theory.outer_measure.map f)) ∘ function.const β}
The dirac outer measure.
Equations
- measure_theory.outer_measure.dirac a = {measure_of := λ (s : set α), s.indicator (λ (_x : α), 1) a, empty := _, mono := _, Union_nat := _}
@[simp]
theorem
measure_theory.outer_measure.dirac_apply
{α : Type u_1}
(a : α)
(s : set α) :
⇑(measure_theory.outer_measure.dirac a) s = s.indicator (λ (_x : α), 1) a
def
measure_theory.outer_measure.sum
{α : Type u_1}
{ι : Type u_2}
(f : ι → measure_theory.outer_measure α) :
The sum of an (arbitrary) collection of outer measures.
Equations
- measure_theory.outer_measure.sum f = {measure_of := λ (s : set α), ∑' (i : ι), ⇑(f i) s, empty := _, mono := _, Union_nat := _}
@[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 : ℝ≥0∞)
(b : α)
(s : set α) :
⇑(a • measure_theory.outer_measure.dirac b) s = s.indicator (λ (_x : α), a) b
Pullback of an outer_measure: comap f μ s = μ (f '' s).
Equations
- measure_theory.outer_measure.comap f = {to_fun := λ (m : measure_theory.outer_measure β), {measure_of := λ (s : set α), ⇑m (f '' s), empty := _, mono := _, Union_nat := _}, map_add' := _, map_smul' := _}
@[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 β) :
⇑(measure_theory.outer_measure.comap f) (⨆ (i : ι), m i) = ⨆ (i : ι), ⇑(measure_theory.outer_measure.comap f) (m i)
Restrict an outer_measure to a set.
@[simp]
theorem
measure_theory.outer_measure.restrict_apply
{α : Type u_1}
(s t : set α)
(m : measure_theory.outer_measure α) :
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}
(m : measure_theory.outer_measure α) :
@[simp]
theorem
measure_theory.outer_measure.restrict_empty
{α : Type u_1}
(m : measure_theory.outer_measure α) :
@[simp]
theorem
measure_theory.outer_measure.restrict_supr
{α : Type u_1}
{ι : Sort u_2}
(s : set α)
(m : ι → measure_theory.outer_measure α) :
⇑(measure_theory.outer_measure.restrict s) (⨆ (i : ι), m i) = ⨆ (i : ι), ⇑(measure_theory.outer_measure.restrict s) (m i)
theorem
measure_theory.outer_measure.map_comap
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(m : measure_theory.outer_measure β) :
theorem
measure_theory.outer_measure.map_comap_le
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(m : measure_theory.outer_measure β) :
theorem
measure_theory.outer_measure.restrict_le_self
{α : Type u_1}
(m : measure_theory.outer_measure α)
(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 : α → β} :
⇑(measure_theory.outer_measure.map f) ma ≤ ⇑(measure_theory.outer_measure.restrict (set.range f)) mb ↔ ⇑(measure_theory.outer_measure.map f) ma ≤ mb
theorem
measure_theory.outer_measure.map_comap_of_surjective
{α : Type u_1}
{β : Type u_2}
{f : α → β}
(hf : function.surjective f)
(m : measure_theory.outer_measure β) :
theorem
measure_theory.outer_measure.le_comap_map
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(m : measure_theory.outer_measure α) :
theorem
measure_theory.outer_measure.comap_map
{α : Type u_1}
{β : Type u_2}
{f : α → β}
(hf : function.injective f)
(m : measure_theory.outer_measure α) :
@[simp]
theorem
measure_theory.outer_measure.map_top_of_surjective
{α : Type u_1}
{β : Type u_2}
(f : α → β)
(hf : function.surjective f) :
theorem
measure_theory.outer_measure.of_function_le
{α : Type u_1}
{m : set α → ℝ≥0∞}
{m_empty : m ∅ = 0}
(s : set α) :
⇑(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 α → ℝ≥0∞}
{m_empty : m ∅ = 0}
{μ : measure_theory.outer_measure α} :
theorem
measure_theory.outer_measure.is_greatest_of_function
{α : Type u_1}
{m : set α → ℝ≥0∞}
{m_empty : m ∅ = 0} :
is_greatest {μ : measure_theory.outer_measure α | ∀ (s : set α), ⇑μ s ≤ m s} (measure_theory.outer_measure.of_function m m_empty)
theorem
measure_theory.outer_measure.of_function_eq_Sup
{α : Type u_1}
{m : set α → ℝ≥0∞}
{m_empty : m ∅ = 0} :
measure_theory.outer_measure.of_function m m_empty = Sup {μ : measure_theory.outer_measure α | ∀ (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).nonempty → m u = ⊤) :
⇑(measure_theory.outer_measure.of_function m m_empty) (s ∪ t) = ⇑(measure_theory.outer_measure.of_function m m_empty) s + ⇑(measure_theory.outer_measure.of_function 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 μ = 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 : monotone m ∨ function.surjective f) :
⇑(measure_theory.outer_measure.comap f) (measure_theory.outer_measure.of_function m m_empty) = measure_theory.outer_measure.of_function (λ (s : set β), m (f '' s)) _
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.map f) (measure_theory.outer_measure.of_function m m_empty) ≤ 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.map f) (measure_theory.outer_measure.of_function m m_empty) = 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) :
⇑(measure_theory.outer_measure.restrict s) (measure_theory.outer_measure.of_function m m_empty) = measure_theory.outer_measure.of_function (λ (t : set α), m (t ∩ s)) _
theorem
measure_theory.outer_measure.smul_of_function
{α : Type u_1}
{m : set α → ℝ≥0∞}
{m_empty : m ∅ = 0}
{c : ℝ≥0∞}
(hc : c ≠ ⊤) :
c • measure_theory.outer_measure.of_function m m_empty = measure_theory.outer_measure.of_function (c • m) _
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
- measure_theory.outer_measure.bounded_by m = measure_theory.outer_measure.of_function (λ (s : set α), ⨆ (h : s.nonempty), m s) _
theorem
measure_theory.outer_measure.bounded_by_le
{α : Type u_1}
{m : set α → ℝ≥0∞}
(s : set α) :
⇑(measure_theory.outer_measure.bounded_by m) s ≤ m s
theorem
measure_theory.outer_measure.bounded_by_eq_of_function
{α : Type u_1}
{m : set α → ℝ≥0∞}
(m_empty : m ∅ = 0)
(s : set α) :
⇑(measure_theory.outer_measure.bounded_by m) s = ⇑(measure_theory.outer_measure.of_function m m_empty) s
theorem
measure_theory.outer_measure.le_bounded_by
{α : Type u_1}
{m : set α → ℝ≥0∞}
{μ : measure_theory.outer_measure α} :
theorem
measure_theory.outer_measure.le_bounded_by'
{α : Type u_1}
{m : set α → ℝ≥0∞}
{μ : measure_theory.outer_measure α} :
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) ∨ function.surjective f) :
⇑(measure_theory.outer_measure.comap f) (measure_theory.outer_measure.bounded_by m) = measure_theory.outer_measure.bounded_by (λ (s : set β), m (f '' 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).nonempty → m 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}
(m : measure_theory.outer_measure α)
(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).
theorem
measure_theory.outer_measure.is_caratheodory_iff_le'
{α : Type u}
(m : measure_theory.outer_measure α)
{s : set α} :
@[simp]
theorem
measure_theory.outer_measure.is_caratheodory_empty
{α : Type u}
(m : measure_theory.outer_measure α) :
theorem
measure_theory.outer_measure.is_caratheodory_compl
{α : Type u}
(m : measure_theory.outer_measure α)
{s₁ : set α} :
m.is_caratheodory s₁ → m.is_caratheodory s₁ᶜ
@[simp]
theorem
measure_theory.outer_measure.is_caratheodory_compl_iff
{α : Type u}
(m : measure_theory.outer_measure α)
{s : set α} :
m.is_caratheodory sᶜ ↔ m.is_caratheodory s
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.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 : ℕ} :
theorem
measure_theory.outer_measure.is_caratheodory_Union_nat
{α : Type u}
(m : measure_theory.outer_measure α)
{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}
(m : measure_theory.outer_measure α)
{s : ℕ → set α}
(h : ∀ (i : ℕ), m.is_caratheodory (s i))
(hd : pairwise (disjoint on s)) :
def
measure_theory.outer_measure.caratheodory_dynkin
{α : Type u}
(m : measure_theory.outer_measure α) :
The Carathéodory-measurable sets for an outer measure m form a Dynkin system.
Equations
- m.caratheodory_dynkin = {has := m.is_caratheodory, has_empty := _, has_compl := _, has_Union_nat := _}
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 α} :
theorem
measure_theory.outer_measure.is_caratheodory_iff_le
{α : Type u}
(m : measure_theory.outer_measure α)
{s : set α} :
theorem
measure_theory.outer_measure.Union_eq_of_caratheodory
{α : Type u}
(m : measure_theory.outer_measure α)
{s : ℕ → set α}
(h : ∀ (i : ℕ), m.caratheodory.measurable_set' (s i))
(hd : pairwise (disjoint on s)) :
@[simp]
theorem
measure_theory.outer_measure.le_add_caratheodory
{α : Type u_1}
(m₁ m₂ : measure_theory.outer_measure α) :
m₁.caratheodory ⊓ m₂.caratheodory ≤ (m₁ + m₂).caratheodory
theorem
measure_theory.outer_measure.le_sum_caratheodory
{α : Type u_1}
{ι : Type u_2}
(m : ι → measure_theory.outer_measure α) :
(⨅ (i : ι), (m i).caratheodory) ≤ (measure_theory.outer_measure.sum m).caratheodory
theorem
measure_theory.outer_measure.le_smul_caratheodory
{α : Type u_1}
(a : ℝ≥0∞)
(m : measure_theory.outer_measure α) :
m.caratheodory ≤ (a • m).caratheodory
@[simp]
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
- measure_theory.outer_measure.Inf_gen m s = ⨅ (μ : measure_theory.outer_measure α) (h : μ ∈ m), ⇑μ s
theorem
measure_theory.outer_measure.Inf_gen_def
{α : Type u_1}
(m : set (measure_theory.outer_measure α))
(t : set α) :
measure_theory.outer_measure.Inf_gen m t = ⨅ (μ : measure_theory.outer_measure α) (h : μ ∈ m), ⇑μ t
theorem
measure_theory.outer_measure.Inf_eq_bounded_by_Inf_gen
{α : Type u_1}
(m : set (measure_theory.outer_measure α)) :
theorem
measure_theory.outer_measure.supr_Inf_gen_nonempty
{α : Type u_1}
{m : set (measure_theory.outer_measure α)}
(h : m.nonempty)
(t : set α) :
(⨆ (h : t.nonempty), measure_theory.outer_measure.Inf_gen m t) = ⨅ (μ : measure_theory.outer_measure α) (h : μ ∈ m), ⇑μ t
theorem
measure_theory.outer_measure.Inf_apply
{α : Type u_1}
{m : set (measure_theory.outer_measure α)}
{s : set α}
(h : m.nonempty) :
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) :
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 α) :
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) :
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 α) :
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) :
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 α) :
⇑(measure_theory.outer_measure.map f) (⨅ (i : ι), m i) ≤ ⨅ (i : ι), ⇑(measure_theory.outer_measure.map f) (m i)
theorem
measure_theory.outer_measure.comap_infi
{α : Type u_1}
{ι : Sort u_2}
{β : Type u_3}
(f : α → β)
(m : ι → measure_theory.outer_measure β) :
⇑(measure_theory.outer_measure.comap f) (⨅ (i : ι), m i) = ⨅ (i : ι), ⇑(measure_theory.outer_measure.comap f) (m i)
theorem
measure_theory.outer_measure.map_infi
{α : Type u_1}
{ι : Sort u_2}
{β : Type u_3}
{f : α → β}
(hf : function.injective f)
(m : ι → measure_theory.outer_measure α) :
⇑(measure_theory.outer_measure.map f) (⨅ (i : ι), m i) = ⇑(measure_theory.outer_measure.restrict (set.range f)) (⨅ (i : ι), ⇑(measure_theory.outer_measure.map f) (m i))
theorem
measure_theory.outer_measure.map_infi_comap
{α : Type u_1}
{ι : Sort u_2}
{β : Type u_3}
[nonempty ι]
{f : α → β}
(m : ι → measure_theory.outer_measure β) :
⇑(measure_theory.outer_measure.map f) (⨅ (i : ι), ⇑(measure_theory.outer_measure.comap f) (m i)) = ⨅ (i : ι), ⇑(measure_theory.outer_measure.map f) (⇑(measure_theory.outer_measure.comap f) (m 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 : ι → measure_theory.outer_measure β) :
⇑(measure_theory.outer_measure.map f) (⨅ (i : ι) (H : i ∈ I), ⇑(measure_theory.outer_measure.comap f) (m i)) = ⨅ (i : ι) (H : i ∈ I), ⇑(measure_theory.outer_measure.map f) (⇑(measure_theory.outer_measure.comap f) (m i))
theorem
measure_theory.outer_measure.restrict_infi_restrict
{α : Type u_1}
{ι : Sort u_2}
(s : set α)
(m : ι → measure_theory.outer_measure α) :
⇑(measure_theory.outer_measure.restrict s) (⨅ (i : ι), ⇑(measure_theory.outer_measure.restrict s) (m i)) = ⇑(measure_theory.outer_measure.restrict s) (⨅ (i : ι), m i)
theorem
measure_theory.outer_measure.restrict_infi
{α : Type u_1}
{ι : Sort u_2}
[nonempty ι]
(s : set α)
(m : ι → measure_theory.outer_measure α) :
⇑(measure_theory.outer_measure.restrict s) (⨅ (i : ι), m i) = ⨅ (i : ι), ⇑(measure_theory.outer_measure.restrict s) (m i)
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)
theorem
measure_theory.outer_measure.restrict_Inf_eq_Inf_restrict
{α : Type u_1}
(m : set (measure_theory.outer_measure α))
{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.
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
- measure_theory.extend m s = ⨅ (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) :
measure_theory.extend m s = m s h
theorem
measure_theory.le_extend
{α : Type u_1}
{P : α → Prop}
(m : Π (s : α), P s → ℝ≥0∞)
{s : α}
(h : P s) :
m s h ≤ measure_theory.extend m s
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) :
measure_theory.extend m sa = measure_theory.extend mb sb
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) _) :
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 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 α) :
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 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₂) :
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 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)) :
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 → ℝ≥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₂) :
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 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}
{μ : measure_theory.outer_measure α} :
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) :
⇑(measure_theory.induced_outer_measure m P0 m0) (s ∪ t) = ⇑(measure_theory.induced_outer_measure m P0 m0) s + ⇑(measure_theory.induced_outer_measure 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 μ = 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) :
⇑(measure_theory.induced_outer_measure m P0 m0) s = measure_theory.extend m 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) :
⇑(measure_theory.induced_outer_measure m P0 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 α) :
⇑(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 → ℝ≥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 α} :
⇑(measure_theory.induced_outer_measure m P0 m0) (⇑f ⁻¹' A) = ⇑(measure_theory.induced_outer_measure m P0 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 : ⇑(measure_theory.induced_outer_measure m P0 m0) s < ⊤)
{ε : ℝ≥0}
(hε : 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 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 α) :
(measure_theory.induced_outer_measure m P0 m0).caratheodory.measurable_set' s ↔ ∀ (t : set α), P t → ⇑(measure_theory.induced_outer_measure m P0 m0) (t ∩ s) + ⇑(measure_theory.induced_outer_measure m P0 m0) (t \ s) ≤ ⇑(measure_theory.induced_outer_measure 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 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 → ℝ≥0∞}
(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₂) :
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 α), measurable_set s → ℝ≥0∞}
(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 α) :
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 α), measurable_set s → ℝ≥0∞}
(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 → ℝ≥0∞}
(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) :
⇑(measure_theory.induced_outer_measure m measurable_set.empty m0) s = m s hs
def
measure_theory.outer_measure.trim
{α : Type u_1}
[measurable_space α]
(m : measure_theory.outer_measure α) :
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
- m.trim = measure_theory.induced_outer_measure (λ (s : set α) (_x : measurable_set s), ⇑m s) measurable_set.empty _
theorem
measure_theory.outer_measure.le_trim
{α : Type u_1}
[measurable_space α]
(m : measure_theory.outer_measure α) :
theorem
measure_theory.outer_measure.trim_eq
{α : Type u_1}
[measurable_space α]
(m : measure_theory.outer_measure α)
{s : set α}
(hs : measurable_set s) :
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) :
theorem
measure_theory.outer_measure.le_trim_iff
{α : Type u_1}
[measurable_space α]
{m₁ m₂ : measure_theory.outer_measure α} :
theorem
measure_theory.outer_measure.trim_eq_infi
{α : Type u_1}
[measurable_space α]
(m : measure_theory.outer_measure α)
(s : set α) :
theorem
measure_theory.outer_measure.trim_eq_infi'
{α : Type u_1}
[measurable_space α]
(m : measure_theory.outer_measure α)
(s : set α) :
theorem
measure_theory.outer_measure.trim_trim
{α : Type u_1}
[measurable_space α]
(m : measure_theory.outer_measure α) :
@[simp]
theorem
measure_theory.outer_measure.trim_sum_ge
{α : Type u_1}
[measurable_space α]
{ι : Type u_2}
(m : ι → measure_theory.outer_measure α) :
measure_theory.outer_measure.sum (λ (i : ι), (m i).trim) ≤ (measure_theory.outer_measure.sum m).trim
theorem
measure_theory.outer_measure.exists_measurable_superset_eq_trim
{α : Type u_1}
[measurable_space α]
(m : measure_theory.outer_measure α)
(s : set α) :
theorem
measure_theory.outer_measure.exists_measurable_superset_of_trim_eq_zero
{α : Type u_1}
[measurable_space α]
{m : measure_theory.outer_measure α}
{s : set α}
(h : ⇑(m.trim) s = 0) :
theorem
measure_theory.outer_measure.exists_measurable_superset_forall_eq_trim
{α : Type u_1}
[measurable_space α]
{ι : Type u_2}
[encodable ι]
(μ : ι → measure_theory.outer_measure α)
(s : set α) :
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 : ℝ≥0∞ → ℝ≥0∞ → ℝ≥0∞}
(h : ∀ (s : set α), ⇑m₁ s = op (⇑m₂ s) (⇑m₃ s))
(s : set α) :
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 : ℝ≥0∞ → ℝ≥0∞}
(h : ∀ (s : set α), ⇑m₁ s = op (⇑m₂ s))
(s : set α) :
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 α) :
trim is additive.
theorem
measure_theory.outer_measure.trim_smul
{α : Type u_1}
[measurable_space α]
(c : ℝ≥0∞)
(m : measure_theory.outer_measure α) :
trim respects scalar multiplication.
theorem
measure_theory.outer_measure.trim_sup
{α : Type u_1}
[measurable_space α]
(m₁ m₂ : measure_theory.outer_measure α) :
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 α]
{ι : Type u_2}
[encodable ι]
(μ : ι → measure_theory.outer_measure α) :
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}
[measurable_space α]
{μ : measure_theory.outer_measure α}
{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.