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

TestingLowerBounds.lean

@@ -19,13 +19,10 @@ import TestingLowerBounds.ForMathlib.ByParts
 import TestingLowerBounds.ForMathlib.CountableOrCountablyGenerated
 import TestingLowerBounds.ForMathlib.EReal
 import TestingLowerBounds.ForMathlib.Integrable_of_empty
-import TestingLowerBounds.ForMathlib.IntegralCongr2
-import TestingLowerBounds.ForMathlib.KernelConstComp
 import TestingLowerBounds.ForMathlib.KernelFstSnd
 import TestingLowerBounds.ForMathlib.LeftRightDeriv
 import TestingLowerBounds.ForMathlib.LogLikelihoodRatioCompProd
 import TestingLowerBounds.ForMathlib.MaxMinEqAbs
-import TestingLowerBounds.ForMathlib.Measure
 import TestingLowerBounds.ForMathlib.MonotoneOnTendsto
 import TestingLowerBounds.ForMathlib.RadonNikodym
 import TestingLowerBounds.ForMathlib.RnDeriv

TestingLowerBounds/CurvatureMeasure.lean

@@ -153,7 +153,7 @@ theorem convex_taylor (hf : ConvexOn ℝ univ f) (hf_cont : Continuous f) {a b :
   have hg : g = fun x ↦ x - b := rfl
   rw [← hg, integral_stieltjes_meas_by_parts g hf.rightDerivStieltjes]
   swap; · rw [hg]; fun_prop
-  simp only [Real.volume_eq_stieltjes_id, add_apply, id_apply, id_eq, const_apply, add_right_neg,
+  simp only [Real.volume_eq_stieltjes_id, add_apply, id_apply, id_eq, const_apply, add_neg_cancel,
     zero_mul, zero_sub, measure_add, measure_const, add_zero, neg_sub, sub_neg_eq_add, g]
   rfl
 

TestingLowerBounds/Divergences/Hellinger.lean

@@ -559,8 +559,8 @@ lemma hellingerDiv_symm' (ha_pos : 0 < a) (ha : a < 1) (h_eq : μ Set.univ = ν
   norm_cast
   simp_rw [mul_sub, ← mul_assoc]
   have : (1 - a) * (a - 1)⁻¹ = a * (-a)⁻¹ := by
-    rw [← neg_neg (1 - a), neg_sub, neg_mul, mul_inv_cancel, inv_neg, mul_comm, neg_mul,
-      inv_mul_cancel ha_pos.ne']
+    rw [← neg_neg (1 - a), neg_sub, neg_mul, mul_inv_cancel₀, inv_neg, mul_comm, neg_mul,
+      inv_mul_cancel₀ ha_pos.ne']
     linarith
   rw [integral_rpow_rnDeriv ha_pos ha.ne]
   congr
@@ -592,7 +592,7 @@ lemma meas_univ_add_mul_hellingerDiv_eq (ha_ne_zero : a ≠ 0) (ha_ne_one : a 
     ↑(ν Set.univ) + (a - 1) * hellingerDiv a μ ν = ∫ x, ((∂μ/∂ν) x).toReal ^ a ∂ν := by
   rw_mod_cast [hellingerDiv_eq_integral_of_ne_top' ha_ne_zero ha_ne_one h,
     ← ENNReal.ofReal_toReal (measure_ne_top ν Set.univ), EReal.coe_ennreal_ofReal,
-    max_eq_left ENNReal.toReal_nonneg, ← mul_sub, ← mul_assoc, mul_inv_cancel _]
+    max_eq_left ENNReal.toReal_nonneg, ← mul_sub, ← mul_assoc, mul_inv_cancel₀ _]
   ring_nf
   exact sub_ne_zero_of_ne ha_ne_one
 
@@ -624,7 +624,7 @@ lemma meas_univ_add_mul_hellingerDiv_nonneg_of_le_one (ha_nonneg : 0 ≤ a) (ha
       · exact hellingerDiv_le_of_lt_one ha_nonneg ha μ ν
     _ = (ν Set.univ) - (ν Set.univ) := by
       norm_cast
-      rw [← mul_assoc, ← EReal.coe_mul, mul_inv_cancel (by linarith), EReal.coe_one, one_mul]
+      rw [← mul_assoc, ← EReal.coe_mul, mul_inv_cancel₀ (by linarith), EReal.coe_one, one_mul]
     _ ≥ _ := by
       rw [← ENNReal.toEReal_sub (measure_ne_top _ _) (le_refl _)]
       simp

TestingLowerBounds/Divergences/KullbackLeibler.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne, Lorenzo Luccioli
 -/
 import TestingLowerBounds.FDiv.CondFDiv
-import TestingLowerBounds.ForMathlib.IntegralCongr2
 import TestingLowerBounds.ForMathlib.LogLikelihoodRatioCompProd
 
 /-!
@@ -586,7 +585,7 @@ lemma kl_compProd [CountableOrCountablyGenerated α β] [IsMarkovKernel κ] [IsM
       + log (Kernel.rnDeriv κ η a x).toReal ∂κ a ∂μ := by
     norm_cast
     have h := hμν.ae_le (Measure.ae_ae_of_ae_compProd (Kernel.rnDeriv_measure_compProd μ ν κ η))
-    apply integral_congr_ae₂
+    apply Kernel.integral_congr_ae₂
     filter_upwards [h, hκη, Measure.rnDeriv_toReal_pos hμν] with a ha hκηa hμν_pos
     have hμν_zero : (μ.rnDeriv ν a).toReal ≠ 0 := by linarith
     filter_upwards [Kernel.rnDeriv_toReal_pos hκηa, hκηa.ae_le ha] with x hκη_pos hx
@@ -618,7 +617,7 @@ lemma kl_compProd [CountableOrCountablyGenerated α β] [IsMarkovKernel κ] [IsM
       + ∫ a, ∫ x, log ((κ a).rnDeriv (η a) x).toReal ∂κ a ∂μ := by
     simp only [integral_const, measure_univ, ENNReal.one_toReal, smul_eq_mul, one_mul]
     congr 2
-    apply integral_congr_ae₂
+    apply Kernel.integral_congr_ae₂
     filter_upwards [hκη] with a ha
     have h := ha.ae_le (Kernel.rnDeriv_eq_rnDeriv_measure κ η a)
     filter_upwards [h] with x hx
@@ -640,7 +639,7 @@ lemma kl_compProd [CountableOrCountablyGenerated α β] [IsMarkovKernel κ] [IsM
 lemma kl_fst_add_condKL [StandardBorelSpace β] [Nonempty β] {μ ν : Measure (α × β)}
     [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
     kl μ.fst ν.fst + condKL μ.condKernel ν.condKernel μ.fst = kl μ ν := by
-  rw [← kl_compProd, μ.compProd_fst_condKernel, ν.compProd_fst_condKernel]
+  rw [← kl_compProd, μ.disintegrate, ν.disintegrate]
 
 /-TODO: this is just a thin wrapper around Kernel.integrable_llr_compProd_iff, so that that lemma
 could be put in an outside file. But I have realised that the choice of having 2 instead of 2' as

TestingLowerBounds/Divergences/Renyi.lean

@@ -108,7 +108,7 @@ lemma renyiDiv_zero_measure_left (ν : Measure α) [IsFiniteMeasure ν] :
   by_cases ha : a = 1
   · simp [ha]
   rw_mod_cast [renyiDiv_of_ne_one ha, hellingerDiv_zero_measure_left, ← mul_assoc, ← neg_sub a 1,
-    ← neg_inv, ← neg_mul_eq_mul_neg, mul_inv_cancel (sub_ne_zero.mpr ha)]
+    ← neg_inv, ← neg_mul_eq_mul_neg, mul_inv_cancel₀ (sub_ne_zero.mpr ha)]
   simp only [EReal.coe_neg, EReal.coe_one, neg_mul, one_mul, ← sub_eq_add_neg,
     EReal.sub_self_le_zero, EReal.toENNReal_of_nonpos, ENNReal.log_zero]
   rcases lt_or_gt_of_ne ha with (ha | ha)
@@ -322,10 +322,10 @@ lemma renyiDiv_symm' (ha_pos : 0 < a) (ha : a < 1) (h_eq : μ Set.univ = ν Set.
     hellingerDiv_symm' ha_pos ha h_eq
   have : (1 - (a : EReal)) * ↑(a - 1)⁻¹ = -1 := by
     norm_cast
-    rw [← neg_neg (1 - a), neg_sub, neg_mul, mul_inv_cancel]
+    rw [← neg_neg (1 - a), neg_sub, neg_mul, mul_inv_cancel₀]
     · simp
     · linarith
-  rw [this, ← EReal.coe_mul, inv_neg, mul_neg, mul_inv_cancel ha_pos.ne', h_eq]
+  rw [this, ← EReal.coe_mul, inv_neg, mul_neg, mul_inv_cancel₀ ha_pos.ne', h_eq]
   simp only [EReal.coe_neg, EReal.coe_one, one_mul]
   congr 4
   norm_cast
@@ -343,7 +343,7 @@ lemma coe_cgf_llr_of_lt_one (ha_pos : 0 < a) (ha : a < 1)
     [hν : NeZero ν] [IsFiniteMeasure μ] [IsFiniteMeasure ν] (hνμ : ν ≪ μ) :
     cgf (llr μ ν) ν a = (a - 1) * renyiDiv a μ ν := by
   rw_mod_cast [renyiDiv_eq_log_integral_of_lt_one ha_pos ha, ← mul_assoc,
-    mul_inv_cancel (by linarith), one_mul, cgf, mgf]
+    mul_inv_cancel₀ (by linarith), one_mul, cgf, mgf]
   have h_ms : ¬ μ ⟂ₘ ν :=
     fun h ↦ hν.out <| Measure.eq_zero_of_absolutelyContinuous_of_mutuallySingular hνμ h.symm
   rw [ENNReal.log_ofReal_of_pos]
@@ -370,7 +370,7 @@ lemma coe_cgf_llr' (ha_pos : 0 < a) [hν : NeZero μ] [IsFiniteMeasure μ] [IsFi
     (h_int : Integrable (fun x ↦ ((∂μ/∂ν) x).toReal ^ (1 + a)) ν) (hμν : μ ≪ ν) :
     cgf (llr μ ν) μ a = a * renyiDiv (1 + a) μ ν := by
   rw_mod_cast [renyiDiv_eq_log_integral' (by linarith) (by linarith) h_int hμν, ← mul_assoc,
-    add_sub_cancel_left, mul_inv_cancel ha_pos.ne', one_mul, cgf, mgf]
+    add_sub_cancel_left, mul_inv_cancel₀ ha_pos.ne', one_mul, cgf, mgf]
   have h_ms : ¬ μ ⟂ₘ ν :=
     fun h ↦ hν.out <| Measure.eq_zero_of_absolutelyContinuous_of_mutuallySingular hμν h
   rw [ENNReal.log_ofReal_of_pos _, integral_congr_ae (exp_mul_llr' hμν)]

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 TestingLowerBounds.ForMathlib.Indicator
 
 /-!
 # Statistical information

TestingLowerBounds/FDiv/Basic.lean

@@ -6,8 +6,6 @@ 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
 
 /-!
 
@@ -257,7 +255,7 @@ lemma fDiv_mul {c : ℝ} (hc : 0 ≤ c) (hf_cvx : ConvexOn ℝ (Ici 0) f)
       exact lt_of_le_of_ne hc (Ne.symm hc0)
     · refine fun h ↦ h_int ?_
       have : (fun x ↦ f ((∂μ/∂ν) x).toReal) = (fun x ↦ c⁻¹ * (c * f ((∂μ/∂ν) x).toReal)) := by
-        ext; rw [← mul_assoc, inv_mul_cancel hc0, one_mul]
+        ext; rw [← mul_assoc, inv_mul_cancel₀ hc0, one_mul]
       rw [this]
       exact h.const_mul _
 

TestingLowerBounds/FDiv/CompProd.lean

@@ -5,7 +5,7 @@ Authors: Rémy Degenne, Lorenzo Luccioli
 -/
 import TestingLowerBounds.FDiv.Basic
 import TestingLowerBounds.FDiv.IntegralRnDerivSingularPart
-import Mathlib.Probability.Kernel.Disintegration.Basic
+import Mathlib.Probability.Kernel.Disintegration.StandardBorel
 /-!
 
 # f-Divergences
@@ -183,7 +183,7 @@ lemma fDiv_compProd_left_eq_top_iff [IsFiniteMeasure μ] [IsFiniteMeasure ν]
   push_neg
   rfl
 
-lemma fDiv_compProd_right [CountableOrCountablyGenerated α β]
+lemma fDiv_compProd_right
     (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν]
     (κ : Kernel α β) [IsMarkovKernel κ] (hf : StronglyMeasurable f)
     (h_cvx : ConvexOn ℝ (Ici 0) f) :
@@ -207,9 +207,10 @@ lemma fDiv_compProd_right [CountableOrCountablyGenerated α β]
     · rw [← ne_eq, fDiv_ne_top_iff] at h_top
       exact h_top.1
 
-variable {γ : Type*} [MeasurableSpace γ]
+end CompProd
 
-lemma fDiv_toReal_eq_ae {ξ : Kernel α β} {κ η : Kernel (α × β) γ} [IsFiniteKernel κ]
+lemma fDiv_toReal_eq_ae {γ : Type*} [MeasurableSpace γ]
+    {ξ : Kernel α β} {κ η : Kernel (α × β) γ} [IsFiniteKernel κ]
     (hf_cvx : ConvexOn ℝ (Ici 0) f)
     (h_ac : derivAtTop f = ⊤ → ∀ᵐ a ∂μ, ∀ᵐ b ∂ξ a, κ (a, b) ≪ η (a, b))
     (h_int : ∀ᵐ a ∂μ, ∀ᵐ b ∂ξ a,
@@ -232,8 +233,6 @@ lemma fDiv_toReal_eq_ae {ξ : Kernel α β} {κ η : Kernel (α × β) γ} [IsFi
         Measure.measure_univ_pos, ne_eq, EReal.coe_ennreal_eq_top_iff, false_or, not_and]
       exact fun _ ↦ measure_ne_top _ _
 
-end CompProd
-
 end Conditional
 
 lemma f_rnDeriv_ae_le_integral [CountableOrCountablyGenerated α β]
@@ -550,8 +549,8 @@ lemma fDiv_fst_le [Nonempty β] [StandardBorelSpace β]
     (hf : StronglyMeasurable f)
     (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousOn f (Ici 0)) :
     fDiv f μ.fst ν.fst ≤ fDiv f μ ν := by
-  rw [← μ.compProd_fst_condKernel, ← ν.compProd_fst_condKernel, Measure.fst_compProd,
-    Measure.fst_compProd]
+  rw [← Measure.disintegrate μ μ.condKernel, ← Measure.disintegrate ν ν.condKernel,
+    Measure.fst_compProd, Measure.fst_compProd]
   exact le_fDiv_compProd μ.fst ν.fst μ.condKernel ν.condKernel hf hf_cvx hf_cont
 
 lemma fDiv_snd_le [Nonempty α] [StandardBorelSpace α]

TestingLowerBounds/FDiv/CondFDiv.lean

@@ -292,6 +292,8 @@ section CompProd
 /-! We show that the integrability of the functions used in `fDiv f (μ ⊗ₘ κ) (μ ⊗ₘ η)`
 and in `condFDiv f κ η μ` are equivalent. -/
 
+section
+
 variable [CountableOrCountablyGenerated α β]
 
 lemma condFDiv_ne_top_iff_fDiv_compProd_ne_top [IsFiniteMeasure μ]
@@ -332,6 +334,8 @@ lemma fDiv_compProd_left (μ : Measure α) [IsFiniteMeasure μ]
       EReal.coe_ennreal_toReal, Set.univ_prod_univ]
     exact measure_ne_top _ _
 
+end
+
 variable {γ : Type*} [MeasurableSpace γ]
 
 lemma condFDiv_snd'_toReal_eq_ae [CountableOrCountablyGenerated β γ] {ξ : Kernel α β}

TestingLowerBounds/ForMathlib/CountableOrCountablyGenerated.lean

@@ -9,6 +9,7 @@ lemma countable_left_of_prod_of_nonempty [Nonempty β] (h : Countable (α × β)
   contrapose h
   rw [not_countable_iff] at *
   infer_instance
+
 -- PRed, see #15418
 lemma countable_right_of_prod_of_nonempty [Nonempty α] (h : Countable (α × β)) : Countable β := by
   contrapose h
@@ -26,6 +27,7 @@ lemma countableOrCountablyGenerated_left_of_prod_left_of_nonempty [Nonempty β]
   · have := countable_left_of_prod_of_nonempty h
     infer_instance
   · infer_instance
+
 -- PRed, see #15418
 lemma countableOrCountablyGenerated_right_of_prod_left_of_nonempty [Nonempty α]
     [h : CountableOrCountablyGenerated (α × β) γ] :
@@ -64,8 +66,10 @@ lemma countableOrCountablyGenerated_left_of_prod_right_of_nonempty [Nonempty γ]
   · infer_instance
   · have := countablyGenerated_left_of_prod_of_nonempty h
     infer_instance
+
 -- PRed, see #15418
 instance [Countable (α × β)] : Countable (β × α) := Countable.of_equiv _ (Equiv.prodComm α β)
+
 -- PRed, see #15418
 instance [h : CountableOrCountablyGenerated (α × β) γ] :
     CountableOrCountablyGenerated (β × α) γ := by