feat(measure_theory/function/ae_eq_of_integral): remove a finite_meas…

…ure assumption (#15899)

src/measure_theory/function/ae_eq_of_integral.lean

@@ -236,72 +236,83 @@ end ennreal
 
 section real
 
-section real_finite_measure
+variables {f : α → ℝ}
 
-variables [is_finite_measure μ] {f : α → ℝ}
-
-/-- Don't use this lemma. Use `ae_nonneg_of_forall_set_integral_nonneg_of_finite_measure`. -/
-lemma ae_nonneg_of_forall_set_integral_nonneg_of_finite_measure_of_strongly_measurable
+/-- Don't use this lemma. Use `ae_nonneg_of_forall_set_integral_nonneg`. -/
+lemma ae_nonneg_of_forall_set_integral_nonneg_of_strongly_measurable
   (hfm : strongly_measurable f)
-  (hf : integrable f μ) (hf_zero : ∀ s, measurable_set s → 0 ≤ ∫ x in s, f x ∂μ) :
+  (hf : integrable f μ) (hf_zero : ∀ s, measurable_set s → μ s < ∞ → 0 ≤ ∫ x in s, f x ∂μ) :
   0 ≤ᵐ[μ] f :=
 begin
   simp_rw [eventually_le, pi.zero_apply],
   rw ae_const_le_iff_forall_lt_measure_zero,
   intros b hb_neg,
   let s := {x | f x ≤ b},
   have hs : measurable_set s, from hfm.measurable_set_le strongly_measurable_const,
+  have mus : μ s < ∞,
+  { let c : ℝ≥0 := ⟨|b|, abs_nonneg _⟩,
+    have c_pos : (c : ℝ≥0∞) ≠ 0, by simpa using hb_neg.ne,
+    calc μ s ≤ μ {x | (c : ℝ≥0∞) ≤ ∥f x∥₊} :
+    begin
+      apply measure_mono,
+      assume x hx,
+      simp only [set.mem_set_of_eq] at hx,
+      simpa only [nnnorm, abs_of_neg hb_neg, abs_of_neg (hx.trans_lt hb_neg), real.norm_eq_abs,
+        subtype.mk_le_mk, neg_le_neg_iff, set.mem_set_of_eq, ennreal.coe_le_coe] using hx,
+    end
+    ... ≤ (∫⁻ x, ∥f x∥₊ ∂μ) / c :
+      meas_ge_le_lintegral_div hfm.ae_measurable.ennnorm c_pos ennreal.coe_ne_top
+    ... < ∞ : ennreal.div_lt_top (ne_of_lt hf.2) c_pos },
   have h_int_gt : ∫ x in s, f x ∂μ ≤ b * (μ s).to_real,
   { have h_const_le : ∫ x in s, f x ∂μ ≤ ∫ x in s, b ∂μ,
     { refine set_integral_mono_ae_restrict hf.integrable_on
-        (integrable_on_const.mpr (or.inr (measure_lt_top μ s))) _,
+        (integrable_on_const.mpr (or.inr mus)) _,
       rw [eventually_le, ae_restrict_iff hs],
       exact eventually_of_forall (λ x hxs, hxs), },
     rwa [set_integral_const, smul_eq_mul, mul_comm] at h_const_le, },
   by_contra,
   refine (lt_self_iff_false (∫ x in s, f x ∂μ)).mp (h_int_gt.trans_lt _),
   refine (mul_neg_iff.mpr (or.inr ⟨hb_neg, _⟩)).trans_le _,
-  swap, { simp_rw measure.restrict_restrict hs, exact hf_zero s hs, },
+  swap, { simp_rw measure.restrict_restrict hs, exact hf_zero s hs mus, },
   refine (ennreal.to_real_nonneg).lt_of_ne (λ h_eq, h _),
   cases (ennreal.to_real_eq_zero_iff _).mp h_eq.symm with hμs_eq_zero hμs_eq_top,
   { exact hμs_eq_zero, },
-  { exact absurd hμs_eq_top (measure_lt_top μ s).ne, },
+  { exact absurd hμs_eq_top mus.ne, },
 end
 
-lemma ae_nonneg_of_forall_set_integral_nonneg_of_finite_measure (hf : integrable f μ)
-  (hf_zero : ∀ s, measurable_set s → 0 ≤ ∫ x in s, f x ∂μ) :
+lemma ae_nonneg_of_forall_set_integral_nonneg (hf : integrable f μ)
+  (hf_zero : ∀ s, measurable_set s → μ s < ∞ → 0 ≤ ∫ x in s, f x ∂μ) :
   0 ≤ᵐ[μ] f :=
 begin
   rcases hf.1 with ⟨f', hf'_meas, hf_ae⟩,
   have hf'_integrable : integrable f' μ, from integrable.congr hf hf_ae,
-  have hf'_zero : ∀ s, measurable_set s → 0 ≤ ∫ x in s, f' x ∂μ,
-  { intros s hs,
+  have hf'_zero : ∀ s, measurable_set s → μ s < ∞ → 0 ≤ ∫ x in s, f' x ∂μ,
+  { intros s hs h's,
     rw set_integral_congr_ae hs (hf_ae.mono (λ x hx hxs, hx.symm)),
-    exact hf_zero s hs, },
-  exact (ae_nonneg_of_forall_set_integral_nonneg_of_finite_measure_of_strongly_measurable hf'_meas
+    exact hf_zero s hs h's, },
+  exact (ae_nonneg_of_forall_set_integral_nonneg_of_strongly_measurable hf'_meas
     hf'_integrable hf'_zero).trans hf_ae.symm.le,
 end
 
 lemma ae_le_of_forall_set_integral_le {f g : α → ℝ} (hf : integrable f μ) (hg : integrable g μ)
-  (hf_le : ∀ s, measurable_set s → ∫ x in s, f x ∂μ ≤ ∫ x in s, g x ∂μ) :
+  (hf_le : ∀ s, measurable_set s → μ s < ∞ → ∫ x in s, f x ∂μ ≤ ∫ x in s, g x ∂μ) :
   f ≤ᵐ[μ] g :=
 begin
   rw ← eventually_sub_nonneg,
-  refine ae_nonneg_of_forall_set_integral_nonneg_of_finite_measure (hg.sub hf) (λ s hs, _),
+  refine ae_nonneg_of_forall_set_integral_nonneg (hg.sub hf) (λ s hs, _),
   rw [integral_sub' hg.integrable_on hf.integrable_on, sub_nonneg],
   exact hf_le s hs
 end
 
-end real_finite_measure
-
-lemma ae_nonneg_restrict_of_forall_set_integral_nonneg_inter {f : α → ℝ} {t : set α} (hμt : μ t ≠ ∞)
-  (hf : integrable_on f t μ) (hf_zero : ∀ s, measurable_set s → 0 ≤ ∫ x in (s ∩ t), f x ∂μ) :
+lemma ae_nonneg_restrict_of_forall_set_integral_nonneg_inter {f : α → ℝ} {t : set α}
+  (hf : integrable_on f t μ)
+  (hf_zero : ∀ s, measurable_set s → μ (s ∩ t) < ∞ → 0 ≤ ∫ x in (s ∩ t), f x ∂μ) :
   0 ≤ᵐ[μ.restrict t] f :=
 begin
-  haveI : fact (μ t < ∞) := ⟨lt_top_iff_ne_top.mpr hμt⟩,
-  refine ae_nonneg_of_forall_set_integral_nonneg_of_finite_measure hf (λ s hs, _),
+  refine ae_nonneg_of_forall_set_integral_nonneg hf (λ s hs h's, _),
   simp_rw measure.restrict_restrict hs,
-  exact hf_zero s hs,
+  apply hf_zero s hs,
+  rwa measure.restrict_apply hs at h's,
 end
 
 lemma ae_nonneg_of_forall_set_integral_nonneg_of_sigma_finite [sigma_finite μ] {f : α → ℝ}
@@ -311,9 +322,9 @@ lemma ae_nonneg_of_forall_set_integral_nonneg_of_sigma_finite [sigma_finite μ]
 begin
   apply ae_of_forall_measure_lt_top_ae_restrict,
   assume t t_meas t_lt_top,
-  apply ae_nonneg_restrict_of_forall_set_integral_nonneg_inter t_lt_top.ne
+  apply ae_nonneg_restrict_of_forall_set_integral_nonneg_inter
     (hf_int_finite t t_meas t_lt_top),
-  assume s s_meas,
+  assume s s_meas hs,
   exact hf_zero _ (s_meas.inter t_meas)
     (lt_of_le_of_lt (measure_mono (set.inter_subset_right _ _)) t_lt_top)
 end
@@ -338,20 +349,14 @@ begin
     exact hf_zero (s ∩ t) (hs.inter hf.measurable_set) hμts, },
 end
 
-lemma integrable.ae_nonneg_of_forall_set_integral_nonneg {f : α → ℝ} (hf : integrable f μ)
-  (hf_zero : ∀ s, measurable_set s → μ s < ∞ → 0 ≤ ∫ x in s, f x ∂μ) :
-  0 ≤ᵐ[μ] f :=
-ae_fin_strongly_measurable.ae_nonneg_of_forall_set_integral_nonneg hf.ae_fin_strongly_measurable
-  (λ s hs hμs, hf.integrable_on) hf_zero
-
 lemma ae_nonneg_restrict_of_forall_set_integral_nonneg {f : α → ℝ}
   (hf_int_finite : ∀ s, measurable_set s → μ s < ∞ → integrable_on f s μ)
   (hf_zero : ∀ s, measurable_set s → μ s < ∞ → 0 ≤ ∫ x in s, f x ∂μ)
   {t : set α} (ht : measurable_set t) (hμt : μ t ≠ ∞) :
   0 ≤ᵐ[μ.restrict t] f :=
 begin
-  refine ae_nonneg_restrict_of_forall_set_integral_nonneg_inter hμt
-    (hf_int_finite t ht (lt_top_iff_ne_top.mpr hμt)) (λ s hs, _),
+  refine ae_nonneg_restrict_of_forall_set_integral_nonneg_inter
+    (hf_int_finite t ht (lt_top_iff_ne_top.mpr hμt)) (λ s hs h's, _),
   refine (hf_zero (s ∩ t) (hs.inter ht) _),
   exact (measure_mono (set.inter_subset_right s t)).trans_lt (lt_top_iff_ne_top.mpr hμt),
 end

src/probability/martingale.lean

@@ -277,9 +277,9 @@ begin
   suffices : 0 ≤ᵐ[μ.trim (ℱ.le i)] μ[f j| ℱ i] - f i,
   { filter_upwards [this] with x hx,
     rwa ← sub_nonneg },
-  refine ae_nonneg_of_forall_set_integral_nonneg_of_finite_measure
+  refine ae_nonneg_of_forall_set_integral_nonneg
     ((integrable_condexp.sub (hint i)).trim _ (strongly_measurable_condexp.sub $ hadp i))
-    (λ s hs, _),
+    (λ s hs h's, _),
   specialize hf i j hij s hs,
   rwa [← set_integral_trim _ (strongly_measurable_condexp.sub $ hadp i) hs,
     integral_sub' integrable_condexp.integrable_on (hint i).integrable_on, sub_nonneg,
@@ -297,15 +297,17 @@ begin
   apply_instance
 end
 
-lemma submartingale.condexp_sub_nonneg [is_finite_measure μ]
+lemma submartingale.condexp_sub_nonneg
   {f : ι → α → ℝ} (hf : submartingale f ℱ μ) {i j : ι} (hij : i ≤ j) :
   0 ≤ᵐ[μ] μ[f j - f i | ℱ i] :=
 begin
+  by_cases h : sigma_finite (μ.trim (ℱ.le i)),
+  swap, { rw condexp_of_not_sigma_finite (ℱ.le i) h },
   refine eventually_le.trans _ (condexp_sub (hf.integrable _) (hf.integrable _)).symm.le,
   rw [eventually_sub_nonneg,
     condexp_of_strongly_measurable (ℱ.le _) (hf.adapted _) (hf.integrable _)],
-  exact hf.2.1 i j hij,
-  apply_instance
+  { exact hf.2.1 i j hij },
+  { exact h }
 end
 
 lemma submartingale_iff_condexp_sub_nonneg [is_finite_measure μ] {f : ι → α → ℝ} :