feat(measure_theory): integral is equal and monotone almost-everywher…

…e and for measurable functions it is a.e. strict at 0

src/measure_theory/integration.lean

@@ -732,6 +732,56 @@ begin
   congr; ext a; by_cases a ∈ s; simp [h, hs]
 end
 
+lemma lintegral_le_lintegral_ae {f g : α → ennreal} (h : ∀ₘ a, f a ≤ g a) :
+  (∫⁻ a, f a) ≤ (∫⁻ a, g a) :=
+begin
+  rcases exists_is_measurable_superset_of_measure_eq_zero h with ⟨t, hts, ht, ht0⟩,
+  have : - t ∈ (@measure_space.μ α _).a_e.sets,
+  { rw [measure.mem_a_e_iff, lattice.neg_neg, ht0] },
+  refine (supr_le $ assume s, supr_le $ assume hfs,
+    le_supr_of_le (s.restrict (- t)) $ le_supr_of_le _ _),
+  { assume a,
+    by_cases a ∈ t;
+      simp [h, simple_func.restrict_apply, ht.compl],
+    exact le_trans (hfs a) (by_contradiction $ assume hnfg, h (hts hnfg)) },
+  { refine le_of_eq (s.integral_congr _ _),
+    filter_upwards [this],
+    refine assume a hnt, _,
+    by_cases hat : a ∈ t; simp [hat, ht.compl],
+    exact (hnt hat).elim }
+end
+
+lemma lintegral_congr_ae {f g : α → ennreal} (h : ∀ₘ a, f a = g a) :
+  (∫⁻ a, f a) = (∫⁻ a, g a) :=
+le_antisymm
+  (lintegral_le_lintegral_ae $ by filter_upwards [h] assume a h, le_of_eq h)
+  (lintegral_le_lintegral_ae $ by filter_upwards [h] assume a h, le_of_eq h.symm)
+
+lemma lintegral_eq_zero_iff {f : α → ennreal} (hf : measurable f) :
+  lintegral f = 0 ↔ (∀ₘ a, f a = 0) :=
+begin
+  refine iff.intro (assume h, _) (assume h, _),
+  { have : ∀n:ℕ, ∀ₘ a, f a < n⁻¹,
+    { assume n,
+      have : is_measurable {a : α | f a ≥ n⁻¹ },
+      { exact hf _ (is_measurable_of_is_closed $ is_closed_ge' _) },
+      have : (n : ennreal)⁻¹ * volume {a | f a ≥ n⁻¹ } = 0,
+      { rw [← simple_func.restrict_const_integral _ _ this, ← le_zero_iff_eq,
+          ← simple_func.lintegral_eq_integral],
+        refine le_trans (lintegral_le_lintegral _ _ _) (le_of_eq h),
+        assume a, by_cases h : (n : ennreal)⁻¹ ≤ f a; simp [h, (≥), this] },
+      rw [ennreal.mul_eq_zero, ennreal.inv_eq_zero] at this,
+      simpa [ennreal.nat_ne_top, all_ae_iff] using this },
+    filter_upwards [all_ae_all_iff.2 this],
+    dsimp,
+    assume a ha,
+    by_contradiction h,
+    rcases ennreal.exists_inv_nat_lt h with ⟨n, hn⟩,
+    exact (lt_irrefl _ $ lt_trans hn $ ha n).elim },
+  { calc lintegral f = lintegral (λa:α, 0) : lintegral_congr_ae h
+      ... = 0 : lintegral_zero }
+end
+
 section
 open encodable
 

src/measure_theory/measure_space.lean

@@ -309,6 +309,26 @@ 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 _
 
@@ -636,6 +656,8 @@ def a_e (μ : measure α) : filter α :=
   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.refl _
+
 end measure
 
 end measure_theory
@@ -854,6 +876,32 @@ 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 | p a } ∈ (@measure_space.μ α _).a_e.sets
+
+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.refl _
+
+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
+
 end measure_space
 
 end measure_theory