feat(measure_theory): add Hahn decomposition

Author: johoelzl

src/data/real/ennreal.lean

@@ -102,6 +102,16 @@ by refine_struct {..}; simp
 lemma add_eq_top : a + b = ∞ ↔ a = ∞ ∨ b = ∞ := with_top.add_eq_top _ _
 lemma add_lt_top : a + b < ∞ ↔ a < ∞ ∧ b < ∞ := with_top.add_lt_top _ _
 
+lemma to_nnreal_add {r₁ r₂ : ennreal} (h₁ : r₁ < ⊤) (h₂ : r₂ < ⊤) :
+  (r₁ + r₂).to_nnreal = r₁.to_nnreal + r₂.to_nnreal :=
+begin
+  rw [← coe_eq_coe, coe_add, coe_to_nnreal, coe_to_nnreal, coe_to_nnreal];
+    apply @ne_top_of_lt ennreal _ _ ⊤,
+  exact h₂,
+  exact h₁,
+  exact add_lt_top.2 ⟨h₁, h₂⟩
+end
+
 /- rw has trouble with the generic lt_top_iff_ne_top and bot_lt_iff_ne_bot
 (contrary to erw). This is solved with the next lemmas -/
 protected lemma lt_top_iff_ne_top : a < ∞ ↔ a ≠ ∞ := lt_top_iff_ne_top

src/data/real/nnreal.lean

@@ -36,6 +36,8 @@ protected def of_real (r : ℝ) : ℝ≥0 := ⟨max r 0, le_max_right _ _⟩
 lemma coe_of_real (r : ℝ) (hr : 0 ≤ r) : (nnreal.of_real r : ℝ) = r :=
 max_eq_left hr
 
+lemma coe_nonneg (r : nnreal) : (0 : ℝ) ≤ r := r.2
+
 instance : has_zero ℝ≥0  := ⟨⟨0, le_refl 0⟩⟩
 instance : has_one ℝ≥0   := ⟨⟨1, zero_le_one⟩⟩
 instance : has_add ℝ≥0   := ⟨λa b, ⟨a + b, add_nonneg a.2 b.2⟩⟩

src/measure_theory/decomposition.lean

@@ -0,0 +1,194 @@
+/-
+Copyright (c) 2019 Johannes Hölzl. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johannes Hölzl
+
+Hahn decomposition theorem
+
+TODO:
+* introduce finite measures (into nnreal)
+* show general for signed measures (into ℝ)
+-/
+import measure_theory.measure_space
+
+local attribute [instance, priority 0] classical.prop_decidable
+
+namespace measure_theory
+open set lattice filter
+
+variables {α : Type*} [measurable_space α] {μ ν : measure α}
+
+lemma hahn_decomposition (hμ : μ univ < ⊤) (hν : ν univ < ⊤) :
+  ∃s, is_measurable s ∧
+    (∀t, is_measurable t → t ⊆ s → ν t ≤ μ t) ∧
+    (∀t, is_measurable t → t ⊆ - s → μ t ≤ ν t) :=
+begin
+  let d : set α → ℝ := λs, ((μ s).to_nnreal : ℝ) - (ν s).to_nnreal,
+  let c : set ℝ := d '' {s | is_measurable s },
+  let γ : ℝ := Sup c,
+
+  have hμ : ∀s, μ s < ⊤ := assume s, lt_of_le_of_lt (measure_mono $ subset_univ _) hμ,
+  have hν : ∀s, ν s < ⊤ := assume s, lt_of_le_of_lt (measure_mono $ subset_univ _) hν,
+  have to_nnreal_μ : ∀s, ((μ s).to_nnreal : ennreal) = μ s :=
+    (assume s, ennreal.coe_to_nnreal $ ne_top_of_lt $ hμ _),
+  have to_nnreal_ν : ∀s, ((ν s).to_nnreal : ennreal) = ν s :=
+    (assume s, ennreal.coe_to_nnreal $ ne_top_of_lt $ hν _),
+
+  have d_empty : d ∅ = 0, { simp [d], rw [measure_empty, measure_empty], simp },
+
+  have d_split : ∀s t, is_measurable s → is_measurable t →
+    d s = d (s \ t) + d (s ∩ t),
+  { assume s t hs ht,
+    simp only [d],
+    rw [measure_eq_inter_diff hs ht, measure_eq_inter_diff hs ht,
+      ennreal.to_nnreal_add (hμ _) (hμ _), ennreal.to_nnreal_add (hν _) (hν _),
+      nnreal.coe_add, nnreal.coe_add],
+    simp only [sub_eq_add_neg, neg_add],
+    ac_refl },
+
+  have d_Union : ∀(s : ℕ → set α), (∀n, is_measurable (s n)) → monotone s →
+    tendsto (λn, d (s n)) at_top (nhds (d (⋃n, s n))),
+  { assume s hs hm,
+    refine tendsto_sub _ _;
+      refine (nnreal.tendsto_coe.2 $
+        (tendsto_measure_Union hs hm).comp $ ennreal.tendsto_to_nnreal $ @ne_top_of_lt _ _ _ ⊤ _),
+    exact hμ _,
+    exact hν _ },
+
+  have d_Inter : ∀(s : ℕ → set α), (∀n, is_measurable (s n)) → (∀n m, n ≤ m → s m ⊆ s n) →
+    tendsto (λn, d (s n)) at_top (nhds (d (⋂n, s n))),
+  { assume s hs hm,
+    refine tendsto_sub _ _;
+      refine (nnreal.tendsto_coe.2 $
+        (tendsto_measure_Inter hs hm _).comp $ ennreal.tendsto_to_nnreal $ @ne_top_of_lt _ _ _ ⊤ _),
+    exact ⟨0, hμ _⟩,
+    exact hμ _,
+    exact ⟨0, hν _⟩,
+    exact hν _ },
+
+  have bdd_c : bdd_above c,
+  { use (μ univ).to_nnreal,
+    rintros r ⟨s, hs, rfl⟩,
+    refine le_trans (sub_le_self _ $ nnreal.coe_nonneg _) _,
+    rw [← nnreal.coe_le, ← ennreal.coe_le_coe, to_nnreal_μ, to_nnreal_μ],
+    exact measure_mono (subset_univ _) },
+
+  have c_nonempty : c ≠ ∅ := ne_empty_of_mem (mem_image_of_mem _ is_measurable.empty),
+
+  have d_le_γ : ∀s, is_measurable s → d s ≤ γ := assume s hs, le_cSup bdd_c ⟨s, hs, rfl⟩,
+
+  have : ∀n:ℕ, ∃s : set α, is_measurable s ∧ γ - (1/2)^n < d s,
+  { assume n,
+    have : γ - (1/2)^n < γ := sub_lt_self γ (pow_pos (half_pos zero_lt_one) n),
+    rcases exists_lt_of_lt_cSup c_nonempty this with ⟨r, ⟨s, hs, rfl⟩, hlt⟩,
+    exact ⟨s, hs, hlt⟩ },
+  rcases classical.axiom_of_choice this with ⟨e, he⟩,
+  change ℕ → set α at e,
+  have he₁ : ∀n, is_measurable (e n) := assume n, (he n).1,
+  have he₂ : ∀n, γ - (1/2)^n < d (e n) := assume n, (he n).2,
+
+  let f : ℕ → ℕ → set α := λn m, (finset.Ico n (m + 1)).inf e,
+
+  have hf : ∀n m, is_measurable (f n m),
+  { assume n m,
+    simp only [f, finset.inf_eq_infi],
+    exact is_measurable.bInter (countable_encodable _) (assume i _, he₁ _) },
+
+  have f_subset_f : ∀{a b c d}, a ≤ b → c ≤ d → f a d ⊆ f b c,
+  { assume a b c d hab hcd,
+    dsimp only [f],
+    rw [finset.inf_eq_infi, finset.inf_eq_infi],
+    refine bInter_subset_bInter_left _,
+    simp,
+    rintros j ⟨hbj, hjc⟩,
+    exact ⟨le_trans hab hbj, lt_of_lt_of_le hjc $ add_le_add_right hcd 1⟩ },
+
+  have f_succ : ∀n m, n ≤ m → f n (m + 1) = f n m ∩ e (m + 1),
+  { assume n m hnm,
+    have : n ≤ m + 1 := le_of_lt (nat.succ_le_succ hnm),
+    simp only [f],
+    rw [finset.Ico.succ_top this, finset.inf_insert, set.inter_comm],
+    refl },
+
+  have le_d_f : ∀n m, m ≤ n → γ - 2 * ((1 / 2) ^ m) + (1 / 2) ^ n ≤ d (f m n),
+  { assume n m h,
+    refine nat.le_induction _ _ n h,
+    { have := he₂ m,
+      simp only [f],
+      rw [finset.Ico.succ_singleton, finset.inf_singleton],
+      linarith },
+    { assume n (hmn : m ≤ n) ih,
+      have : γ + (γ - 2 * (1 / 2)^m + (1 / 2) ^ (n + 1)) ≤ γ + d (f m (n + 1)),
+      { calc γ + (γ - 2 * (1 / 2)^m + (1 / 2) ^ (n+1)) ≤
+            γ + (γ - 2 * (1 / 2)^m + ((1 / 2) ^ n - (1/2)^(n+1))) :
+          begin
+            refine add_le_add_left (add_le_add_left _ _) γ,
+            simp only [pow_add, pow_one, le_sub_iff_add_le],
+            linarith
+          end
+          ... = (γ - (1 / 2)^(n+1)) + (γ - 2 * (1 / 2)^m + (1 / 2)^n) :
+            by simp only [sub_eq_add_neg]; ac_refl
+          ... ≤ d (e (n + 1)) + d (f m n) : add_le_add (le_of_lt $ he₂ _) ih
+          ... ≤ d (e (n + 1)) + d (f m n \ e (n + 1)) + d (f m (n + 1)) :
+            by rw [f_succ _ _ hmn, d_split (f m n) (e (n + 1)) (hf _ _) (he₁ _), add_assoc]
+          ... = d (e (n + 1) ∪ f m n) + d (f m (n + 1)) :
+            begin
+              rw [d_split (e (n + 1) ∪ f m n) (e (n + 1)),
+                union_diff_left, union_inter_cancel_left],
+              ac_refl,
+              exact (he₁ _).union (hf _ _),
+              exact (he₁ _)
+            end
+          ... ≤ γ + d (f m (n + 1)) :
+            add_le_add_right (d_le_γ _ $ (he₁ _).union (hf _ _)) _ },
+      exact (add_le_add_iff_left γ).1 this } },
+
+  let s := ⋃ m, ⋂n, f m n,
+  have γ_le_d_s : γ ≤ d s,
+  { have hγ : tendsto (λm:ℕ, γ - 2 * (1/2)^m) at_top (nhds γ),
+    { suffices : tendsto (λm:ℕ, γ - 2 * (1/2)^m) at_top (nhds (γ - 2 * 0)), { simpa },
+      exact (tendsto_sub tendsto_const_nhds $ tendsto_mul tendsto_const_nhds $
+        tendsto_pow_at_top_nhds_0_of_lt_1
+          (le_of_lt $ half_pos $ zero_lt_one) (half_lt_self zero_lt_one)) },
+    have hd : tendsto (λm, d (⋂n, f m n)) at_top (nhds (d (⋃ m, ⋂ n, f m n))),
+    { refine d_Union _ _ _,
+      { assume n, exact is_measurable.Inter (assume m, hf _ _) },
+      { exact assume n m hnm, subset_Inter
+          (assume i, subset.trans (Inter_subset (f n) i) $ f_subset_f hnm $ le_refl _) } },
+    refine le_of_tendsto_of_tendsto (@at_top_ne_bot ℕ _ _) hγ hd (univ_mem_sets' $ assume m, _),
+    change γ - 2 * (1 / 2) ^ m ≤ d (⋂ (n : ℕ), f m n),
+    have : tendsto (λn, d (f m n)) at_top (nhds (d (⋂ n, f m n))),
+    { refine d_Inter _ _ _,
+      { assume n, exact hf _ _ },
+      { assume n m hnm, exact f_subset_f (le_refl _) hnm } },
+    refine ge_of_tendsto (@at_top_ne_bot ℕ _ _) this (mem_at_top_sets.2 ⟨m, assume n hmn, _⟩),
+    change γ - 2 * (1 / 2) ^ m ≤ d (f m n),
+    refine le_trans _ (le_d_f _ _ hmn),
+    exact le_add_of_le_of_nonneg (le_refl _) (pow_nonneg (le_of_lt $ half_pos $ zero_lt_one) _) },
+
+  have hs : is_measurable s :=
+    is_measurable.Union (assume n, is_measurable.Inter (assume m, hf _ _)),
+  refine ⟨s, hs, _, _⟩,
+  { assume t ht hts,
+    have : 0 ≤ d t := ((add_le_add_iff_left γ).1 $
+      calc γ + 0 ≤ d s : by rw [add_zero]; exact γ_le_d_s
+        ... = d (s \ t) + d t : by rw [d_split _ _ hs ht, inter_eq_self_of_subset_right hts]
+        ... ≤ γ + d t : add_le_add (d_le_γ _ (hs.diff ht)) (le_refl _)),
+    rw [← to_nnreal_μ, ← to_nnreal_ν, ennreal.coe_le_coe, nnreal.coe_le],
+    simpa only [d, le_sub_iff_add_le, zero_add] using this },
+  { assume t ht hts,
+    have : d t ≤ 0,
+    exact ((add_le_add_iff_left γ).1 $
+      calc γ + d t ≤ d s + d t : add_le_add γ_le_d_s (le_refl _)
+        ... = d (s ∪ t) :
+        begin
+          rw [d_split _ _ (hs.union ht) ht, union_diff_right, union_inter_cancel_right,
+            diff_eq_self.2],
+          exact assume a ⟨hat, has⟩, hts hat has
+        end
+        ... ≤ γ + 0 : by rw [add_zero]; exact d_le_γ _ (hs.union ht)),
+    rw [← to_nnreal_μ, ← to_nnreal_ν, ennreal.coe_le_coe, nnreal.coe_le],
+    simpa only [d, sub_le_iff_le_add, zero_add] using this }
+end
+
+end measure_theory

src/measure_theory/measure_space.lean

@@ -26,6 +26,26 @@ local attribute [instance] prop_decidable
 
 universes u v w x
 
+section tendsto
+variables {α : Type*} [topological_space α]
+open lattice filter
+
+lemma tendsto_at_top_supr_nat [complete_linear_order α] [orderable_topology α]
+  (f : ℕ → α) (hf : monotone f) : tendsto f at_top (nhds (⨆i, f i)) :=
+tendsto_orderable.2 $ and.intro
+  (assume a ha, let ⟨n, hn⟩ := lt_supr_iff.1 ha in
+    mem_at_top_sets.2 ⟨n, assume i hi, lt_of_lt_of_le hn (hf hi)⟩)
+  (assume a ha, univ_mem_sets' (assume n, lt_of_le_of_lt (le_supr _ n) ha))
+
+lemma tendsto_at_top_infi_nat [complete_linear_order α] [orderable_topology α]
+  (f : ℕ → α) (hf : ∀{n m}, n ≤ m → f m ≤ f n) : tendsto f at_top (nhds (⨅i, f i)) :=
+tendsto_orderable.2 $ and.intro
+  (assume a ha, univ_mem_sets' (assume n, lt_of_lt_of_le ha (infi_le _ _)))
+  (assume a ha, let ⟨n, hn⟩ := infi_lt_iff.1 ha in
+    mem_at_top_sets.2 ⟨n, assume i hi, lt_of_le_of_lt (hf hi) hn⟩)
+
+end tendsto
+
 namespace measure_theory
 
 section of_measurable
@@ -383,6 +403,28 @@ begin
   { 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 (nhds (μ (⋃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 (nhds (μ (⋂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 α)
@@ -486,14 +528,13 @@ begin
   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 hd : disjoint (u ∩ s) (u \ s) := assume a ⟨⟨_, hs⟩, _, hns⟩, hns hs ,
   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 [← inter_union_diff u s, measure_union hd (hu.inter hs) (hu.diff hs)],
+  rw [measure_eq_inter_diff hu hs],
   refine add_le_add' (hm $ inter_subset_inter_left _ htu) (hm $ diff_subset_diff_left htu)
 end
 
@@ -551,7 +592,7 @@ if hf : measurable f then
   le_to_outer_measure_caratheodory μ _ (hf _ hs) (f ⁻¹' t)
 else 0
 
-variable {μ : measure α}
+variables {μ ν : measure α}
 
 @[simp] theorem map_apply {f : α → β} (hf : measurable f)
   {s : set β} (hs : is_measurable s) :