Outer Measures
An outer measure is a function μ : set α → ennreal, from the powerset of a type to the extended
nonnegative real numbers that satisfies the following conditions:
μ ∅ = 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 α → ennreal that sends ∅ to 0 we can define an outer
measure on α that on s is defined to be the infimum of ∑ᵢ, m (sᵢ) for all collections of sets
sᵢ that cover s. This is the unique maximal outer measure that is at most the given function.
We also define this for functions m defined on a subset of set α, by treating the function as
having value ∞ outside its domain.
Given an outer measure m, the Carathéodory-measurable sets are the sets s such that
for all sets t we have m t = m (t ∩ s) + m (t \ s). This forms a measurable space.
Main definitions and statements
outer_measure.of_functionis the greatest outer measure that is at most the given function.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 α → ennreal
- 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 α → ennreal, 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 α} :
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 α} :
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.coe_fn_injective
{α : Type u_1}
⦃μ₁ μ₂ : measure_theory.outer_measure α⦄ :
@[ext]
theorem
measure_theory.outer_measure.ext
{α : Type u_1}
{μ₁ μ₂ : measure_theory.outer_measure α} :
@[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 := _, add_comm := _}
@[instance]
Equations
- measure_theory.outer_measure.has_scalar = {smul := λ (c : ennreal) (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 : ennreal)
(m : measure_theory.outer_measure α) :
theorem
measure_theory.outer_measure.smul_apply
{α : Type u_1}
(c : ennreal)
(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
- 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), Inf := complete_lattice.Inf (complete_lattice_of_Sup (measure_theory.outer_measure α) measure_theory.outer_measure.complete_lattice._proof_1), le_Sup := _, Sup_le := _, Inf_le := _, le_Inf := _}
@[simp]
theorem
measure_theory.outer_measure.Sup_apply
{α : Type u_1}
(ms : set (measure_theory.outer_measure α))
(s : set α) :
⇑(has_Sup.Sup ms) s = ⨆ (m : measure_theory.outer_measure α) (H : m ∈ ms), ⇑m s
@[simp]
theorem
measure_theory.outer_measure.supr_apply
{α : Type u_1}
{ι : Sort u_2}
(f : ι → measure_theory.outer_measure α)
(s : set α) :
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 α) :
def
measure_theory.outer_measure.map
{α : Type u_1}
{β : Type u_2} :
(α → β) → (measure_theory.outer_measure α →ₗ[ennreal] measure_theory.outer_measure β)
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
@[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 α), ⨆ (h : a ∈ s), 1, 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 = ⨆ (h : a ∈ s), 1
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 : ennreal)
(b : α)
(s : set α) :
⇑(a • measure_theory.outer_measure.dirac b) s = ⨆ (h : b ∈ s), a
def
measure_theory.outer_measure.comap
{α : Type u_1}
{β : Type u_2} :
(α → β) → (measure_theory.outer_measure β →ₗ[ennreal] measure_theory.outer_measure α)
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 α) :
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 α) :
def
measure_theory.outer_measure.of_function
{α : Type u_1}
(m : set α → ennreal) :
m ∅ = 0 → measure_theory.outer_measure α
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 α.
theorem
measure_theory.outer_measure.of_function_le
{α : Type u_1}
{m : set α → ennreal}
{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 α → ennreal}
{m_empty : m ∅ = 0}
{μ : measure_theory.outer_measure α} :
def
measure_theory.outer_measure.is_caratheodory
{α : Type u} :
measure_theory.outer_measure α → 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 α} :
m.is_caratheodory s₁ → 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 α} :
m.is_caratheodory s₁ → m.is_caratheodory s₂ → m.is_caratheodory (s₁ ∩ s₂)
theorem
measure_theory.outer_measure.is_caratheodory_sum
{α : Type u}
(m : measure_theory.outer_measure α)
{s : ℕ → set α}
(h : ∀ (i : ℕ), m.is_caratheodory (s i))
(hd : pairwise (disjoint on s))
{t : set α}
{n : ℕ} :
theorem
measure_theory.outer_measure.is_caratheodory_Union_nat
{α : Type u}
(m : measure_theory.outer_measure α)
{s : ℕ → set α} :
(∀ (i : ℕ), m.is_caratheodory (s i)) → pairwise (disjoint on s) → m.is_caratheodory (⋃ (i : ℕ), s i)
theorem
measure_theory.outer_measure.f_Union
{α : Type u}
(m : measure_theory.outer_measure α)
{s : ℕ → set α} :
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 α} :
theorem
measure_theory.outer_measure.of_function_caratheodory
{α : Type u_1}
{m : set α → ennreal}
{s : set α}
{h₀ : m ∅ = 0} :
(∀ (t : set α), m (t ∩ s) + m (t \ s) ≤ m t) → (measure_theory.outer_measure.of_function m h₀).caratheodory.is_measurable s
@[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 : ennreal)
(m : measure_theory.outer_measure α) :
m.caratheodory ≤ (a • m).caratheodory
@[simp]
def
measure_theory.outer_measure.Inf_gen
{α : Type u_1} :
set (measure_theory.outer_measure α) → set α → ennreal
Given a set of outer measures, we define a new function that on a set s is defined to be the
infimum of μ(s) for the outer measures μ in the collection. We ensure that this
function is defined to be 0 on ∅, even if the collection of outer measures is empty.
The outer measure generated by this function is the infimum of the given outer measures.
Equations
- measure_theory.outer_measure.Inf_gen m s = ⨆ (h : s.nonempty), ⨅ (μ : measure_theory.outer_measure α) (h : μ ∈ m), ⇑μ s
@[simp]
theorem
measure_theory.outer_measure.Inf_gen_empty
{α : Type u_1}
(m : set (measure_theory.outer_measure α)) :
theorem
measure_theory.outer_measure.Inf_gen_nonempty1
{α : Type u_1}
(m : set (measure_theory.outer_measure α))
(t : set α) :
t.nonempty → (measure_theory.outer_measure.Inf_gen m t = ⨅ (μ : measure_theory.outer_measure α) (h : μ ∈ m), ⇑μ t)
theorem
measure_theory.outer_measure.Inf_gen_nonempty2
{α : Type u_1}
(m : set (measure_theory.outer_measure α))
(μ : measure_theory.outer_measure α)
(h : μ ∈ m)
(t : set α) :
measure_theory.outer_measure.Inf_gen m t = ⨅ (μ : measure_theory.outer_measure α) (h : μ ∈ m), ⇑μ t
theorem
measure_theory.outer_measure.Inf_eq_of_function_Inf_gen
{α : Type u_1}
(m : set (measure_theory.outer_measure α)) :
Induced Outer Measure
We can extend a function defined on a subset of set α to an outer measure.
The underlying function is called extend, and the measure it induces is called
induced_outer_measure.
Some lemmas below are proven twice, once in the general case, and one where the function m
is only defined on measurable sets (i.e. when P = is_measurable). In the latter cases, we can
remove some hypotheses in the statement. The general version has the same name, but with a prime
at the end.
We can trivially extend a function defined on a subclass of objects (with codomain ennreal)
to all objects by defining it to be ∞ on the objects not in the class.
Equations
- 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 → ennreal)
{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 → ennreal)
{s : α}
(h : P s) :
m s h ≤ measure_theory.extend m s
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)) :
(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 → 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 α) :
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 → ennreal}
(m_mono : ∀ ⦃s₁ s₂ : set α⦄ (hs₁ : P s₁) (hs₂ : P s₂), s₁ ⊆ s₂ → m s₁ hs₁ ≤ m s₂ hs₂)
⦃s₁ s₂ : set α⦄ :
P s₁ → s₁ ⊆ s₂ → measure_theory.extend m s₁ ≤ measure_theory.extend m s₂
theorem
measure_theory.extend_Union
{α : Type u_1}
{P : set α → Prop}
{m : Π (s : set α), P 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}
[encodable β]
{f : β → set α} :
pairwise (disjoint on f) → (∀ (i : β), P (f i)) → (measure_theory.extend m (⋃ (i : β), f i) = ∑' (i : β), measure_theory.extend m (f i))
theorem
measure_theory.extend_union
{α : Type u_1}
{P : set α → Prop}
{m : Π (s : set α), P 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 α} :
disjoint s₁ s₂ → P s₁ → P s₂ → measure_theory.extend m (s₁ ∪ s₂) = measure_theory.extend m s₁ + measure_theory.extend m s₂
def
measure_theory.induced_outer_measure
{α : Type u_1}
{P : set α → Prop}
(m : Π (s : set α), P s → ennreal)
(P0 : P ∅) :
m ∅ P0 = 0 → measure_theory.outer_measure α
Given an arbitrary function on a subset of sets, we can define the outer measure corresponding
to it (this is the unique maximal outer measure that is at most m on the domain of m).
Equations
theorem
measure_theory.induced_outer_measure_eq_extend'
{α : Type u_1}
{P : set α → Prop}
{m : Π (s : set α), P 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 α} :
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 → 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) :
⇑(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 → 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 α} :
⇑(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 → 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 < ⊤)
{ε : nnreal} :
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 α) :
(measure_theory.induced_outer_measure m P0 m0).caratheodory.is_measurable 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 is_measurable for some measurable space, then we can remove some hypotheses of the
above lemmas.
theorem
measure_theory.extend_mono
{α : Type u_1}
[measurable_space α]
{m : Π (s : set α), is_measurable s → ennreal}
(m0 : m ∅ is_measurable.empty = 0)
(mU : ∀ ⦃f : ℕ → set α⦄ (hm : ∀ (i : ℕ), is_measurable (f i)), pairwise (disjoint on f) → (m (⋃ (i : ℕ), f i) _ = ∑' (i : ℕ), m (f i) _))
{s₁ s₂ : set α} :
is_measurable s₁ → s₁ ⊆ s₂ → measure_theory.extend m s₁ ≤ measure_theory.extend m s₂
theorem
measure_theory.extend_Union_le_tsum_nat
{α : Type u_1}
[measurable_space α]
{m : Π (s : set α), is_measurable s → ennreal}
(m0 : m ∅ is_measurable.empty = 0)
(mU : ∀ ⦃f : ℕ → set α⦄ (hm : ∀ (i : ℕ), is_measurable (f i)), pairwise (disjoint on f) → (m (⋃ (i : ℕ), f i) _ = ∑' (i : ℕ), m (f i) _))
(s : ℕ → set α) :
measure_theory.extend m (⋃ (i : ℕ), s i) ≤ ∑' (i : ℕ), measure_theory.extend m (s i)
theorem
measure_theory.induced_outer_measure_eq_extend
{α : Type u_1}
[measurable_space α]
{m : Π (s : set α), is_measurable s → ennreal}
(m0 : m ∅ is_measurable.empty = 0)
(mU : ∀ ⦃f : ℕ → set α⦄ (hm : ∀ (i : ℕ), is_measurable (f i)), pairwise (disjoint on f) → (m (⋃ (i : ℕ), f i) _ = ∑' (i : ℕ), m (f i) _))
{s : set α} :
theorem
measure_theory.induced_outer_measure_eq
{α : Type u_1}
[measurable_space α]
{m : Π (s : set α), is_measurable s → ennreal}
(m0 : m ∅ is_measurable.empty = 0)
(mU : ∀ ⦃f : ℕ → set α⦄ (hm : ∀ (i : ℕ), is_measurable (f i)), pairwise (disjoint on f) → (m (⋃ (i : ℕ), f i) _ = ∑' (i : ℕ), m (f i) _))
{s : set α}
(hs : is_measurable s) :
⇑(measure_theory.induced_outer_measure m is_measurable.empty m0) s = m s hs
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 : is_measurable s), ⇑m s) is_measurable.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 α} :
is_measurable s → ⇑(m.trim) s = ⇑m s
theorem
measure_theory.outer_measure.trim_congr
{α : Type u_1}
[measurable_space α]
{m₁ m₂ : measure_theory.outer_measure α} :
theorem
measure_theory.outer_measure.trim_le_trim
{α : Type u_1}
[measurable_space α]
{m₁ m₂ : measure_theory.outer_measure α} :
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_add
{α : Type u_1}
[measurable_space α]
(m₁ m₂ : measure_theory.outer_measure α) :
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_is_measurable_superset_of_trim_eq_zero
{α : Type u_1}
[measurable_space α]
{m : measure_theory.outer_measure α}
{s : set α} :
theorem
measure_theory.outer_measure.trim_smul
{α : Type u_1}
[measurable_space α]
(c : ennreal)
(m : measure_theory.outer_measure α) :