Merge branch 'LL/dotNotation' into TestLeanCopilot

TestingLowerBounds.lean

@@ -23,10 +23,8 @@ import TestingLowerBounds.ForMathlib.KernelFstSnd
 import TestingLowerBounds.ForMathlib.LeftRightDeriv
 import TestingLowerBounds.ForMathlib.LogLikelihoodRatioCompProd
 import TestingLowerBounds.ForMathlib.MaxMinEqAbs
-import TestingLowerBounds.ForMathlib.MonotoneOnTendsto
 import TestingLowerBounds.ForMathlib.RadonNikodym
 import TestingLowerBounds.ForMathlib.RnDeriv
-import TestingLowerBounds.ForMathlib.SetIntegral
 import TestingLowerBounds.Kernel.Basic
 import TestingLowerBounds.Kernel.BayesInv
 import TestingLowerBounds.Kernel.Monoidal

TestingLowerBounds/DerivAtTop.lean

@@ -159,7 +159,7 @@ lemma MonotoneOn.derivAtTop_eq_top_iff (hf : MonotoneOn (rightDeriv f) (Ioi 0))
     derivAtTop f = ⊤ ↔ Tendsto (rightDeriv f) atTop atTop := by
   refine ⟨fun h ↦ ?_, fun h ↦ derivAtTop_of_tendsto_atTop h⟩
   exact EReal.tendsto_toReal_atTop.comp (tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _
-    (h ▸ hf.tendsto_derivAtTop) (eventually_of_forall fun _ ↦ EReal.coe_ne_top _))
+    (h ▸ hf.tendsto_derivAtTop) (.of_forall fun _ ↦ EReal.coe_ne_top _))
 
 lemma ConvexOn.derivAtTop_eq_top_iff (hf : ConvexOn ℝ (Ici 0) f) :
     derivAtTop f = ⊤ ↔ Tendsto (rightDeriv f) atTop atTop :=
@@ -278,7 +278,7 @@ lemma le_add_derivAtTop (h_cvx : ConvexOn ℝ (Ici 0) f)
   | inl h_eq => simp [h_eq]
   | inr h_lt =>
     have h_le := slope_le_derivAtTop h_cvx h hy h_lt
-    rwa [div_le_iff, sub_le_iff_le_add'] at h_le
+    rwa [div_le_iff₀, sub_le_iff_le_add'] at h_le
     simp [h_lt]
 
 lemma le_add_derivAtTop'' (h_cvx : ConvexOn ℝ (Ici 0) f)

TestingLowerBounds/Divergences/Hellinger.lean

@@ -656,7 +656,7 @@ lemma meas_univ_add_mul_hellingerDiv_eq_zero_iff (ha_ne_one : a ≠ 1)
   · rw [meas_univ_add_mul_hellingerDiv_zero_eq ha_zero, ← Measure.rnDeriv_eq_zero,
       EReal.coe_ennreal_eq_zero]
     simp_rw [← not_le, ← ae_iff]
-    exact eventually_congr <| eventually_of_forall <| fun _ ↦ nonpos_iff_eq_zero
+    exact eventually_congr <| .of_forall <| fun _ ↦ nonpos_iff_eq_zero
   rw [meas_univ_add_mul_hellingerDiv_eq ha_zero ha_ne_one h_top]
   norm_cast
   refine integral_rpow_rnDeriv_eq_zero_iff_mutuallySingular ha_zero ?_
@@ -770,7 +770,7 @@ lemma integrable_hellingerDiv_iff_of_lt_one (ha_nonneg : 0 ≤ a) (ha : a < 1)
     [IsFiniteKernel κ] [IsFiniteKernel η] :
     Integrable (fun x ↦ (hellingerDiv a (κ x) (η x)).toReal) μ
       ↔ Integrable (fun x ↦ ∫ b, hellingerFun a ((∂κ x/∂η x) b).toReal ∂η x) μ := by
-  refine integrable_congr (eventually_of_forall fun x ↦ ?_)
+  refine integrable_congr (.of_forall fun x ↦ ?_)
   simp_rw [hellingerDiv_eq_integral_of_lt_one ha_nonneg ha, EReal.toReal_coe]
 
 lemma integrable_hellingerDiv_iff' (ha_pos : 0 < a) (ha_ne_one : a ≠ 1)
@@ -805,7 +805,7 @@ lemma integrable_hellingerDiv_iff' (ha_pos : 0 < a) (ha_ne_one : a ≠ 1)
   obtain ⟨C, ⟨hC_finite, hC⟩⟩ := IsFiniteKernel.exists_univ_le (κ := η)
   refine integrable_add_iff_integrable_left <| (integrable_const C.toReal).mono' ?_ ?_
   · exact η.measurable_coe .univ |>.ennreal_toReal.neg.aestronglyMeasurable
-  refine eventually_of_forall (fun x ↦ ?_)
+  refine .of_forall (fun x ↦ ?_)
   rw [norm_eq_abs, abs_neg, abs_eq_self.mpr ENNReal.toReal_nonneg, ENNReal.toReal_le_toReal
     (measure_ne_top _ _) (lt_top_iff_ne_top.mp hC_finite)]
   exact hC x
@@ -831,7 +831,7 @@ lemma integrable_hellingerDiv_zero [CountableOrCountablyGenerated α β]
     apply Measurable.ennreal_toReal
     exact Kernel.measurable_kernel_prod_mk_left
       (measurableSet_eq_fun (κ.measurable_rnDeriv η).ennreal_toReal measurable_const)
-  · refine eventually_of_forall (fun x ↦ ?_)
+  · refine .of_forall fun x ↦ ?_
     simp only [norm_eq_abs, ENNReal.abs_toReal, ENNReal.toReal_le_toReal
     (measure_ne_top _ _) (lt_top_iff_ne_top.mp hC_finite)]
     exact measure_mono (Set.subset_univ _) |>.trans (hC x)
@@ -840,7 +840,7 @@ lemma integrable_hellingerDiv_iff'_of_lt_one (ha_pos : 0 < a) (ha : a < 1)
     [IsFiniteMeasure μ] [IsFiniteKernel κ] [IsFiniteKernel η] :
     Integrable (fun x ↦ (hellingerDiv a (κ x) (η x)).toReal) μ
       ↔ Integrable (fun x ↦ ∫ b, ((∂κ x/∂η x) b).toReal ^ a ∂η x) μ :=
-  integrable_hellingerDiv_iff' ha_pos ha.ne (eventually_of_forall
+  integrable_hellingerDiv_iff' ha_pos ha.ne (.of_forall
     (fun _ ↦ integrable_rpow_rnDeriv_of_lt_one ha_pos.le ha)) (not_le_of_gt ha).elim
 
 /-- Conditional Hellinger divergence of order `a`. -/
@@ -947,15 +947,15 @@ lemma condHellingerDiv_zero_eq [CountableOrCountablyGenerated α β]
     condHellingerDiv 0 κ η μ = ∫ x, (hellingerDiv 0 (κ x) (η x)).toReal ∂μ :=
   condHellingerDiv_of_ae_finite_of_integrable
     ((hellingerDiv_ae_ne_top_iff' _ _).mpr
-      ⟨eventually_of_forall (fun _ ↦ integrable_hellingerFun_zero), by simp⟩)
+      ⟨.of_forall fun _ ↦ integrable_hellingerFun_zero, by simp⟩)
     integrable_hellingerDiv_zero
 
 lemma condHellingerDiv_zero_of_ae_integrable_of_integrable [IsFiniteKernel κ] [IsFiniteKernel η]
     (h_int2 : Integrable (fun x ↦ (hellingerDiv 0 (κ x) (η x)).toReal) μ) :
     condHellingerDiv 0 κ η μ = ∫ x, (hellingerDiv 0 (κ x) (η x)).toReal ∂μ :=
   condHellingerDiv_of_ae_finite_of_integrable
     ((hellingerDiv_ae_ne_top_iff' _ _).mpr
-      ⟨eventually_of_forall (fun _ ↦ integrable_hellingerFun_zero), by simp⟩) h_int2
+      ⟨.of_forall fun _ ↦ integrable_hellingerFun_zero, by simp⟩) h_int2
 
 --TODO: try to generalize this to the case `a = 0`
 lemma condHellingerDiv_of_ae_integrable_of_ae_ac_of_integrable' (ha_pos : 0 < a) (ha_ne_one : a ≠ 1)
@@ -981,7 +981,7 @@ lemma condHellingerDiv_of_integrable'_of_lt_one (ha_pos : 0 < a) (ha : a < 1)
     condHellingerDiv a κ η μ = ∫ x, (hellingerDiv a (κ x) (η x)).toReal ∂μ :=
   condHellingerDiv_of_ae_finite_of_integrable
     ((hellingerDiv_ae_ne_top_iff_of_lt_one ha _ _).mpr
-      (eventually_of_forall <| fun _ ↦ integrable_rpow_rnDeriv_of_lt_one ha_pos.le ha))
+      (.of_forall <| fun _ ↦ integrable_rpow_rnDeriv_of_lt_one ha_pos.le ha))
     (integrable_hellingerDiv_iff'_of_lt_one ha_pos ha |>.mpr h_int')
 
 lemma condHellingerDiv_eq_top_iff [IsFiniteKernel κ] [IsFiniteKernel η] :
@@ -1062,7 +1062,7 @@ lemma condHellingerDiv_eq_top_iff_of_lt_one' (ha_pos : 0 < a) (ha : a < 1)
     condHellingerDiv a κ η μ = ⊤
       ↔ ¬ Integrable (fun x ↦ ∫ b, ((∂κ x/∂η x) b).toReal ^ a ∂η x) μ := by
   simp_rw [condHellingerDiv_eq_top_iff_of_lt_one ha,
-    (eventually_of_forall <| fun _ ↦ integrable_hellingerFun_rnDeriv_of_lt_one ha_pos.le ha),
+    (Eventually.of_forall <| fun _ ↦ integrable_hellingerFun_rnDeriv_of_lt_one ha_pos.le ha),
     integrable_hellingerDiv_iff'_of_lt_one ha_pos ha, not_true, false_or]
 
 lemma condHellingerDiv_ne_top_iff_of_lt_one' (ha_pos : 0 < a) (ha : a < 1)
@@ -1113,7 +1113,7 @@ lemma condHellingerDiv_eq_integral'_of_one_lt (ha : 1 < a)
         hellingerDiv_ne_top_iff_of_one_lt ha _ _ |>.mpr ⟨hx_int, hx_ac⟩
     _ = ∫ x, ((a - 1)⁻¹ * ∫ b, ((∂κ x/∂η x) b).toReal ^ a ∂η x
         - (a - 1)⁻¹ * ((η x) .univ).toReal) ∂μ := by
-      refine integral_congr_ae (eventually_of_forall fun x ↦ ?_)
+      refine integral_congr_ae (.of_forall fun x ↦ ?_)
       dsimp
       rw [EReal.toReal_sub (ne_of_beq_false (by rfl)) (ne_of_beq_false (by rfl))]
       congr
@@ -1166,7 +1166,7 @@ lemma condHellingerDiv_eq_integral'_of_lt_one (ha_pos : 0 < a) (ha : a < 1)
       exact hellingerDiv_eq_integral_of_lt_one' ha_pos ha _ _
     _ = ∫ x, ((a - 1)⁻¹ * ∫ b, ((∂κ x/∂η x) b).toReal ^ a ∂η x --from here to the end the proof is the same as the one of `condHellingerDiv_eq_integral'_of_one_lt`, consider separating this part as a lemma
         - (a - 1)⁻¹ * ((η x) .univ).toReal) ∂μ := by
-      refine integral_congr_ae (eventually_of_forall fun x ↦ ?_)
+      refine integral_congr_ae (.of_forall fun x ↦ ?_)
       dsimp
       rw [EReal.toReal_sub (ne_of_beq_false (by rfl)) (ne_of_beq_false (by rfl))]
       congr

TestingLowerBounds/Divergences/StatInfo.lean

@@ -9,7 +9,6 @@ import Mathlib.Order.CompletePartialOrder
 import TestingLowerBounds.FDiv.Basic
 import TestingLowerBounds.Testing.Binary
 import Mathlib.MeasureTheory.Constructions.Prod.Integral
-import TestingLowerBounds.ForMathlib.SetIntegral
 
 /-!
 # Statistical information
@@ -66,7 +65,7 @@ lemma statInfo_le_min : statInfo μ ν π ≤ min (π {false} * μ univ) (π {tr
 lemma statInfo_ne_top [IsFiniteMeasure μ] [IsFiniteMeasure π] :
     statInfo μ ν π ≠ ⊤ :=
   (statInfo_le_min.trans_lt <| min_lt_iff.mpr <| Or.inl
-    <| ENNReal.mul_lt_top (measure_ne_top π _) (measure_ne_top μ _)).ne
+    <| ENNReal.mul_lt_top (measure_lt_top π _) (measure_lt_top μ _)).ne
 
 lemma statInfo_symm : statInfo μ ν π = statInfo ν μ (π.map Bool.not) := by
   simp_rw [statInfo, bayesBinaryRisk_symm _ _ π]
@@ -730,18 +729,18 @@ lemma lintegral_f_rnDeriv_eq_lintegralfDiv_statInfoFun_of_absolutelyContinuous
     ← integral_statInfoFun_curvatureMeasure' hf_cvx hf_cont hf_one hfderiv_one]
   have (x : 𝒳) : ENNReal.ofReal (∫ γ, statInfoFun 1 γ ((∂μ/∂ν) x).toReal ∂curvatureMeasure f) =
       ∫⁻ γ, ENNReal.ofReal (statInfoFun 1 γ ((∂μ/∂ν) x).toReal) ∂curvatureMeasure f := by
-    rw [integral_eq_lintegral_of_nonneg_ae (eventually_of_forall fun y ↦ statInfoFun_nonneg _ _ _)
+    rw [integral_eq_lintegral_of_nonneg_ae (.of_forall fun y ↦ statInfoFun_nonneg _ _ _)
         h_meas.of_uncurry_left.stronglyMeasurable.aestronglyMeasurable]
     refine ENNReal.ofReal_toReal <| (lintegral_ofReal_le_lintegral_nnnorm _).trans_lt ?_ |>.ne
     exact (integrable_statInfoFun 1 _).hasFiniteIntegral
   simp_rw [this]
   rw [lintegral_lintegral_swap h_meas.ennreal_ofReal.aemeasurable]
   congr with y
-  rw [integral_eq_lintegral_of_nonneg_ae (eventually_of_forall fun _ ↦ statInfoFun_nonneg _ _ _)
+  rw [integral_eq_lintegral_of_nonneg_ae (.of_forall fun _ ↦ statInfoFun_nonneg _ _ _)
     h_meas.of_uncurry_right.stronglyMeasurable.aestronglyMeasurable, ENNReal.ofReal_toReal]
   refine (integrable_toReal_iff ?_ ?_).mp ?_
   · exact h_meas.comp (f := fun x ↦ (x, y)) (by fun_prop) |>.ennreal_ofReal.aemeasurable
-  · exact eventually_of_forall fun _ ↦ ENNReal.ofReal_ne_top
+  · exact .of_forall fun _ ↦ ENNReal.ofReal_ne_top
   · simp_rw [ENNReal.toReal_ofReal (statInfoFun_nonneg 1 _ _)]
     exact integrable_statInfoFun_rnDeriv 1 y μ ν
 
@@ -764,12 +763,12 @@ lemma fDiv_ne_top_iff_integrable_fDiv_statInfoFun_of_absolutelyContinuous'
   rotate_left
   · exact hf_cont.measurable.comp (μ.measurable_rnDeriv ν).ennreal_toReal
       |>.ennreal_ofReal.aemeasurable
-  · exact eventually_of_forall fun _ ↦ ENNReal.ofReal_ne_top
+  · exact .of_forall fun _ ↦ ENNReal.ofReal_ne_top
   rw [integrable_toReal_iff]
   rotate_left
   · exact (fDiv_statInfoFun_stronglyMeasurable μ ν).measurable.comp (f := fun x ↦ (1, x))
       (by fun_prop) |>.ereal_toENNReal.aemeasurable
-  · exact eventually_of_forall fun _ ↦ EReal.toENNReal_ne_top_iff.mpr fDiv_statInfoFun_ne_top
+  · exact .of_forall fun _ ↦ EReal.toENNReal_ne_top_iff.mpr fDiv_statInfoFun_ne_top
   rw [lintegral_f_rnDeriv_eq_lintegralfDiv_statInfoFun_of_absolutelyContinuous hf_cvx hf_cont
     hf_one hfderiv_one h_ac]
 
@@ -823,21 +822,21 @@ lemma fDiv_eq_integral_fDiv_statInfoFun_of_absolutelyContinuous'
         ∂curvatureMeasure f ∂ν).toReal := by
     rw [integral_eq_lintegral_of_nonneg_ae]
     rotate_left
-    · exact eventually_of_forall fun _ ↦ (integral_nonneg (fun _ ↦ statInfoFun_nonneg _ _ _))
+    · exact .of_forall fun _ ↦ (integral_nonneg (fun _ ↦ statInfoFun_nonneg _ _ _))
     · refine (StronglyMeasurable.integral_prod_left ?_).aestronglyMeasurable
       exact (measurable_swap_iff.mpr h_meas).stronglyMeasurable
     congr with x
-    rw [integral_eq_lintegral_of_nonneg_ae (eventually_of_forall fun y ↦ statInfoFun_nonneg _ _ _)
+    rw [integral_eq_lintegral_of_nonneg_ae (.of_forall fun y ↦ statInfoFun_nonneg _ _ _)
       h_meas.of_uncurry_left.stronglyMeasurable.aestronglyMeasurable]
     refine ENNReal.ofReal_toReal <| (lintegral_ofReal_le_lintegral_nnnorm _).trans_lt ?_ |>.ne
     exact (integrable_statInfoFun 1 _).hasFiniteIntegral
   rw [int_eq_lint, lintegral_lintegral_swap h_meas.ennreal_ofReal.aemeasurable,
     integral_eq_lintegral_of_nonneg_ae]
   rotate_left
-  · exact eventually_of_forall fun _ ↦ (integral_nonneg (fun _ ↦ statInfoFun_nonneg _ _ _))
+  · exact .of_forall fun _ ↦ (integral_nonneg (fun _ ↦ statInfoFun_nonneg _ _ _))
   · exact h_meas.stronglyMeasurable.integral_prod_left.aestronglyMeasurable
   congr with γ
-  rw [integral_eq_lintegral_of_nonneg_ae (eventually_of_forall fun _ ↦ statInfoFun_nonneg _ _ _)
+  rw [integral_eq_lintegral_of_nonneg_ae (.of_forall fun _ ↦ statInfoFun_nonneg _ _ _)
     h_meas.of_uncurry_right.stronglyMeasurable.aestronglyMeasurable, ENNReal.ofReal_toReal]
   have h_lt_top := (integrable_statInfoFun_rnDeriv 1 γ μ ν).hasFiniteIntegral
   simp_rw [HasFiniteIntegral, lt_top_iff_ne_top] at h_lt_top
@@ -877,7 +876,7 @@ lemma fDiv_eq_lintegral_fDiv_statInfoFun_of_absolutelyContinuous [IsFiniteMeasur
   · rw [fDiv_eq_integral_fDiv_statInfoFun_of_absolutelyContinuous hf_cvx hf_cont h_int h_ac,
       integral_eq_lintegral_of_nonneg_ae]
     rotate_left
-    · exact eventually_of_forall <| fun _ ↦ EReal.toReal_nonneg fDiv_statInfoFun_nonneg
+    · exact .of_forall <| fun _ ↦ EReal.toReal_nonneg fDiv_statInfoFun_nonneg
     · exact (fDiv_statInfoFun_stronglyMeasurable μ ν).measurable.comp (f := fun x ↦ (1, x))
         (by fun_prop) |>.ereal_toReal.aestronglyMeasurable
     simp_rw [← EReal.toENNReal_of_ne_top fDiv_statInfoFun_ne_top]
@@ -887,7 +886,7 @@ lemma fDiv_eq_lintegral_fDiv_statInfoFun_of_absolutelyContinuous [IsFiniteMeasur
     refine (integrable_toReal_iff ?_ ?_).mp ?_
     · exact (fDiv_statInfoFun_stronglyMeasurable μ ν).measurable.comp (f := fun x ↦ (1, x))
         (by fun_prop) |>.ereal_toENNReal.aemeasurable
-    · exact eventually_of_forall fun _ ↦ EReal.toENNReal_ne_top_iff.mpr fDiv_statInfoFun_ne_top
+    · exact .of_forall fun _ ↦ EReal.toENNReal_ne_top_iff.mpr fDiv_statInfoFun_ne_top
     simp_rw [EReal.toReal_toENNReal fDiv_statInfoFun_nonneg, h_int]
   · classical
     rw [fDiv_of_absolutelyContinuous h_ac, if_neg h_int]
@@ -904,7 +903,7 @@ lemma fDiv_eq_lintegral_fDiv_statInfoFun_of_absolutelyContinuous [IsFiniteMeasur
     refine (integrable_toReal_iff ?_ ?_).mpr h
     · exact (fDiv_statInfoFun_stronglyMeasurable μ ν).measurable.comp (f := fun x ↦ (1, x))
         (by fun_prop) |>.ereal_toENNReal.aemeasurable
-    · exact eventually_of_forall fun _ ↦ EReal.toENNReal_ne_top_iff.mpr fDiv_statInfoFun_ne_top
+    · exact .of_forall fun _ ↦ EReal.toENNReal_ne_top_iff.mpr fDiv_statInfoFun_ne_top
 
 lemma lintegral_statInfoFun_one_zero (hf_cvx : ConvexOn ℝ univ f) (hf_cont : Continuous f) :
     ∫⁻ x, ENNReal.ofReal (statInfoFun 1 x 0) ∂curvatureMeasure f
@@ -913,17 +912,16 @@ lemma lintegral_statInfoFun_one_zero (hf_cvx : ConvexOn ℝ univ f) (hf_cont : C
   have := convex_taylor hf_cvx hf_cont (a := 1) (b := 0)
   simp only [zero_sub, mul_neg, mul_one, sub_neg_eq_add] at this
   rw [this, intervalIntegral.integral_of_ge (zero_le_one' _), integral_neg, neg_neg,
-    ← ofReal_integral_eq_lintegral_ofReal _
-    (eventually_of_forall fun x ↦ statInfoFun_nonneg 1 x 0)]
+    ← ofReal_integral_eq_lintegral_ofReal _ (.of_forall fun x ↦ statInfoFun_nonneg 1 x 0)]
   rotate_left
   · refine Integrable.mono' (g := (Ioc 0 1).indicator 1) ?_
       measurable_statInfoFun2.aestronglyMeasurable ?_
     · exact IntegrableOn.integrable_indicator
         (integrableOn_const.mpr (Or.inr measure_Ioc_lt_top)) measurableSet_Ioc
     · simp_rw [Real.norm_of_nonneg (statInfoFun_nonneg 1 _ 0),
         statInfoFun_of_one_of_right_le_one zero_le_one, sub_zero]
-      exact eventually_of_forall fun x ↦ Set.indicator_le_indicator' fun hx ↦ hx.2
-  rw [EReal.coe_ennreal_ofReal, max_eq_left (integral_nonneg_of_ae <| eventually_of_forall
+      exact .of_forall fun x ↦ Set.indicator_le_indicator' fun hx ↦ hx.2
+  rw [EReal.coe_ennreal_ofReal, max_eq_left (integral_nonneg_of_ae <| .of_forall
     fun x ↦ statInfoFun_nonneg 1 x 0), ← integral_indicator measurableSet_Ioc]
   simp_rw [statInfoFun_of_one_of_right_le_one zero_le_one, sub_zero]
 
@@ -1029,11 +1027,10 @@ lemma fDiv_eq_lintegral_fDiv_statInfoFun [IsFiniteMeasure μ] [IsFiniteMeasure 
     rw [ENNReal.toReal_toEReal_of_ne_top (measure_ne_top ν _), ← EReal.coe_ennreal_mul,
       ← ENNReal.toEReal_sub h_ne_top]
     swap
-    · exact lintegral_mul_const' _ _ (measure_ne_top ν _) ▸ lintegral_mono fun x ↦ h_le x
+    · exact lintegral_mul_const' _ _ (measure_ne_top ν _) ▸ lintegral_mono h_le
     rw [← lintegral_mul_const' _ _ (measure_ne_top ν _),
       ← lintegral_sub (measurable_statInfoFun2.ennreal_ofReal.mul_const _)
-      (lintegral_mul_const' _ _ (measure_ne_top ν _) ▸ h_ne_top)
-      (eventually_of_forall fun x ↦ h_le x)]
+      (lintegral_mul_const' _ _ (measure_ne_top ν _) ▸ h_ne_top) (.of_forall h_le)]
     congr with x
     rw [EReal.toENNReal_sub (mul_nonneg (EReal.coe_nonneg.mpr (statInfoFun_nonneg 1 x 0))
       (EReal.coe_ennreal_nonneg _)),

TestingLowerBounds/FDiv/Basic.lean

@@ -792,7 +792,7 @@ lemma fDiv_mono'' (hf_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν
 /- The hypothesis `hfg'` can probably be removed if we ask for the functions to be convex, since then it is true that `derivAtTop` is monotone, but we still don't have the result formalized. Moreover in the convex case we can also relax `hf_int` and only ask for a.e. strong measurability of `f` (at least when `μ` and `ν` are finite), because then the negative part of the function is always integrable, hence if `f` is not integrable `g` is also not integrable. -/
 lemma fDiv_mono' (hf_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν)
     (hfg : f ≤ g) (hfg' : derivAtTop f ≤ derivAtTop g) : fDiv f μ ν ≤ fDiv g μ ν :=
-  fDiv_mono'' hf_int (eventually_of_forall hfg) hfg'
+  fDiv_mono'' hf_int (.of_forall hfg) hfg'
 
 lemma fDiv_nonneg_of_nonneg (hf : 0 ≤ f) (hf' : 0 ≤ derivAtTop f) :
     0 ≤ fDiv f μ ν :=
@@ -820,7 +820,7 @@ lemma fDiv_eq_zero_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h_mass : μ .u
   simp only [ENNReal.one_toReal, Function.const_one, log_one, mul_zero, lt_self_iff_false,
     or_false, hf_one] at h_eq
   exact (Measure.rnDeriv_eq_one_iff_eq hμν).mp <| ENNReal.eventuallyEq_of_toReal_eventuallyEq
-    (μ.rnDeriv_ne_top _) (eventually_of_forall fun _ ↦ ENNReal.one_ne_top) h_eq
+    (μ.rnDeriv_ne_top _) (.of_forall fun _ ↦ ENNReal.one_ne_top) h_eq
 
 lemma fDiv_eq_zero_iff' [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
     (hf_deriv : derivAtTop f = ⊤) (hf_cvx : StrictConvexOn ℝ (Ici 0) f)

TestingLowerBounds/FDiv/CondFDiv.lean

@@ -454,7 +454,7 @@ lemma condFDiv_compProd_meas_eq_top [CountableOrCountablyGenerated (α × β) γ
         ¬ Integrable (fun x ↦ (condFDiv f (κ.snd' x) (η.snd' x) (ξ x)).toReal) μ := by
   by_cases h_empty : Nonempty α
   swap; simp only [isEmpty_prod, not_nonempty_iff.mp h_empty, true_or, condFDiv_of_isEmpty_left,
-    EReal.zero_ne_top, IsEmpty.forall_iff, eventually_of_forall, not_true_eq_false,
+    EReal.zero_ne_top, IsEmpty.forall_iff, Eventually.of_forall, not_true_eq_false,
     Integrable.of_isEmpty, or_self]
   have := countableOrCountablyGenerated_right_of_prod_left_of_nonempty (α := α) (β := β) (γ := γ)
   rw [condFDiv_eq_top_iff hf_cvx]