feat(measure_theory/function/ae_eq_of_integral): two ennreal-valued f…

…unction are a.e. equal if their integrals agree (#9372)

src/measure_theory/function/ae_eq_of_integral.lean

@@ -471,4 +471,33 @@ end
 
 end ae_eq_of_forall_set_integral_eq
 
+section lintegral
+
+lemma ae_measurable.ae_eq_of_forall_set_lintegral_eq {f g : α → ℝ≥0∞}
+  (hf : ae_measurable f μ) (hg : ae_measurable g μ)
+  (hfi : ∫⁻ x, f x ∂μ ≠ ∞) (hgi : ∫⁻ x, g x ∂μ ≠ ∞)
+  (hfg : ∀ ⦃s⦄, measurable_set s → μ s < ∞ → ∫⁻ x in s, f x ∂μ = ∫⁻ x in s, g x ∂μ) :
+  f =ᵐ[μ] g :=
+begin
+  refine ennreal.eventually_eq_of_to_real_eventually_eq
+    (ae_lt_top' hf hfi).ne_of_lt (ae_lt_top' hg hgi).ne_of_lt
+    (integrable.ae_eq_of_forall_set_integral_eq _ _
+      (integrable_to_real_of_lintegral_ne_top hf hfi)
+      (integrable_to_real_of_lintegral_ne_top hg hgi) (λ s hs hs', _)),
+  rw [integral_eq_lintegral_of_nonneg_ae, integral_eq_lintegral_of_nonneg_ae],
+  { congr' 1,
+    rw [lintegral_congr_ae (of_real_to_real_ae_eq _),
+        lintegral_congr_ae (of_real_to_real_ae_eq _)],
+    { exact hfg hs hs' },
+    { refine (ae_lt_top' hg.restrict (ne_of_lt (lt_of_le_of_lt _ hgi.lt_top))),
+      exact @set_lintegral_univ α _ μ g ▸ lintegral_mono_set (set.subset_univ _) },
+    { refine (ae_lt_top' hf.restrict (ne_of_lt (lt_of_le_of_lt _ hfi.lt_top))),
+      exact @set_lintegral_univ α _ μ f ▸ lintegral_mono_set (set.subset_univ _) } },
+  -- putting the proofs where they are used is extremely slow
+  exacts [ae_of_all _ (λ x, ennreal.to_real_nonneg), hg.ennreal_to_real.restrict,
+          ae_of_all _ (λ x, ennreal.to_real_nonneg), hf.ennreal_to_real.restrict]
+end
+
+end lintegral
+
 end measure_theory

src/order/filter/basic.lean

@@ -1354,6 +1354,22 @@ lemma eventually_le.le_iff_eq [partial_order β] {l : filter α} {f g : α → 
   g ≤ᶠ[l] f ↔ g =ᶠ[l] f :=
 ⟨λ h', h'.antisymm h, eventually_eq.le⟩
 
+lemma eventually.ne_of_lt [preorder β] {l : filter α} {f g : α → β}
+  (h : ∀ᶠ x in l, f x < g x) : ∀ᶠ x in l, f x ≠ g x :=
+h.mono (λ x hx, hx.ne)
+
+lemma eventually.ne_top_of_lt [order_top β] {l : filter α} {f g : α → β}
+  (h : ∀ᶠ x in l, f x < g x) : ∀ᶠ x in l, f x ≠ ⊤ :=
+h.mono (λ x hx, hx.ne_top)
+
+lemma eventually.lt_top_of_ne [order_top β] {l : filter α} {f : α → β}
+  (h : ∀ᶠ x in l, f x ≠ ⊤) : ∀ᶠ x in l, f x < ⊤ :=
+h.mono (λ x hx, hx.lt_top)
+
+lemma eventually.lt_top_iff_ne_top [order_top β] {l : filter α} {f : α → β} :
+  (∀ᶠ x in l, f x < ⊤) ↔ ∀ᶠ x in l, f x ≠ ⊤ :=
+⟨eventually.ne_of_lt, eventually.lt_top_of_ne⟩
+
 @[mono] lemma eventually_le.inter {s t s' t' : set α} {l : filter α} (h : s ≤ᶠ[l] t)
   (h' : s' ≤ᶠ[l] t') :
   (s ∩ s' : set α) ≤ᶠ[l] (t ∩ t' : set α) :=

src/topology/instances/ennreal.lean

@@ -120,6 +120,16 @@ begin
   exact tendsto_id
 end
 
+lemma eventually_eq_of_to_real_eventually_eq {l : filter α} {f g : α → ℝ≥0∞}
+  (hfi : ∀ᶠ x in l, f x ≠ ∞) (hgi : ∀ᶠ x in l, g x ≠ ∞)
+  (hfg : (λ x, (f x).to_real) =ᶠ[l] (λ x, (g x).to_real)) :
+  f =ᶠ[l] g :=
+begin
+  filter_upwards [hfi, hgi, hfg],
+  intros x hfx hgx hfgx,
+  rwa ← ennreal.to_real_eq_to_real hfx hgx,
+end
+
 lemma continuous_on_to_nnreal : continuous_on ennreal.to_nnreal {a | a ≠ ∞}  :=
 λ a ha, continuous_at.continuous_within_at (tendsto_to_nnreal ha)