RemyDegenne · Oct 29, 2026 · Oct 29, 2026
diff --git a/Statlib.lean b/Statlib.lean
@@ -2,7 +2,10 @@ import Statlib.Causal.PotentialResponse
 import Statlib.Contiguity.Def
 import Statlib.Divergence.BretagnolleHuber
 import Statlib.Divergence.Chernoff
+import Statlib.Divergence.Chernoff.Prod
+import Statlib.Divergence.Chernoff.Properties
 import Statlib.Divergence.FDiv.Basic
+import Statlib.Divergence.FDiv.Binary
 import Statlib.Divergence.FDiv.CompProd
 import Statlib.Divergence.FDiv.CondFDiv
 import Statlib.Divergence.FDiv.Conj
@@ -14,25 +17,50 @@ import Statlib.Divergence.FDiv.DivFunction.CurvatureMeasure
 import Statlib.Divergence.FDiv.DivFunction.DerivAtTop
 import Statlib.Divergence.FDiv.DivFunction.OfReal
 import Statlib.Divergence.FDiv.DivFunction.RightDerivStieltjes
+import Statlib.Divergence.FDiv.Estimation
 import Statlib.Divergence.FDiv.IntegralRepresentation
 import Statlib.Divergence.FDiv.Measurable
+import Statlib.Divergence.FDiv.SupRatio
 import Statlib.Divergence.FDiv.Trim
+import Statlib.Divergence.FDiv.TrimApprox
 import Statlib.Divergence.Hellinger.Basic
 import Statlib.Divergence.Hellinger.CondHellinger
 import Statlib.Divergence.Hellinger.HellingerDivFun
 import Statlib.Divergence.Hellinger.HellingerFun
+import Statlib.Divergence.Hellinger.Prod
+import Statlib.Divergence.Hellinger.Renyi
+import Statlib.Divergence.Hellinger.TotalVariation
+import Statlib.Divergence.JensenShannon.Basic
+import Statlib.Divergence.JensenShannon.Hellinger
+import Statlib.Divergence.JensenShannon.Variational
 import Statlib.Divergence.KullbackLeibler.Basic
 import Statlib.Divergence.KullbackLeibler.CondKL
+import Statlib.Divergence.KullbackLeibler.Estimation
+import Statlib.Divergence.KullbackLeibler.Event
 import Statlib.Divergence.KullbackLeibler.KLDivFun
+import Statlib.Divergence.MutualInformation.Basic
+import Statlib.Divergence.MutualInformation.Bool
+import Statlib.Divergence.MutualInformation.Estimation
+import Statlib.Divergence.MutualInformation.LeftRight
 import Statlib.Divergence.Renyi.Basic
 import Statlib.Divergence.Renyi.Bernoulli
+import Statlib.Divergence.Renyi.ChainRule
 import Statlib.Divergence.Renyi.CondRenyi
+import Statlib.Divergence.Renyi.DataProcessing
+import Statlib.Divergence.Renyi.Order
+import Statlib.Divergence.Renyi.Order.Limits
+import Statlib.Divergence.Renyi.Prod
+import Statlib.Divergence.Renyi.ProdCountable
 import Statlib.Divergence.Renyi.Variational
 import Statlib.Divergence.StatInfo.Basic
+import Statlib.Divergence.StatInfo.CurvatureMeasure
+import Statlib.Divergence.StatInfo.Event
 import Statlib.Divergence.StatInfo.FDiv
 import Statlib.Divergence.StatInfo.StatInfoDivFun
 import Statlib.Divergence.StatInfo.StatInfoFun
 import Statlib.Divergence.TotalVariation
+import Statlib.Divergence.TotalVariation.Event
+import Statlib.Divergence.TotalVariation.Integral
 import Statlib.EValues.Bernoulli
 import Statlib.EValues.DPI
 import Statlib.EValues.Divergence
@@ -46,37 +74,81 @@ import Statlib.EValues.RIPr
 import Statlib.EValues.Utility.Basic
 import Statlib.EValues.Utility.Log
 import Statlib.ForMathlib.Analysis.Calculus.LocalExtr.Basic
+import Statlib.ForMathlib.Analysis.Convex.Deriv
 import Statlib.ForMathlib.Analysis.Convex.DerivAtTop
 import Statlib.ForMathlib.Analysis.SpecialFunctions.Log.Basic
+import Statlib.ForMathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp
+import Statlib.ForMathlib.Analysis.SpecialFunctions.Pow.Deriv
+import Statlib.ForMathlib.Analysis.SpecialFunctions.Pow.NNReal
+import Statlib.ForMathlib.Analysis.SpecialFunctions.Pow.Real
 import Statlib.ForMathlib.Convex
 import Statlib.ForMathlib.ENNReal
 import Statlib.ForMathlib.EReal
 import Statlib.ForMathlib.ISup
 import Statlib.ForMathlib.InformationTheory.KullbackLeibler.Basic
 import Statlib.ForMathlib.InformationTheory.KullbackLeibler.Bernoulli
+import Statlib.ForMathlib.InformationTheory.KullbackLeibler.ChainRule
 import Statlib.ForMathlib.InformationTheory.KullbackLeibler.DataProcessing
 import Statlib.ForMathlib.InformationTheory.KullbackLeibler.EIntegral
+import Statlib.ForMathlib.MeasureTheory.Constructions.Pi
+import Statlib.ForMathlib.MeasureTheory.Function.ConditionalLExpectation
 import Statlib.ForMathlib.MeasureTheory.Integral.EReal.Bochner
 import Statlib.ForMathlib.MeasureTheory.Integral.EReal.EIntegrable
 import Statlib.ForMathlib.MeasureTheory.Integral.EReal.EIntegral
 import Statlib.ForMathlib.MeasureTheory.Integral.EReal.Kernel
 import Statlib.ForMathlib.MeasureTheory.Integral.EReal.Prod
+import Statlib.ForMathlib.MeasureTheory.Integral.Layercake
+import Statlib.ForMathlib.MeasureTheory.Integral.MeanInequalities
+import Statlib.ForMathlib.MeasureTheory.Integral.Pi
 import Statlib.ForMathlib.MeasureTheory.Komlos
+import Statlib.ForMathlib.MeasureTheory.MeasurableSpace.Basic
 import Statlib.ForMathlib.MeasureTheory.Measure.Bool
+import Statlib.ForMathlib.MeasureTheory.Measure.Decomposition.Hahn
 import Statlib.ForMathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
 import Statlib.ForMathlib.MeasureTheory.Measure.Decomposition.IntegralRPowRNDeriv
+import Statlib.ForMathlib.MeasureTheory.Measure.Decomposition.RNDerivProd
+import Statlib.ForMathlib.MeasureTheory.Measure.Decomposition.RNDerivTrim
 import Statlib.ForMathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
 import Statlib.ForMathlib.MeasureTheory.Measure.ERealStieltjes
 import Statlib.ForMathlib.MeasureTheory.Measure.Lebesgue.Basic
 import Statlib.ForMathlib.MeasureTheory.Measure.LogLikelihoodRatio
+import Statlib.ForMathlib.MeasureTheory.Measure.Prod
+import Statlib.ForMathlib.MeasureTheory.Measure.Real
+import Statlib.ForMathlib.MeasureTheory.Measure.Trim
+import Statlib.ForMathlib.MeasureTheory.Measure.Typeclasses.Probability
+import Statlib.ForMathlib.MeasureTheory.Measure.Typeclasses.SFinite
 import Statlib.ForMathlib.MeasureTheory.Order.Group.Lattice
 import Statlib.ForMathlib.Probability.Decision.BayesEstimator
+import Statlib.ForMathlib.Probability.Decision.Risk.Basic
+import Statlib.ForMathlib.Probability.Decision.Risk.RiskIncrease
+import Statlib.ForMathlib.Probability.Decision.ZeroOneLoss
 import Statlib.ForMathlib.Probability.Distributions.Bernoulli
+import Statlib.ForMathlib.Probability.Kernel.Basic
+import Statlib.ForMathlib.Probability.Kernel.Composition.Lemmas
 import Statlib.ForMathlib.Probability.Kernel.Composition.MeasureCompProd
 import Statlib.ForMathlib.Probability.Kernel.Composition.RadonNikodym
+import Statlib.ForMathlib.Probability.Kernel.Posterior
+import Statlib.ForMathlib.Probability.Moments.Variance
+import Statlib.ForMathlib.Probability.Process.Filtration
+import Statlib.ForMathlib.Probability.Process.PartitionFiltration
+import Statlib.ForMathlib.Probability.Process.Stopping
+import Statlib.ForMathlib.Probability.ProductMeasure
+import Statlib.ForMathlib.Probability.StrongLaw
 import Statlib.ForMathlib.Topology.Order.MonotoneConvergence
 import Statlib.Inference.Inference
 import Statlib.Inference.QMD
 import Statlib.Testing.Binary
+import Statlib.Testing.BinaryRenyi
 import Statlib.Testing.ChangeMeasure
+import Statlib.Testing.ChangeMeasureMoments
+import Statlib.Testing.ChangeMeasureRisk
+import Statlib.Testing.Chernoff
+import Statlib.Testing.Fano
+import Statlib.Testing.Hellinger
 import Statlib.Testing.RenyiChangeMeasure
+import Statlib.Testing.SampleComplexity
+import Statlib.Testing.SampleComplexityBounds
+import Statlib.Testing.Sequential.Basic
+import Statlib.Testing.Sequential.KLDiv
+import Statlib.Testing.Sequential.Renyi
+import Statlib.Testing.Sequential.Wald
diff --git a/Statlib/Divergence/Chernoff.lean b/Statlib/Divergence/Chernoff.lean
@@ -17,16 +17,21 @@ public import Statlib.Divergence.Renyi.Basic
 
 ## Main statements
 
+* `chernoffDiv_comm`: the Chernoff divergence is symmetric.
+* `chernoffDiv_zero_measure_left`, `chernoffDiv_zero_measure_right`: the Chernoff divergence
+  between the zero measure and any measure is infinite.
 * `chernoffDiv_one`: the Chernoff divergence of order `1` as an infimum of Kullback-Leibler
   divergences.
+* `chernoffDiv_smul_smul`, `chernoffDiv_eq_chernoffDiv_inv_smul`: invariance under scaling of the
+  measures.
 
 This file is adapted from the testing-lower-bounds project of Rémy Degenne and Lorenzo Luccioli
 (https://github.com/RemyDegenne/testing-lower-bounds).
 -/
 
 @[expose] public section
 
-open Real MeasureTheory InformationTheory
+open MeasureTheory InformationTheory
 
 open scoped ENNReal
 
@@ -40,6 +45,22 @@ of order `a` from `ξ` to `μ` and from `ξ` to `ν`. -/
 noncomputable def chernoffDiv (a : ℝ) (μ ν : Measure α) : ℝ≥0∞ :=
   ⨅ (ξ : Measure α) (_hξ : IsProbabilityMeasure ξ), max (renyiDiv a ξ μ) (renyiDiv a ξ ν)
 
+/-- The Chernoff divergence is symmetric. -/
+lemma chernoffDiv_comm (a : ℝ) (μ ν : Measure α) : chernoffDiv a μ ν = chernoffDiv a ν μ := by
+  simp_rw [chernoffDiv, max_comm]
+
+/-- The Chernoff divergence between the zero measure and any measure is infinite. -/
+@[simp]
+lemma chernoffDiv_zero_measure_left (ha : 0 ≤ a) (ν : Measure α) : chernoffDiv a 0 ν = ∞ :=
+  iInf₂_eq_top.mpr fun ξ _ ↦ by rw [renyiDiv_zero_measure_right ha ξ, max_eq_left le_top]
+
+/-- The Chernoff divergence between any measure and the zero measure is infinite. -/
+@[simp]
+lemma chernoffDiv_zero_measure_right (ha : 0 ≤ a) (μ : Measure α) : chernoffDiv a μ 0 = ∞ := by
+  rw [chernoffDiv_comm, chernoffDiv_zero_measure_left ha]
+
+/-- For probability measures, the Chernoff divergence of order `1` is the infimum over probability
+measures `ξ` of `max (KL(ξ, μ)) (KL(ξ, ν))`. -/
 lemma chernoffDiv_one [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] :
     chernoffDiv 1 μ ν
       = ⨅ (ξ : Measure α) (_hξ : IsProbabilityMeasure ξ), max (klDiv ξ μ) (klDiv ξ ν) := by
@@ -48,4 +69,24 @@ lemma chernoffDiv_one [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] :
   congr with hξ
   rw [renyiDiv_one_of_isProbabilityMeasure, renyiDiv_one_of_isProbabilityMeasure]
 
+/-- The Chernoff divergence is invariant under scaling of the measures by positive finite
+constants. -/
+lemma chernoffDiv_smul_smul (ha : 0 ≤ a) [IsFiniteMeasure μ] [IsFiniteMeasure ν] {c c' : ℝ≥0∞}
+    (hc : c ≠ 0) (hc_top : c ≠ ∞) (hc' : c' ≠ 0) (hc'_top : c' ≠ ∞) :
+    chernoffDiv a (c • μ) (c' • ν) = chernoffDiv a μ ν :=
+  iInf_congr fun _ ↦ iInf_congr fun _ ↦ by
+    rw [renyiDiv_smul_right' ha hc hc_top, renyiDiv_smul_right' ha hc' hc'_top]
+
+/-- The Chernoff divergence between finite measures is the Chernoff divergence between the
+normalized measures. -/
+lemma chernoffDiv_eq_chernoffDiv_inv_smul (ha : 0 ≤ a) [IsFiniteMeasure μ] [IsFiniteMeasure ν] :
+    chernoffDiv a μ ν = chernoffDiv a ((μ .univ)⁻¹ • μ) ((ν .univ)⁻¹ • ν) := by
+  rcases eq_zero_or_neZero μ with rfl | _
+  · simp [ha]
+  rcases eq_zero_or_neZero ν with rfl | _
+  · simp [ha]
+  exact (chernoffDiv_smul_smul ha (ENNReal.inv_ne_zero.mpr (measure_ne_top _ _))
+    (ENNReal.inv_ne_top.mpr (NeZero.ne _)) (ENNReal.inv_ne_zero.mpr (measure_ne_top _ _))
+    (ENNReal.inv_ne_top.mpr (NeZero.ne _))).symm
+
 end ProbabilityTheory
diff --git a/Statlib/Divergence/Chernoff/Prod.lean b/Statlib/Divergence/Chernoff/Prod.lean
@@ -0,0 +1,77 @@
+/-
+Copyright (c) 2026 Rémy Degenne. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Rémy Degenne
+-/
+module
+
+public import Statlib.Divergence.Chernoff
+public import Statlib.Divergence.Renyi.Prod
+
+/-!
+# Chernoff divergence of product measures
+
+The Chernoff divergence `Cₐ(μ, ν) = ⨅ ξ, max (Rₐ(ξ, μ)) (Rₐ(ξ, ν))` is subadditive on finite
+products of finite measures: taking product measures `∏ ξ i` in the infimum and using the
+tensorization of the Rényi divergence (`renyiDiv_pi`) gives
+`Cₐ(∏ μ i, ∏ ν i) ≤ ∑ i, Cₐ(μ i, ν i)`.
+
+## Main statements
+
+* `ProbabilityTheory.chernoffDiv_pi_le`: `Cₐ(∏ μ i, ∏ ν i) ≤ ∑ i, Cₐ(μ i, ν i)` for `0 ≤ a` and
+  finite measures.
+* `ProbabilityTheory.chernoffDiv_pi_const_le`: `Cₐ(μ^⊗ι, ν^⊗ι) ≤ |ι| * Cₐ(μ, ν)`.
+-/
+
+@[expose] public section
+
+open MeasureTheory
+
+open scoped ENNReal
+
+namespace ProbabilityTheory
+
+variable {α : Type*} {mα : MeasurableSpace α} {μ ν : Measure α} {a : ℝ}
+
+/-- **Subadditivity of the Chernoff divergence on products**: for `0 ≤ a` and finite measures,
+`Cₐ(∏ μ i, ∏ ν i) ≤ ∑ i, Cₐ(μ i, ν i)`. -/
+theorem chernoffDiv_pi_le (ha : 0 ≤ a) {ι : Type*} [Fintype ι] {β : ι → Type*}
+    [∀ i, MeasurableSpace (β i)] {μ ν : (i : ι) → Measure (β i)} [∀ i, IsFiniteMeasure (μ i)]
+    [∀ i, IsFiniteMeasure (ν i)] :
+    chernoffDiv a (Measure.pi μ) (Measure.pi ν) ≤ ∑ i, chernoffDiv a (μ i) (ν i) := by
+  -- for `ε > 0`, choose for each `i` a probability measure `ξ i` which is `ε / |ι|`-optimal in the
+  -- infimum defining `Cₐ(μ i, ν i)`, and use the product measure `∏ ξ i`
+  refine ENNReal.le_of_forall_pos_le_add fun ε hε h_lt ↦ ?_
+  have h_ex i : ∃ ξ : Measure (β i), ∃ _ : IsProbabilityMeasure ξ,
+      max (renyiDiv a ξ (μ i)) (renyiDiv a ξ (ν i))
+        < chernoffDiv a (μ i) (ν i) + ε / Fintype.card ι := by
+    have h_ne : chernoffDiv a (μ i) (ν i) ≠ ∞ :=
+      (ENNReal.sum_lt_top.mp h_lt i (Finset.mem_univ i)).ne
+    simpa only [chernoffDiv, iInf_lt_iff] using ENNReal.lt_add_right h_ne
+      (ENNReal.div_pos (by simpa using hε.ne') (ENNReal.natCast_ne_top _)).ne'
+  choose ξ hξ h_lt_ξ using h_ex
+  calc chernoffDiv a (Measure.pi μ) (Measure.pi ν)
+      ≤ max (renyiDiv a (Measure.pi ξ) (Measure.pi μ)) (renyiDiv a (Measure.pi ξ) (Measure.pi ν)) :=
+        iInf₂_le (Measure.pi ξ) (by infer_instance)
+    _ = max (∑ i, renyiDiv a (ξ i) (μ i)) (∑ i, renyiDiv a (ξ i) (ν i)) := by
+        rw [renyiDiv_pi ha, renyiDiv_pi ha]
+    _ ≤ ∑ i, max (renyiDiv a (ξ i) (μ i)) (renyiDiv a (ξ i) (ν i)) :=
+        max_le (Finset.sum_le_sum fun _ _ ↦ le_max_left _ _)
+          (Finset.sum_le_sum fun _ _ ↦ le_max_right _ _)
+    _ ≤ ∑ i, (chernoffDiv a (μ i) (ν i) + ε / Fintype.card ι) :=
+        Finset.sum_le_sum fun i _ ↦ (h_lt_ξ i).le
+    _ ≤ ∑ i, chernoffDiv a (μ i) (ν i) + ε := by
+        rw [Finset.sum_add_distrib, Finset.sum_const, Finset.card_univ, nsmul_eq_mul]
+        gcongr
+        exact ENNReal.mul_div_le
+
+/-- **Subadditivity of the Chernoff divergence on powers**: for `0 ≤ a` and finite measures,
+`Cₐ(μ^⊗ι, ν^⊗ι) ≤ |ι| * Cₐ(μ, ν)`. -/
+theorem chernoffDiv_pi_const_le (ha : 0 ≤ a) {ι : Type*} [Fintype ι] [IsFiniteMeasure μ]
+    [IsFiniteMeasure ν] :
+    chernoffDiv a (Measure.pi fun _ : ι ↦ μ) (Measure.pi fun _ : ι ↦ ν)
+      ≤ Fintype.card ι * chernoffDiv a μ ν := by
+  simpa [Finset.sum_const, nsmul_eq_mul] using
+    chernoffDiv_pi_le ha (μ := fun _ : ι ↦ μ) (ν := fun _ : ι ↦ ν)
+
+end ProbabilityTheory