Merge remote-tracking branch 'upstream/master' into TestLeanCopilot

TestingLowerBounds/CurvatureMeasure.lean

@@ -44,36 +44,36 @@ lemma measure_Ioi {l : ℝ} (hf : Tendsto f atTop (𝓝 l)) (x : ℝ) :
 
 --PR this and the following lemmas to mathlib, just after `StieltjesFunction.measure_univ`
 lemma measure_Ioi_of_tendsto_atTop_atTop (hf : Tendsto f atTop atTop) (x : ℝ) :
-    f.measure (Ioi x) = ⊤ := by
+    f.measure (Ioi x) = ∞ := by
   refine ENNReal.eq_top_of_forall_nnreal_le fun r ↦ ?_
   obtain ⟨N, hN⟩ := eventually_atTop.mp (tendsto_atTop.mp hf (r + f x))
   exact (f.measure_Ioc x (max x N) ▸ ENNReal.coe_nnreal_eq r ▸ (ENNReal.ofReal_le_ofReal <|
     le_tsub_of_add_le_right <| hN _ (le_max_right x N))).trans (measure_mono Ioc_subset_Ioi_self)
 
 lemma measure_Ici_of_tendsto_atTop_atTop (hf : Tendsto f atTop atTop) (x : ℝ) :
-    f.measure (Ici x) = ⊤ := by
+    f.measure (Ici x) = ∞ := by
   rw [← top_le_iff, ← f.measure_Ioi_of_tendsto_atTop_atTop hf x]
   exact measure_mono Ioi_subset_Ici_self
 
 lemma measure_Iic_of_tendsto_atBot_atBot (hf : Tendsto f atBot atBot) (x : ℝ) :
-    f.measure (Iic x) = ⊤ := by
+    f.measure (Iic x) = ∞ := by
   refine ENNReal.eq_top_of_forall_nnreal_le fun r ↦ ?_
   obtain ⟨N, hN⟩ := eventually_atBot.mp (tendsto_atBot.mp hf (f x - r))
   exact (f.measure_Ioc (min x N) x ▸ ENNReal.coe_nnreal_eq r ▸ (ENNReal.ofReal_le_ofReal <|
     le_sub_comm.mp <| hN _ (min_le_right x N))).trans (measure_mono Ioc_subset_Iic_self)
 
 lemma measure_Iio_of_tendsto_atBot_atBot (hf : Tendsto f atBot atBot) (x : ℝ) :
-    f.measure (Iio x) = ⊤ := by
+    f.measure (Iio x) = ∞ := by
   rw [← top_le_iff, ← f.measure_Iic_of_tendsto_atBot_atBot hf (x - 1)]
   exact measure_mono <| Set.Iic_subset_Iio.mpr <| sub_one_lt x
 
 lemma measure_univ_of_tendsto_atTop_atTop (hf : Tendsto f atTop atTop) :
-    f.measure univ = ⊤ := by
+    f.measure univ = ∞ := by
   rw [← top_le_iff, ← f.measure_Ioi_of_tendsto_atTop_atTop hf 0]
   exact measure_mono fun _ _ ↦ trivial
 
 lemma measure_univ_of_tendsto_atBot_atBot (hf : Tendsto f atBot atBot) :
-    f.measure univ = ⊤ := by
+    f.measure univ = ∞ := by
   rw [← top_le_iff, ← f.measure_Iio_of_tendsto_atBot_atBot hf 0]
   exact measure_mono fun _ _ ↦ trivial
 

TestingLowerBounds/DerivAtTop.lean

@@ -6,7 +6,6 @@ Authors: Rémy Degenne
 import TestingLowerBounds.Convex
 import TestingLowerBounds.ForMathlib.LeftRightDeriv
 import TestingLowerBounds.ForMathlib.EReal
-import TestingLowerBounds.ForMathlib.Tendsto
 
 /-!
 
@@ -159,8 +158,8 @@ lemma ConvexOn.derivAtTop_eq_iff {y : EReal} (hf : ConvexOn ℝ (Ici 0) f) :
 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_punctured_nhds_of_tendsto_nhds_right
-    (eventually_of_forall fun _ ↦ EReal.coe_ne_top _) (h ▸ hf.tendsto_derivAtTop))
+  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 _))
 
 lemma ConvexOn.derivAtTop_eq_top_iff (hf : ConvexOn ℝ (Ici 0) f) :
     derivAtTop f = ⊤ ↔ Tendsto (rightDeriv f) atTop atTop :=

TestingLowerBounds/Divergences/StatInfo.lean

@@ -10,7 +10,6 @@ import TestingLowerBounds.FDiv.Basic
 import TestingLowerBounds.Testing.Binary
 import Mathlib.MeasureTheory.Constructions.Prod.Integral
 import TestingLowerBounds.ForMathlib.SetIntegral
-import Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
 import TestingLowerBounds.ForMathlib.Indicator
 
 /-!
@@ -152,8 +151,6 @@ lemma toReal_statInfo_eq_min_sub_integral (μ ν : Measure 𝒳) [IsFiniteMeasur
   rw [toReal_bayesBinaryRisk_eq_integral_min,
     MonotoneOn.map_min (fun _ _ _ hb hab ↦ ENNReal.toReal_mono hb hab) hμ hν]
 
-#check Measure.rnDeriv_eq_div'
-
 lemma toReal_statInfo_eq_min_sub_integral' {ζ : Measure 𝒳} [IsFiniteMeasure μ] [IsFiniteMeasure ν]
     [SigmaFinite ζ] (π : Measure Bool) [IsFiniteMeasure π]  (hμζ : μ ≪ ζ) (hνζ : ν ≪ ζ) :
     (statInfo μ ν π).toReal = min (π {false} * μ univ).toReal (π {true} * ν univ).toReal
@@ -719,26 +716,6 @@ lemma integral_statInfoFun_curvatureMeasure' (hf_cvx : ConvexOn ℝ univ f) (hf_
   rw [integral_statInfoFun_curvatureMeasure hf_cvx hf_cont, hf_one, hfderiv_one, sub_zero, zero_mul,
     sub_zero]
 
-lemma fDiv_eq_fDiv_centeredFunction [IsFiniteMeasure μ] [IsFiniteMeasure ν]
-    (hf_cvx : ConvexOn ℝ univ f) :
-    fDiv f μ ν = fDiv (fun x ↦ f x - f 1 - rightDeriv f 1 * (x - 1)) μ ν
-      + f 1 * ν univ + rightDeriv f 1 * ((μ univ).toReal - (ν univ).toReal) := by
-  simp_rw [sub_eq_add_neg (f _), sub_eq_add_neg (_ + _), ← neg_mul]
-  rw [fDiv_add_linear']
-  swap; · exact hf_cvx.subset (fun _ _ ↦ trivial) (convex_Ici 0) |>.add_const _
-  rw [fDiv_add_const]
-  swap; · exact hf_cvx.subset (fun _ _ ↦ trivial) (convex_Ici 0)
-  simp_rw [EReal.coe_neg, neg_mul]
-  rw [add_assoc, add_comm (_ * _), ← add_assoc, add_assoc _ (-(_ * _)), add_comm (-(_ * _)),
-    ← sub_eq_add_neg (_ * _), EReal.sub_self, add_zero]
-  rotate_left
-  · refine (EReal.mul_ne_top _ _).mpr ⟨?_, Or.inr <| EReal.add_top_iff_ne_bot.mp rfl,
-      ?_, Or.inr <| Ne.symm (ne_of_beq_false rfl)⟩ <;> simp
-  · refine (EReal.mul_ne_bot _ _).mpr ⟨?_, Or.inr <| EReal.add_top_iff_ne_bot.mp rfl,
-      ?_, Or.inr <| Ne.symm (ne_of_beq_false rfl)⟩ <;> simp
-  rw [add_assoc, add_comm (-(_ * _)), ← sub_eq_add_neg, EReal.sub_self, add_zero]
-    <;> simp [EReal.mul_ne_top, EReal.mul_ne_bot, measure_ne_top]
-
 lemma lintegral_f_rnDeriv_eq_lintegralfDiv_statInfoFun_of_absolutelyContinuous
     [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hf_cvx : ConvexOn ℝ univ f) (hf_cont : Continuous f)
     (hf_one : f 1 = 0) (hfderiv_one : rightDeriv f 1 = 0) (h_ac : μ ≪ ν) :
@@ -992,10 +969,10 @@ lemma fDiv_eq_lintegral_fDiv_statInfoFun_of_mutuallySingular [IsFiniteMeasure μ
         · rw [h_top, EReal.top_sub_coe, EReal.toENNReal_top,
             StieltjesFunction.measure_Ioi_of_tendsto_atTop_atTop]
           exact hf_cvx'.derivAtTop_eq_top_iff.mp h_top
-        · have ⟨x, hx⟩ := EReal.eq_coe_of_ne_top_of_ne_bot h_top hf_cvx'.derivAtTop_ne_bot
-          rw [hx, StieltjesFunction.measure_Ioi _ ?_ 1 (l := x)]
+        · lift (derivAtTop f) to ℝ using ⟨h_top, hf_cvx'.derivAtTop_ne_bot⟩ with x hx
+          rw [StieltjesFunction.measure_Ioi _ ?_ 1 (l := x)]
           · norm_cast
-          exact (hx ▸ hf_cvx'.tendsto_toReal_derivAtTop h_top :)
+          exact (hx ▸ hf_cvx'.tendsto_toReal_derivAtTop (hx ▸ h_top) :)
   simp_rw [fDiv_of_mutuallySingular h_ms, h1]
   push_cast
   rw [lintegral_statInfoFun_one_zero hf_cvx hf_cont, h2, EReal.coe_toENNReal]

TestingLowerBounds/FDiv/Basic.lean

@@ -6,6 +6,8 @@ Authors: Rémy Degenne, Lorenzo Luccioli
 import TestingLowerBounds.DerivAtTop
 import TestingLowerBounds.ForMathlib.RadonNikodym
 import TestingLowerBounds.ForMathlib.RnDeriv
+-- TODO: remove this import after the next mathlib bump, now it is only needed for `ConvexOn.add_const`, but this lemma has recently been moved to `Mathlib.Analysis.Convex.Function`.
+import Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup
 
 /-!
 
@@ -143,9 +145,7 @@ lemma fDiv_congr (μ ν : Measure α) (h : ∀ x ≥ 0, f x = g x) :
   congr
   simp_rw [this]
 
--- TODO: finish the proof of `fDiv_of_eq_on_nonneg` and use it to shorten the proof of `fDiv_of_zero_on_nonneg`.
---the name feels a bit wrong, what could I write instead of `on_nonneg`?
-lemma fDiv_of_zero_on_nonneg (μ ν : Measure α) (hf : ∀ x ≥ 0, f x = 0) :
+lemma fDiv_eq_zero_of_forall_nonneg (μ ν : Measure α) (hf : ∀ x ≥ 0, f x = 0) :
     fDiv f μ ν = 0 := by
   have (x : α) : f ((∂μ/∂ν) x).toReal = 0 := hf _ ENNReal.toReal_nonneg
   rw [fDiv_of_integrable (by simp [this])]
@@ -363,6 +363,26 @@ lemma fDiv_add_linear {c : ℝ} [IsFiniteMeasure μ] [IsFiniteMeasure ν]
   rw [fDiv_add_linear' hf_cvx, h_eq, ← EReal.coe_sub, sub_self]
   simp
 
+lemma fDiv_eq_fDiv_centeredFunction [IsFiniteMeasure μ] [IsFiniteMeasure ν]
+    (hf_cvx : ConvexOn ℝ univ f) :
+    fDiv f μ ν = fDiv (fun x ↦ f x - f 1 - rightDeriv f 1 * (x - 1)) μ ν
+      + f 1 * ν univ + rightDeriv f 1 * ((μ univ).toReal - (ν univ).toReal) := by
+  simp_rw [sub_eq_add_neg (f _), sub_eq_add_neg (_ + _), ← neg_mul]
+  rw [fDiv_add_linear']
+  swap; · exact hf_cvx.subset (fun _ _ ↦ trivial) (convex_Ici 0) |>.add_const _
+  rw [fDiv_add_const]
+  swap; · exact hf_cvx.subset (fun _ _ ↦ trivial) (convex_Ici 0)
+  simp_rw [EReal.coe_neg, neg_mul]
+  rw [add_assoc, add_comm (_ * _), ← add_assoc, add_assoc _ (-(_ * _)), add_comm (-(_ * _)),
+    ← sub_eq_add_neg (_ * _), EReal.sub_self, add_zero]
+  rotate_left
+  · refine (EReal.mul_ne_top _ _).mpr ⟨?_, Or.inr <| EReal.add_top_iff_ne_bot.mp rfl,
+      ?_, Or.inr <| Ne.symm (ne_of_beq_false rfl)⟩ <;> simp
+  · refine (EReal.mul_ne_bot _ _).mpr ⟨?_, Or.inr <| EReal.add_top_iff_ne_bot.mp rfl,
+      ?_, Or.inr <| Ne.symm (ne_of_beq_false rfl)⟩ <;> simp
+  rw [add_assoc, add_comm (-(_ * _)), ← sub_eq_add_neg, EReal.sub_self, add_zero]
+    <;> simp [EReal.mul_ne_top, EReal.mul_ne_bot, measure_ne_top]
+
 lemma fDiv_of_mutuallySingular [SigmaFinite μ] [IsFiniteMeasure ν] (h : μ ⟂ₘ ν) :
     fDiv f μ ν = (f 0 : EReal) * ν Set.univ + derivAtTop f * μ Set.univ := by
   have : μ.singularPart ν = μ := (μ.singularPart_eq_self).mpr h
@@ -769,7 +789,7 @@ lemma fDiv_nonneg [IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
 some lemma like `derivAtTop_mono`, and I'm not sure this is true in gneral, without any assumption on `f`.
 We could prove it if we had some lemma saying that the new derivAtTop is equal to the old definition,
 this is probably false in general, but under some assumptions it should be true. -/
-lemma fDiv_mono' (hf_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν)
+lemma fDiv_mono'' (hf_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν)
     (hfg : f ≤ᵐ[ν.map (fun x ↦ ((∂μ/∂ν) x).toReal)] g) (hfg' : derivAtTop f ≤ derivAtTop g) :
     fDiv f μ ν ≤ fDiv g μ ν := by
   rw [fDiv_of_integrable hf_int, fDiv]
@@ -780,13 +800,14 @@ lemma fDiv_mono' (hf_int : Integrable (fun x ↦ f ((∂μ/∂ν) x).toReal) ν)
       ae_of_ae_map (Measure.measurable_rnDeriv μ ν).ennreal_toReal.aemeasurable hfg
   · exact EReal.coe_ennreal_nonneg _
 
-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 (eventually_of_forall hfg) hfg'
 
 lemma fDiv_nonneg_of_nonneg (hf : 0 ≤ f) (hf' : 0 ≤ derivAtTop f) :
     0 ≤ fDiv f μ ν :=
-  fDiv_zero μ ν ▸ fDiv_mono (integrable_zero α ℝ ν) hf (derivAtTop_zero ▸ hf')
+  fDiv_zero μ ν ▸ fDiv_mono' (integrable_zero α ℝ ν) hf (derivAtTop_zero ▸ hf')
 
 lemma fDiv_eq_zero_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν] (h_mass : μ Set.univ = ν Set.univ)
     (hf_deriv : derivAtTop f = ⊤) (hf_cvx : StrictConvexOn ℝ (Ici 0) f)

TestingLowerBounds/ForMathlib/EReal.lean

@@ -24,9 +24,6 @@ instance : NoZeroDivisors EReal where
     · rcases lt_or_gt_of_ne h.2 with (h | h)
         <;> simp [EReal.top_mul_of_pos, EReal.top_mul_of_neg, h]
 
-lemma eq_coe_of_ne_top_of_ne_bot {x : EReal} (hx : x ≠ ⊤) (hx' : x ≠ ⊥) : ∃ r : ℝ, x = r := by
-  induction x <;> tauto
-
 lemma coe_ennreal_toReal {x : ℝ≥0∞} (hx : x ≠ ∞) : (x.toReal : EReal) = x := by
   lift x to ℝ≥0 using hx
   rfl
@@ -301,12 +298,12 @@ lemma toReal_eq_zero_iff {x : EReal} : x.toReal = 0 ↔ x = 0 ∨ x = ⊤ ∨ x
   induction x <;> norm_num
 
 lemma sub_nonneg {x y : EReal} (hy : y ≠ ⊤) (hy' : y ≠ ⊥) : 0 ≤ x - y ↔ y ≤ x := by
-  obtain ⟨_, ha⟩ := eq_coe_of_ne_top_of_ne_bot hy hy'
-  induction x <;> simp [← EReal.coe_sub, ha]
+  lift y to ℝ using ⟨hy, hy'⟩
+  induction x <;> simp [← EReal.coe_sub]
 
 lemma sub_nonpos {x y : EReal} (hy : y ≠ ⊤) (hy' : y ≠ ⊥) : x - y ≤ 0 ↔ x ≤ y := by
-  obtain ⟨_, ha⟩ := eq_coe_of_ne_top_of_ne_bot hy hy'
-  induction x <;> simp [← EReal.coe_sub, ha]
+  lift y to ℝ using ⟨hy, hy'⟩
+  induction x <;> simp [← EReal.coe_sub]
 
 @[simp]
 lemma nsmul_eq_mul {n : ℕ} {x : EReal} : n • x = n * x := by

blueprint/src/sections/dpi_div.tex

@@ -93,7 +93,7 @@ \section{Generic divergences}
 
 
 \begin{lemma}[Conditioning increases divergence]
-  \label{lem:}
+  \label{lem:div_comp_le_div_compProd_right}
   %\lean{}
   %\leanok
   \uses{def:div, def:dpi}