Try doing some basic maths questions in the Lean Theorem Prover. Functions, real numbers, equivalence relations and groups. Click on README.md and then on "Open in CoCalc with one click".
License: APACHE
/-
Copyright (c) 2017 Johannes Hölzl. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johannes Hölzl, Mario Carneiro
-/
import data.set.lattice data.set.finite
import topology.instances.ennreal
measure_theory.outer_measure
/-!
# Measure spaces
Measures are restricted to a measurable space (associated by the type class `measurable_space`).
This allows us to prove equalities between measures by restricting to a generating set of the
measurable space.
On the other hand, the `μ.measure s` projection (i.e. the measure of `s` on the measure space `μ`)
is the _outer_ measure generated by `μ`. This gives us a unrestricted monotonicity rule and it is
somehow well-behaved on non-measurable sets.
This allows us for the `lebesgue` measure space to have the `borel` measurable space, but still be
a complete measure.
-/
noncomputable theory
open classical set lattice filter finset function
open_locale classical topological_space
universes u v w x
namespace measure_theory
section of_measurable
parameters {α : Type*} [measurable_space α]
parameters (m : Π (s : set α), is_measurable s → ennreal)
parameters (m0 : m ∅ is_measurable.empty = 0)
include m0
/-- Measure projection which is ∞ for non-measurable sets.
`measure'` is mainly used to derive the outer measure, for the main `measure` projection. -/
def measure' (s : set α) : ennreal := ⨅ h : is_measurable s, m s h
lemma measure'_eq {s} (h : is_measurable s) : measure' s = m s h :=
by simp [measure', h]
lemma measure'_empty : measure' ∅ = 0 :=
(measure'_eq is_measurable.empty).trans m0
lemma measure'_Union_nat
{f : ℕ → set α}
(hm : ∀i, is_measurable (f i))
(mU : m (⋃i, f i) (is_measurable.Union hm) = (∑i, m (f i) (hm i))) :
measure' (⋃i, f i) = (∑i, measure' (f i)) :=
(measure'_eq _).trans $ mU.trans $
by congr; funext i; rw measure'_eq
/-- outer measure of a measure -/
def outer_measure' : outer_measure α :=
outer_measure.of_function measure' measure'_empty
lemma measure'_Union_le_tsum_nat'
(mU : ∀ {f : ℕ → set α} (hm : ∀i, is_measurable (f i)),
m (⋃i, f i) (is_measurable.Union hm) ≤ (∑i, m (f i) (hm i)))
(s : ℕ → set α) :
measure' (⋃i, s i) ≤ (∑i, measure' (s i)) :=
begin
by_cases h : ∀i, is_measurable (s i),
{ rw [measure'_eq _ _ (is_measurable.Union h),
congr_arg tsum _], {apply mU h},
funext i, apply measure'_eq _ _ (h i) },
{ cases not_forall.1 h with i hi,
exact le_trans (le_infi $ λ h, hi.elim h) (ennreal.le_tsum i) }
end
parameter (mU : ∀ {f : ℕ → set α} (hm : ∀i, is_measurable (f i)),
pairwise (disjoint on f) →
m (⋃i, f i) (is_measurable.Union hm) = (∑i, m (f i) (hm i)))
include mU
lemma measure'_Union
{β} [encodable β] {f : β → set α}
(hd : pairwise (disjoint on f)) (hm : ∀i, is_measurable (f i)) :
measure' (⋃i, f i) = (∑i, measure' (f i)) :=
begin
rw [encodable.Union_decode2, outer_measure.Union_aux],
{ exact measure'_Union_nat _ _
(λ n, encodable.Union_decode2_cases is_measurable.empty hm)
(mU _ (measurable_space.Union_decode2_disjoint_on hd)) },
{ apply measure'_empty },
end
lemma measure'_union {s₁ s₂ : set α}
(hd : disjoint s₁ s₂) (h₁ : is_measurable s₁) (h₂ : is_measurable s₂) :
measure' (s₁ ∪ s₂) = measure' s₁ + measure' s₂ :=
begin
rw [union_eq_Union, measure'_Union _ _ @mU
(pairwise_disjoint_on_bool.2 hd) (bool.forall_bool.2 ⟨h₂, h₁⟩),
tsum_fintype],
change _+_ = _, simp
end
lemma measure'_mono {s₁ s₂ : set α} (h₁ : is_measurable s₁) (hs : s₁ ⊆ s₂) :
measure' s₁ ≤ measure' s₂ :=
le_infi $ λ h₂, begin
have := measure'_union _ _ @mU disjoint_diff h₁ (h₂.diff h₁),
rw union_diff_cancel hs at this,
rw ← measure'_eq m m0 _,
exact le_iff_exists_add.2 ⟨_, this⟩
end
lemma measure'_Union_le_tsum_nat : ∀ (s : ℕ → set α),
measure' (⋃i, s i) ≤ (∑i, measure' (s i)) :=
measure'_Union_le_tsum_nat' $ λ f h, begin
simp [Union_disjointed.symm] {single_pass := tt},
rw [mU (is_measurable.disjointed h) disjoint_disjointed],
refine ennreal.tsum_le_tsum (λ i, _),
rw [← measure'_eq m m0, ← measure'_eq m m0],
exact measure'_mono _ _ @mU (is_measurable.disjointed h _) (inter_subset_left _ _)
end
lemma outer_measure'_eq {s : set α} (hs : is_measurable s) :
outer_measure' s = m s hs :=
by rw ← measure'_eq m m0 hs; exact
(le_antisymm (outer_measure.of_function_le _ _ _) $
le_infi $ λ f, le_infi $ λ hf,
le_trans (measure'_mono _ _ @mU hs hf) $
measure'_Union_le_tsum_nat _ _ @mU _)
lemma outer_measure'_eq_measure' {s : set α} (hs : is_measurable s) :
outer_measure' s = measure' s :=
by rw [measure'_eq m m0 hs, outer_measure'_eq m m0 @mU hs]
end of_measurable
namespace outer_measure
variables {α : Type*} [measurable_space α] (m : outer_measure α)
def trim : outer_measure α :=
outer_measure' (λ s _, m s) m.empty
theorem trim_ge : m ≤ m.trim :=
λ s, le_infi $ λ f, le_infi $ λ hs,
le_trans (m.mono hs) $ le_trans (m.Union_nat f) $
ennreal.tsum_le_tsum $ λ i, le_infi $ λ hf, le_refl _
theorem trim_eq {s : set α} (hs : is_measurable s) : m.trim s = m s :=
le_antisymm (le_trans (of_function_le _ _ _) (infi_le _ hs)) (trim_ge _ _)
theorem trim_congr {m₁ m₂ : outer_measure α}
(H : ∀ {s : set α}, is_measurable s → m₁ s = m₂ s) :
m₁.trim = m₂.trim :=
by unfold trim; congr; funext s hs; exact H hs
theorem trim_le_trim {m₁ m₂ : outer_measure α} (H : m₁ ≤ m₂) : m₁.trim ≤ m₂.trim :=
λ s, infi_le_infi $ λ f, infi_le_infi $ λ hs,
ennreal.tsum_le_tsum $ λ b, infi_le_infi $ λ hf, H _
theorem le_trim_iff {m₁ m₂ : outer_measure α} : m₁ ≤ m₂.trim ↔
∀ s, is_measurable s → m₁ s ≤ m₂ s :=
le_of_function.trans $ forall_congr $ λ s, le_infi_iff
theorem trim_eq_infi (s : set α) : m.trim s = ⨅ t (st : s ⊆ t) (ht : is_measurable t), m t :=
begin
refine le_antisymm
(le_infi $ λ t, le_infi $ λ st, le_infi $ λ ht, _)
(le_infi $ λ f, le_infi $ λ hf, _),
{ rw ← trim_eq m ht, exact (trim m).mono st },
{ by_cases h : ∀i, is_measurable (f i),
{ refine infi_le_of_le _ (infi_le_of_le hf $
infi_le_of_le (is_measurable.Union h) _),
rw congr_arg tsum _, {exact m.Union_nat _},
funext i, exact measure'_eq _ _ (h i) },
{ cases not_forall.1 h with i hi,
exact le_trans (le_infi $ λ h, hi.elim h) (ennreal.le_tsum i) } }
end
theorem trim_eq_infi' (s : set α) : m.trim s = ⨅ t : {t // s ⊆ t ∧ is_measurable t}, m t.1 :=
by simp [infi_subtype, infi_and, trim_eq_infi]
theorem trim_trim (m : outer_measure α) : m.trim.trim = m.trim :=
le_antisymm (le_trim_iff.2 $ λ s hs, by simp [trim_eq _ hs, le_refl]) (trim_ge _)
theorem trim_zero : (0 : outer_measure α).trim = 0 :=
ext $ λ s, le_antisymm
(le_trans ((trim 0).mono (subset_univ s)) $
le_of_eq $ trim_eq _ is_measurable.univ)
(zero_le _)
theorem trim_add (m₁ m₂ : outer_measure α) : (m₁ + m₂).trim = m₁.trim + m₂.trim :=
ext $ λ s, begin
simp [trim_eq_infi'],
rw ennreal.infi_add_infi,
rintro ⟨t₁, st₁, ht₁⟩ ⟨t₂, st₂, ht₂⟩,
exact ⟨⟨_, subset_inter_iff.2 ⟨st₁, st₂⟩, ht₁.inter ht₂⟩,
add_le_add'
(m₁.mono' (inter_subset_left _ _))
(m₂.mono' (inter_subset_right _ _))⟩,
end
theorem trim_sum_ge {ι} (m : ι → outer_measure α) : sum (λ i, (m i).trim) ≤ (sum m).trim :=
λ s, by simp [trim_eq_infi]; exact
λ t st ht, ennreal.tsum_le_tsum (λ i,
infi_le_of_le t $ infi_le_of_le st $ infi_le _ ht)
end outer_measure
structure measure (α : Type*) [measurable_space α] extends outer_measure α :=
(m_Union {f : ℕ → set α} :
(∀i, is_measurable (f i)) → pairwise (disjoint on f) →
measure_of (⋃i, f i) = (∑i, measure_of (f i)))
(trimmed : to_outer_measure.trim = to_outer_measure)
/-- Measure projections for a measure space.
For measurable sets this returns the measure assigned by the `measure_of` field in `measure`.
But we can extend this to _all_ sets, but using the outer measure. This gives us monotonicity and
subadditivity for all sets.
-/
instance measure.has_coe_to_fun {α} [measurable_space α] : has_coe_to_fun (measure α) :=
⟨λ _, set α → ennreal, λ m, m.to_outer_measure⟩
namespace measure
def of_measurable {α} [measurable_space α]
(m : Π (s : set α), is_measurable s → ennreal)
(m0 : m ∅ is_measurable.empty = 0)
(mU : ∀ {f : ℕ → set α} (h : ∀i, is_measurable (f i)),
pairwise (disjoint on f) →
m (⋃i, f i) (is_measurable.Union h) = (∑i, m (f i) (h i))) :
measure α :=
{ m_Union := λ f hf hd,
show outer_measure' m m0 (Union f) =
∑ i, outer_measure' m m0 (f i), begin
rw [outer_measure'_eq m m0 @mU, mU hf hd],
congr, funext n, rw outer_measure'_eq m m0 @mU
end,
trimmed :=
show (outer_measure' m m0).trim = outer_measure' m m0, begin
unfold outer_measure.trim,
congr, funext s hs,
exact outer_measure'_eq m m0 @mU hs
end,
..outer_measure' m m0 }
lemma of_measurable_apply {α} [measurable_space α]
{m : Π (s : set α), is_measurable s → ennreal}
{m0 : m ∅ is_measurable.empty = 0}
{mU : ∀ {f : ℕ → set α} (h : ∀i, is_measurable (f i)),
pairwise (disjoint on f) →
m (⋃i, f i) (is_measurable.Union h) = (∑i, m (f i) (h i))}
(s : set α) (hs : is_measurable s) :
of_measurable m m0 @mU s = m s hs :=
outer_measure'_eq m m0 @mU hs
@[ext] lemma ext {α} [measurable_space α] :
∀ {μ₁ μ₂ : measure α}, (∀s, is_measurable s → μ₁ s = μ₂ s) → μ₁ = μ₂
| ⟨m₁, u₁, h₁⟩ ⟨m₂, u₂, h₂⟩ h := by congr; rw [← h₁, ← h₂];
exact outer_measure.trim_congr h
end measure
section
variables {α : Type*} {β : Type*} [measurable_space α] {μ μ₁ μ₂ : measure α} {s s₁ s₂ : set α}
@[simp] lemma to_outer_measure_apply (s) : μ.to_outer_measure s = μ s := rfl
lemma measure_eq_trim (s) : μ s = μ.to_outer_measure.trim s :=
by rw μ.trimmed; refl
lemma measure_eq_infi (s) : μ s = ⨅ t (st : s ⊆ t) (ht : is_measurable t), μ t :=
by rw [measure_eq_trim, outer_measure.trim_eq_infi]; refl
lemma measure_eq_outer_measure' :
μ s = outer_measure' (λ s _, μ s) μ.empty s :=
measure_eq_trim _
lemma to_outer_measure_eq_outer_measure' :
μ.to_outer_measure = outer_measure' (λ s _, μ s) μ.empty :=
μ.trimmed.symm
lemma measure_eq_measure' (hs : is_measurable s) :
μ s = measure' (λ s _, μ s) μ.empty s :=
by rw [measure_eq_outer_measure',
outer_measure'_eq_measure' (λ s _, μ s) _ μ.m_Union hs]
@[simp] lemma measure_empty : μ ∅ = 0 := μ.empty
lemma measure_mono (h : s₁ ⊆ s₂) : μ s₁ ≤ μ s₂ := μ.mono h
lemma measure_mono_null (h : s₁ ⊆ s₂) (h₂ : μ s₂ = 0) : μ s₁ = 0 :=
by rw [← le_zero_iff_eq, ← h₂]; exact measure_mono h
lemma exists_is_measurable_superset_of_measure_eq_zero {s : set α} (h : μ s = 0) :
∃t, s ⊆ t ∧ is_measurable t ∧ μ t = 0 :=
begin
rw [measure_eq_infi] at h,
have h := (infi_eq_bot _).1 h,
choose t ht using show ∀n:ℕ, ∃t, s ⊆ t ∧ is_measurable t ∧ μ t < n⁻¹,
{ assume n,
have : (0 : ennreal) < n⁻¹ :=
(zero_lt_iff_ne_zero.2 $ ennreal.inv_ne_zero.2 $ ennreal.nat_ne_top _),
rcases h _ this with ⟨t, ht⟩,
use [t],
simpa [(>), infi_lt_iff, -add_comm] using ht },
refine ⟨⋂n, t n, subset_Inter (λn, (ht n).1), is_measurable.Inter (λn, (ht n).2.1), _⟩,
refine eq_of_le_of_forall_le_of_dense bot_le (assume r hr, _),
rcases ennreal.exists_inv_nat_lt (ne_of_gt hr) with ⟨n, hn⟩,
calc μ (⋂n, t n) ≤ μ (t n) : measure_mono (Inter_subset _ _)
... ≤ n⁻¹ : le_of_lt (ht n).2.2
... ≤ r : le_of_lt hn
end
theorem measure_Union_le {β} [encodable β] (s : β → set α) : μ (⋃i, s i) ≤ (∑i, μ (s i)) :=
μ.to_outer_measure.Union _
lemma measure_Union_null {β} [encodable β] {s : β → set α} :
(∀ i, μ (s i) = 0) → μ (⋃i, s i) = 0 :=
μ.to_outer_measure.Union_null
theorem measure_union_le (s₁ s₂ : set α) : μ (s₁ ∪ s₂) ≤ μ s₁ + μ s₂ :=
μ.to_outer_measure.union _ _
lemma measure_union_null {s₁ s₂ : set α} : μ s₁ = 0 → μ s₂ = 0 → μ (s₁ ∪ s₂) = 0 :=
μ.to_outer_measure.union_null
lemma measure_Union {β} [encodable β] {f : β → set α}
(hn : pairwise (disjoint on f)) (h : ∀i, is_measurable (f i)) :
μ (⋃i, f i) = (∑i, μ (f i)) :=
by rw [measure_eq_measure' (is_measurable.Union h),
measure'_Union (λ s _, μ s) _ μ.m_Union hn h];
simp [measure_eq_measure', h]
lemma measure_union (hd : disjoint s₁ s₂) (h₁ : is_measurable s₁) (h₂ : is_measurable s₂) :
μ (s₁ ∪ s₂) = μ s₁ + μ s₂ :=
by rw [measure_eq_measure' (h₁.union h₂),
measure'_union (λ s _, μ s) _ μ.m_Union hd h₁ h₂];
simp [measure_eq_measure', h₁, h₂]
lemma measure_bUnion {s : set β} {f : β → set α} (hs : countable s)
(hd : pairwise_on s (disjoint on f)) (h : ∀b∈s, is_measurable (f b)) :
μ (⋃b∈s, f b) = ∑p:s, μ (f p.1) :=
begin
haveI := hs.to_encodable,
rw [← measure_Union, bUnion_eq_Union],
{ rintro ⟨i, hi⟩ ⟨j, hj⟩ ij x ⟨h₁, h₂⟩,
exact hd i hi j hj (mt subtype.eq' ij:_) ⟨h₁, h₂⟩ },
{ simpa }
end
lemma measure_sUnion {S : set (set α)} (hs : countable S)
(hd : pairwise_on S disjoint) (h : ∀s∈S, is_measurable s) :
μ (⋃₀ S) = ∑s:S, μ s.1 :=
by rw [sUnion_eq_bUnion, measure_bUnion hs hd h]
lemma measure_diff {s₁ s₂ : set α} (h : s₂ ⊆ s₁)
(h₁ : is_measurable s₁) (h₂ : is_measurable s₂)
(h_fin : μ s₂ < ⊤) : μ (s₁ \ s₂) = μ s₁ - μ s₂ :=
begin
refine (ennreal.add_sub_self' h_fin).symm.trans _,
rw [← measure_union disjoint_diff h₂ (h₁.diff h₂), union_diff_cancel h]
end
lemma measure_Union_eq_supr_nat {s : ℕ → set α} (h : ∀i, is_measurable (s i)) (hs : monotone s) :
μ (⋃i, s i) = (⨆i, μ (s i)) :=
begin
refine le_antisymm _ (supr_le $ λ i, measure_mono $ subset_Union _ _),
rw [← Union_disjointed,
measure_Union disjoint_disjointed (is_measurable.disjointed h),
ennreal.tsum_eq_supr_nat],
refine supr_le (λ n, _),
cases n, {apply zero_le _},
suffices : sum (finset.range n.succ) (λ i, μ (disjointed s i)) = μ (s n),
{ rw this, exact le_supr _ n },
rw [← Union_disjointed_of_mono hs, measure_Union, tsum_eq_sum],
{ apply sum_congr rfl, intros i hi,
simp [finset.mem_range.1 hi] },
{ intros i hi, simp [mt finset.mem_range.2 hi] },
{ rintro i j ij x ⟨⟨_, ⟨_, rfl⟩, h₁⟩, ⟨_, ⟨_, rfl⟩, h₂⟩⟩,
exact disjoint_disjointed i j ij ⟨h₁, h₂⟩ },
{ intro i,
by_cases h' : i < n.succ; simp [h', is_measurable.empty],
apply is_measurable.disjointed h }
end
lemma measure_Inter_eq_infi_nat {s : ℕ → set α}
(h : ∀i, is_measurable (s i)) (hs : ∀i j, i ≤ j → s j ⊆ s i)
(hfin : ∃i, μ (s i) < ⊤) :
μ (⋂i, s i) = (⨅i, μ (s i)) :=
begin
rcases hfin with ⟨k, hk⟩,
rw [← ennreal.sub_sub_cancel (by exact hk) (infi_le _ k),
ennreal.sub_infi,
← ennreal.sub_sub_cancel (by exact hk) (measure_mono (Inter_subset _ k)),
← measure_diff (Inter_subset _ k) (h k) (is_measurable.Inter h)
(lt_of_le_of_lt (measure_mono (Inter_subset _ k)) hk),
diff_Inter, measure_Union_eq_supr_nat],
{ congr, funext i,
cases le_total k i with ik ik,
{ exact measure_diff (hs _ _ ik) (h k) (h i)
(lt_of_le_of_lt (measure_mono (hs _ _ ik)) hk) },
{ rw [diff_eq_empty.2 (hs _ _ ik), measure_empty,
ennreal.sub_eq_zero_of_le (measure_mono (hs _ _ ik))] } },
{ exact λ i, (h k).diff (h i) },
{ exact λ i j ij, diff_subset_diff_right (hs _ _ ij) }
end
lemma measure_eq_inter_diff {μ : measure α} {s t : set α}
(hs : is_measurable s) (ht : is_measurable t) :
μ s = μ (s ∩ t) + μ (s \ t) :=
have hd : disjoint (s ∩ t) (s \ t) := assume a ⟨⟨_, hs⟩, _, hns⟩, hns hs ,
by rw [← measure_union hd (hs.inter ht) (hs.diff ht), inter_union_diff s t]
lemma tendsto_measure_Union {μ : measure α} {s : ℕ → set α}
(hs : ∀n, is_measurable (s n)) (hm : monotone s) :
tendsto (μ ∘ s) at_top (𝓝 (μ (⋃n, s n))) :=
begin
rw measure_Union_eq_supr_nat hs hm,
exact tendsto_at_top_supr_nat (μ ∘ s) (assume n m hnm, measure_mono $ hm $ hnm)
end
lemma tendsto_measure_Inter {μ : measure α} {s : ℕ → set α}
(hs : ∀n, is_measurable (s n)) (hm : ∀n m, n ≤ m → s m ⊆ s n) (hf : ∃i, μ (s i) < ⊤) :
tendsto (μ ∘ s) at_top (𝓝 (μ (⋂n, s n))) :=
begin
rw measure_Inter_eq_infi_nat hs hm hf,
exact tendsto_at_top_infi_nat (μ ∘ s) (assume n m hnm, measure_mono $ hm _ _ $ hnm),
end
end
def outer_measure.to_measure {α} (m : outer_measure α)
[ms : measurable_space α] (h : ms ≤ m.caratheodory) :
measure α :=
measure.of_measurable (λ s _, m s) m.empty
(λ f hf hd, m.Union_eq_of_caratheodory (λ i, h _ (hf i)) hd)
lemma le_to_outer_measure_caratheodory {α} [ms : measurable_space α]
(μ : measure α) : ms ≤ μ.to_outer_measure.caratheodory :=
begin
assume s hs,
rw to_outer_measure_eq_outer_measure',
refine outer_measure.caratheodory_is_measurable (λ t, le_infi $ λ ht, _),
rw [← measure_eq_measure' (ht.inter hs),
← measure_eq_measure' (ht.diff hs),
← measure_union _ (ht.inter hs) (ht.diff hs),
inter_union_diff],
exact le_refl _,
exact λ x ⟨⟨_, h₁⟩, _, h₂⟩, h₂ h₁
end
lemma to_measure_to_outer_measure {α} (m : outer_measure α)
[ms : measurable_space α] (h : ms ≤ m.caratheodory) :
(m.to_measure h).to_outer_measure = m.trim := rfl
@[simp] lemma to_measure_apply {α} (m : outer_measure α)
[ms : measurable_space α] (h : ms ≤ m.caratheodory)
{s : set α} (hs : is_measurable s) :
m.to_measure h s = m s := m.trim_eq hs
lemma to_outer_measure_to_measure {α : Type*} [ms : measurable_space α] {μ : measure α} :
μ.to_outer_measure.to_measure (le_to_outer_measure_caratheodory _) = μ :=
measure.ext $ λ s, μ.to_outer_measure.trim_eq
namespace measure
variables {α : Type*} {β : Type*} {γ : Type*}
[measurable_space α] [measurable_space β] [measurable_space γ]
instance : has_zero (measure α) :=
⟨{ to_outer_measure := 0,
m_Union := λ f hf hd, tsum_zero.symm,
trimmed := outer_measure.trim_zero }⟩
@[simp] theorem zero_to_outer_measure :
(0 : measure α).to_outer_measure = 0 := rfl
@[simp] theorem zero_apply (s : set α) : (0 : measure α) s = 0 := rfl
instance : inhabited (measure α) := ⟨0⟩
instance : has_add (measure α) :=
⟨λμ₁ μ₂, {
to_outer_measure := μ₁.to_outer_measure + μ₂.to_outer_measure,
m_Union := λs hs hd,
show μ₁ (⋃ i, s i) + μ₂ (⋃ i, s i) = ∑ i, μ₁ (s i) + μ₂ (s i),
by rw [ennreal.tsum_add, measure_Union hd hs, measure_Union hd hs],
trimmed := by rw [outer_measure.trim_add, μ₁.trimmed, μ₂.trimmed] }⟩
@[simp] theorem add_to_outer_measure (μ₁ μ₂ : measure α) :
(μ₁ + μ₂).to_outer_measure = μ₁.to_outer_measure + μ₂.to_outer_measure := rfl
@[simp] theorem add_apply (μ₁ μ₂ : measure α) (s : set α) :
(μ₁ + μ₂) s = μ₁ s + μ₂ s := rfl
instance add_comm_monoid : add_comm_monoid (measure α) :=
{ zero := 0,
add := (+),
add_assoc := assume a b c, ext $ assume s hs, add_assoc _ _ _,
add_comm := assume a b, ext $ assume s hs, add_comm _ _,
zero_add := assume a, ext $ assume s hs, zero_add _,
add_zero := assume a, ext $ assume s hs, add_zero _ }
instance : partial_order (measure α) :=
{ le := λm₁ m₂, ∀ s, is_measurable s → m₁ s ≤ m₂ s,
le_refl := assume m s hs, le_refl _,
le_trans := assume m₁ m₂ m₃ h₁ h₂ s hs, le_trans (h₁ s hs) (h₂ s hs),
le_antisymm := assume m₁ m₂ h₁ h₂, ext $
assume s hs, le_antisymm (h₁ s hs) (h₂ s hs) }
theorem le_iff {μ₁ μ₂ : measure α} :
μ₁ ≤ μ₂ ↔ ∀ s, is_measurable s → μ₁ s ≤ μ₂ s := iff.rfl
theorem to_outer_measure_le {μ₁ μ₂ : measure α} :
μ₁.to_outer_measure ≤ μ₂.to_outer_measure ↔ μ₁ ≤ μ₂ :=
by rw [← μ₂.trimmed, outer_measure.le_trim_iff]; refl
theorem le_iff' {μ₁ μ₂ : measure α} :
μ₁ ≤ μ₂ ↔ ∀ s, μ₁ s ≤ μ₂ s :=
to_outer_measure_le.symm
section
variables {m : set (measure α)} {μ : measure α}
lemma Inf_caratheodory (s : set α) (hs : is_measurable s) :
(Inf (measure.to_outer_measure '' m)).caratheodory.is_measurable s :=
begin
rw [outer_measure.Inf_eq_of_function_Inf_gen],
refine outer_measure.caratheodory_is_measurable (assume t, _),
cases t.eq_empty_or_nonempty with ht ht, by simp [ht],
simp only [outer_measure.Inf_gen_nonempty1 _ _ ht, le_infi_iff, ball_image_iff,
to_outer_measure_apply, measure_eq_infi t],
assume μ hμ u htu hu,
have hm : ∀{s t}, s ⊆ t → outer_measure.Inf_gen (to_outer_measure '' m) s ≤ μ t,
{ assume s t hst,
rw [outer_measure.Inf_gen_nonempty2 _ _ (mem_image_of_mem _ hμ)],
refine infi_le_of_le (μ.to_outer_measure) (infi_le_of_le (mem_image_of_mem _ hμ) _),
rw [to_outer_measure_apply],
refine measure_mono hst },
rw [measure_eq_inter_diff hu hs],
refine add_le_add' (hm $ inter_subset_inter_left _ htu) (hm $ diff_subset_diff_left htu)
end
instance : has_Inf (measure α) :=
⟨λm, (Inf (to_outer_measure '' m)).to_measure $ Inf_caratheodory⟩
lemma Inf_apply {m : set (measure α)} {s : set α} (hs : is_measurable s) :
Inf m s = Inf (to_outer_measure '' m) s :=
to_measure_apply _ _ hs
private lemma Inf_le (h : μ ∈ m) : Inf m ≤ μ :=
have Inf (to_outer_measure '' m) ≤ μ.to_outer_measure := Inf_le (mem_image_of_mem _ h),
assume s hs, by rw [Inf_apply hs, ← to_outer_measure_apply]; exact this s
private lemma le_Inf (h : ∀μ' ∈ m, μ ≤ μ') : μ ≤ Inf m :=
have μ.to_outer_measure ≤ Inf (to_outer_measure '' m) :=
le_Inf $ ball_image_of_ball $ assume μ hμ, to_outer_measure_le.2 $ h _ hμ,
assume s hs, by rw [Inf_apply hs, ← to_outer_measure_apply]; exact this s
instance : has_Sup (measure α) := ⟨λs, Inf {μ' | ∀μ∈s, μ ≤ μ' }⟩
private lemma le_Sup (h : μ ∈ m) : μ ≤ Sup m := le_Inf $ assume μ' h', h' _ h
private lemma Sup_le (h : ∀μ' ∈ m, μ' ≤ μ) : Sup m ≤ μ := Inf_le h
instance : order_bot (measure α) :=
{ bot := 0, bot_le := assume a s hs, bot_le, .. measure.partial_order }
instance : order_top (measure α) :=
{ top := (⊤ : outer_measure α).to_measure (by rw [outer_measure.top_caratheodory]; exact le_top),
le_top := assume a s hs,
by cases s.eq_empty_or_nonempty with h h;
simp [h, to_measure_apply ⊤ _ hs, outer_measure.top_apply],
.. measure.partial_order }
instance : complete_lattice (measure α) :=
{ Inf := Inf,
Sup := Sup,
inf := λa b, Inf {a, b},
sup := λa b, Sup {a, b},
le_Sup := assume s μ h, le_Sup h,
Sup_le := assume s μ h, Sup_le h,
Inf_le := assume s μ h, Inf_le h,
le_Inf := assume s μ h, le_Inf h,
le_sup_left := assume a b, le_Sup $ by simp,
le_sup_right := assume a b, le_Sup $ by simp,
sup_le := assume a b c hac hbc, Sup_le $ by simp [*, or_imp_distrib] {contextual := tt},
inf_le_left := assume a b, Inf_le $ by simp,
inf_le_right := assume a b, Inf_le $ by simp,
le_inf := assume a b c hac hbc, le_Inf $ by simp [*, or_imp_distrib] {contextual := tt},
.. measure.partial_order, .. measure.lattice.order_top, .. measure.lattice.order_bot }
end
def map (f : α → β) (μ : measure α) : measure β :=
if hf : measurable f then
(μ.to_outer_measure.map f).to_measure $ λ s hs t,
le_to_outer_measure_caratheodory μ _ (hf _ hs) (f ⁻¹' t)
else 0
variables {μ ν : measure α}
@[simp] theorem map_apply {f : α → β} (hf : measurable f)
{s : set β} (hs : is_measurable s) :
(map f μ : measure β) s = μ (f ⁻¹' s) :=
by rw [map, dif_pos hf, to_measure_apply _ _ hs]; refl
@[simp] lemma map_id : map id μ = μ :=
ext $ λ s, map_apply measurable_id
lemma map_map {g : β → γ} {f : α → β} (hg : measurable g) (hf : measurable f) :
map g (map f μ) = map (g ∘ f) μ :=
ext $ λ s hs,
by simp [hf, hg, hs, hg.preimage hs, hg.comp hf];
rw ← preimage_comp
/-- The dirac measure. -/
def dirac (a : α) : measure α :=
(outer_measure.dirac a).to_measure (by simp)
@[simp] lemma dirac_apply (a : α) {s : set α} (hs : is_measurable s) :
(dirac a : measure α) s = ⨆ h : a ∈ s, 1 :=
to_measure_apply _ _ hs
/-- Sum of an indexed family of measures. -/
def sum {ι : Type*} (f : ι → measure α) : measure α :=
(outer_measure.sum (λ i, (f i).to_outer_measure)).to_measure $
le_trans
(by exact le_infi (λ i, le_to_outer_measure_caratheodory _))
(outer_measure.le_sum_caratheodory _)
/-- Counting measure on any measurable space. -/
def count : measure α := sum dirac
@[class] def is_complete {α} {_:measurable_space α} (μ : measure α) : Prop :=
∀ s, μ s = 0 → is_measurable s
/-- The "almost everywhere" filter of co-null sets. -/
def a_e (μ : measure α) : filter α :=
{ sets := {s | μ (-s) = 0},
univ_sets := by simp [measure_empty],
inter_sets := λ s t hs ht, by simp [compl_inter]; exact measure_union_null hs ht,
sets_of_superset := λ s t hs hst, measure_mono_null (set.compl_subset_compl.2 hst) hs }
lemma mem_a_e_iff (s : set α) : s ∈ μ.a_e.sets ↔ μ (- s) = 0 := iff.rfl
end measure
end measure_theory
section is_complete
open measure_theory
variables {α : Type*} [measurable_space α] (μ : measure α)
def is_null_measurable (s : set α) : Prop :=
∃ t z, s = t ∪ z ∧ is_measurable t ∧ μ z = 0
theorem is_null_measurable_iff {μ : measure α} {s : set α} :
is_null_measurable μ s ↔
∃ t, t ⊆ s ∧ is_measurable t ∧ μ (s \ t) = 0 :=
begin
split,
{ rintro ⟨t, z, rfl, ht, hz⟩,
refine ⟨t, set.subset_union_left _ _, ht, measure_mono_null _ hz⟩,
simp [union_diff_left, diff_subset] },
{ rintro ⟨t, st, ht, hz⟩,
exact ⟨t, _, (union_diff_cancel st).symm, ht, hz⟩ }
end
theorem is_null_measurable_measure_eq {μ : measure α} {s t : set α}
(st : t ⊆ s) (hz : μ (s \ t) = 0) : μ s = μ t :=
begin
refine le_antisymm _ (measure_mono st),
have := measure_union_le t (s \ t),
rw [union_diff_cancel st, hz] at this, simpa
end
theorem is_measurable.is_null_measurable
{s : set α} (hs : is_measurable s) : is_null_measurable μ s :=
⟨s, ∅, by simp, hs, μ.empty⟩
theorem is_null_measurable_of_complete [c : μ.is_complete]
{s : set α} : is_null_measurable μ s ↔ is_measurable s :=
⟨by rintro ⟨t, z, rfl, ht, hz⟩; exact
is_measurable.union ht (c _ hz),
λ h, h.is_null_measurable _⟩
variables {μ}
theorem is_null_measurable.union_null {s z : set α}
(hs : is_null_measurable μ s) (hz : μ z = 0) :
is_null_measurable μ (s ∪ z) :=
begin
rcases hs with ⟨t, z', rfl, ht, hz'⟩,
exact ⟨t, z' ∪ z, set.union_assoc _ _ _, ht, le_zero_iff_eq.1
(le_trans (measure_union_le _ _) $ by simp [hz, hz'])⟩
end
theorem null_is_null_measurable {z : set α}
(hz : μ z = 0) : is_null_measurable μ z :=
by simpa using (is_measurable.empty.is_null_measurable _).union_null hz
theorem is_null_measurable.Union_nat {s : ℕ → set α}
(hs : ∀ i, is_null_measurable μ (s i)) :
is_null_measurable μ (Union s) :=
begin
choose t ht using assume i, is_null_measurable_iff.1 (hs i),
simp [forall_and_distrib] at ht,
rcases ht with ⟨st, ht, hz⟩,
refine is_null_measurable_iff.2
⟨Union t, Union_subset_Union st, is_measurable.Union ht,
measure_mono_null _ (measure_Union_null hz)⟩,
rw [diff_subset_iff, ← Union_union_distrib],
exact Union_subset_Union (λ i, by rw ← diff_subset_iff)
end
theorem is_measurable.diff_null {s z : set α}
(hs : is_measurable s) (hz : μ z = 0) :
is_null_measurable μ (s \ z) :=
begin
rw measure_eq_infi at hz,
choose f hf using show ∀ q : {q:ℚ//q>0}, ∃ t:set α,
z ⊆ t ∧ is_measurable t ∧ μ t < (nnreal.of_real q.1 : ennreal),
{ rintro ⟨ε, ε0⟩,
have : 0 < (nnreal.of_real ε : ennreal), { simpa using ε0 },
rw ← hz at this, simpa [infi_lt_iff] },
refine is_null_measurable_iff.2 ⟨s \ Inter f,
diff_subset_diff_right (subset_Inter (λ i, (hf i).1)),
hs.diff (is_measurable.Inter (λ i, (hf i).2.1)),
measure_mono_null _ (le_zero_iff_eq.1 $ le_of_not_lt $ λ h, _)⟩,
{ exact Inter f },
{ rw [diff_subset_iff, diff_union_self],
exact subset.trans (diff_subset _ _) (subset_union_left _ _) },
rcases ennreal.lt_iff_exists_rat_btwn.1 h with ⟨ε, ε0', ε0, h⟩,
simp at ε0,
apply not_le_of_lt (lt_trans (hf ⟨ε, ε0⟩).2.2 h),
exact measure_mono (Inter_subset _ _)
end
theorem is_null_measurable.diff_null {s z : set α}
(hs : is_null_measurable μ s) (hz : μ z = 0) :
is_null_measurable μ (s \ z) :=
begin
rcases hs with ⟨t, z', rfl, ht, hz'⟩,
rw [set.union_diff_distrib],
exact (ht.diff_null hz).union_null (measure_mono_null (diff_subset _ _) hz')
end
theorem is_null_measurable.compl {s : set α}
(hs : is_null_measurable μ s) :
is_null_measurable μ (-s) :=
begin
rcases hs with ⟨t, z, rfl, ht, hz⟩,
rw compl_union,
exact ht.compl.diff_null hz
end
def null_measurable {α : Type u} [measurable_space α]
(μ : measure α) : measurable_space α :=
{ is_measurable := is_null_measurable μ,
is_measurable_empty := is_measurable.empty.is_null_measurable _,
is_measurable_compl := λ s hs, hs.compl,
is_measurable_Union := λ f, is_null_measurable.Union_nat }
def completion {α : Type u} [measurable_space α] (μ : measure α) :
@measure_theory.measure α (null_measurable μ) :=
{ to_outer_measure := μ.to_outer_measure,
m_Union := λ s hs hd, show μ (Union s) = ∑ i, μ (s i), begin
choose t ht using assume i, is_null_measurable_iff.1 (hs i),
simp [forall_and_distrib] at ht, rcases ht with ⟨st, ht, hz⟩,
rw is_null_measurable_measure_eq (Union_subset_Union st),
{ rw measure_Union _ ht,
{ congr, funext i,
exact (is_null_measurable_measure_eq (st i) (hz i)).symm },
{ rintro i j ij x ⟨h₁, h₂⟩,
exact hd i j ij ⟨st i h₁, st j h₂⟩ } },
{ refine measure_mono_null _ (measure_Union_null hz),
rw [diff_subset_iff, ← Union_union_distrib],
exact Union_subset_Union (λ i, by rw ← diff_subset_iff) }
end,
trimmed := begin
letI := null_measurable μ,
refine le_antisymm (λ s, _) (outer_measure.trim_ge _),
rw outer_measure.trim_eq_infi,
dsimp, clear _inst,
rw measure_eq_infi s,
exact infi_le_infi (λ t, infi_le_infi $ λ st,
infi_le_infi2 $ λ ht, ⟨ht.is_null_measurable _, le_refl _⟩)
end }
instance completion.is_complete {α : Type u} [measurable_space α] (μ : measure α) :
(completion μ).is_complete :=
λ z hz, null_is_null_measurable hz
end is_complete
namespace measure_theory
section prio
set_option default_priority 100 -- see Note [default priority]
/-- A measure space is a measurable space equipped with a
measure, referred to as `volume`. -/
class measure_space (α : Type*) extends measurable_space α :=
(μ {} : measure α)
end prio
section measure_space
variables {α : Type*} [measure_space α] {s₁ s₂ : set α}
open measure_space
def volume : set α → ennreal := @μ α _
@[simp] lemma volume_empty : volume (∅ : set α) = 0 := μ.empty
lemma volume_mono : s₁ ⊆ s₂ → volume s₁ ≤ volume s₂ := measure_mono
lemma volume_mono_null : s₁ ⊆ s₂ → volume s₂ = 0 → volume s₁ = 0 :=
measure_mono_null
theorem volume_Union_le {β} [encodable β] :
∀ (s : β → set α), volume (⋃i, s i) ≤ (∑i, volume (s i)) :=
measure_Union_le
lemma volume_Union_null {β} [encodable β] {s : β → set α} :
(∀ i, volume (s i) = 0) → volume (⋃i, s i) = 0 :=
measure_Union_null
theorem volume_union_le : ∀ (s₁ s₂ : set α), volume (s₁ ∪ s₂) ≤ volume s₁ + volume s₂ :=
measure_union_le
lemma volume_union_null : volume s₁ = 0 → volume s₂ = 0 → volume (s₁ ∪ s₂) = 0 :=
measure_union_null
lemma volume_Union {β} [encodable β] {f : β → set α} :
pairwise (disjoint on f) → (∀i, is_measurable (f i)) →
volume (⋃i, f i) = (∑i, volume (f i)) :=
measure_Union
lemma volume_union : disjoint s₁ s₂ → is_measurable s₁ → is_measurable s₂ →
volume (s₁ ∪ s₂) = volume s₁ + volume s₂ :=
measure_union
lemma volume_bUnion {β} {s : set β} {f : β → set α} : countable s →
pairwise_on s (disjoint on f) → (∀b∈s, is_measurable (f b)) →
volume (⋃b∈s, f b) = ∑p:s, volume (f p.1) :=
measure_bUnion
lemma volume_sUnion {S : set (set α)} : countable S →
pairwise_on S disjoint → (∀s∈S, is_measurable s) →
volume (⋃₀ S) = ∑s:S, volume s.1 :=
measure_sUnion
lemma volume_bUnion_finset {β} {s : finset β} {f : β → set α}
(hd : pairwise_on ↑s (disjoint on f)) (hm : ∀b∈s, is_measurable (f b)) :
volume (⋃b∈s, f b) = s.sum (λp, volume (f p)) :=
show volume (⋃b∈(↑s : set β), f b) = s.sum (λp, volume (f p)),
begin
rw [volume_bUnion (countable_finite (finset.finite_to_set s)) hd hm, tsum_eq_sum],
{ show s.attach.sum (λb:(↑s : set β), volume (f b)) = s.sum (λb, volume (f b)),
exact @finset.sum_attach _ _ s _ (λb, volume (f b)) },
simp
end
lemma volume_diff : s₂ ⊆ s₁ → is_measurable s₁ → is_measurable s₂ →
volume s₂ < ⊤ → volume (s₁ \ s₂) = volume s₁ - volume s₂ :=
measure_diff
/-- `∀ₘ a:α, p a` states that the property `p` is almost everywhere true in the measure space
associated with `α`. This means that the measure of the complementary of `p` is `0`.
In a probability measure, the measure of `p` is `1`, when `p` is measurable.
-/
def all_ae (p : α → Prop) : Prop :=
∀ᶠ a in μ.a_e, p a
notation `∀ₘ` binders `, ` r:(scoped P, all_ae P) := r
lemma all_ae_congr {p q : α → Prop} (h : ∀ₘ a, p a ↔ q a) : (∀ₘ a, p a) ↔ (∀ₘ a, q a) :=
iff.intro
(assume h', by filter_upwards [h, h'] assume a hpq hp, hpq.1 hp)
(assume h', by filter_upwards [h, h'] assume a hpq hq, hpq.2 hq)
lemma all_ae_iff {p : α → Prop} : (∀ₘ a, p a) ↔ volume { a | ¬ p a } = 0 := iff.rfl
lemma all_ae_of_all {p : α → Prop} : (∀a, p a) → ∀ₘ a, p a := univ_mem_sets'
lemma all_ae_all_iff {ι : Type*} [encodable ι] {p : α → ι → Prop} :
(∀ₘ a, ∀i, p a i) ↔ (∀i, ∀ₘ a, p a i) :=
begin
refine iff.intro (assume h i, _) (assume h, _),
{ filter_upwards [h] assume a ha, ha i },
{ have h := measure_Union_null h,
rw [← compl_Inter] at h,
filter_upwards [h] assume a, mem_Inter.1 }
end
variables {β : Type*}
lemma all_ae_eq_refl (f : α → β) : ∀ₘ a, f a = f a :=
by { filter_upwards [], assume a, apply eq.refl }
lemma all_ae_eq_symm {f g : α → β} : (∀ₘ a, f a = g a) → (∀ₘ a, g a = f a) :=
by { assume h, filter_upwards [h], assume a, apply eq.symm }
lemma all_ae_eq_trans {f g h: α → β} (h₁ : ∀ₘ a, f a = g a) (h₂ : ∀ₘ a, g a = h a) :
∀ₘ a, f a = h a :=
by { filter_upwards [h₁, h₂], intro a, exact eq.trans }
end measure_space
end measure_theory