[RemyDegenne]

This pull request proves that the bipolar rate equals the smallest relative entropy to the null when that relative entropy is lower semicontinuous at the alternative [RR26, Theorem 4.1]. It adds LMLExplore/EValues/BipolarRate/Semicontinuity.lean with the theorem, the general relative-entropy lemmas in LMLExplore/InformationTheory/KullbackLeibler/Pi.lean and .../KullbackLeibler/Cond.lean (namespace InformationTheory), the empirical-average lemmas in LMLExplore/Probability/LargeDeviations/EmpiricalAverage.lean, and two lemmas, le_bipolarRate_of_tendsto and le_maxLogGrowth_of_ofReal_exp_mul_le_one, to the existing LMLExplore/EValues/BipolarRate.lean.

The statement

bipolarRate_eq_iInf_klDiv_of_forall_exists_forall_le: for a probability measure Q and a set S of probability measures on any measurable space, if for every c : ℝ≥0∞ below ⨅ P ∈ S, klDiv Q P there are finitely many bounded measurable functions f i and ε > 0 such that every probability measure R with |∫ f i ∂R − ∫ f i ∂Q| ≤ ε for all i has c ≤ ⨅ P ∈ S, klDiv R P, then bipolarRate Q S = ⨅ P ∈ S, klDiv Q P.

The hypothesis is lower semicontinuity of R ↦ ⨅ P ∈ S, klDiv R P at Q, written with neighbourhoods, for the topology generated by the integrals of bounded measurable functions. That topology is finer than the topology of weak convergence, so the hypothesis of [RR26] (a Polish space and lower semicontinuity for weak convergence) implies it. No topology on the sample space is used.

Main declarations

• InformationTheory.sum_klDiv_map_eval_le, with InformationTheory.klDiv_fst_add_klDiv_snd_le: the relative entropy from a law on a finite product ∀ i, 𝓧 i to a product law Measure.pi P is at least the sum of the relative entropies of its marginals (from Statlib's maxUtility_fst_add_maxUtility_snd_le).
• InformationTheory.klDiv_cond_le: klDiv (μ[|A]) μ ≤ log (1 / μ A).
• ofReal_exp_mul_measure_pi_le_one: a Sanov-type bound. If every law whose integrals of the f i are within ε of a i is at relative entropy at least c from P, the probability under P ^ m that the empirical averages are within ε of the a i is at most exp (−m c) (Csiszár's conditioning argument [Csi84]). Helpers: isProbabilityMeasure_sum_smul_map_eval, integral_sum_smul_map_eval, abs_integral_sum_smul_map_eval_sub_le, integrable_comp_eval_of_abs_le, measurableSet_setOf_forall_abs_sum_div_sub_le.
• measure_pi_lt_abs_sum_div_sub_le: the weak law of large numbers for a square-integrable function g under Q ^ m, from Chebyshev's inequality, with the bound Var[g; Q] / (m ε ^ 2), and one_sub_div_le_measureReal_pi_forall_abs_sum_div_sub_le, its version for finitely many functions.
• le_maxLogGrowth_of_ofReal_exp_mul_le_one (in BipolarRate.lean): an event with null probability at most exp (−t) gives the m-sample e-variable 1/2 + (1/2) exp(t) 1_A and a lower bound on maxLogGrowth.
• le_bipolarRate_of_tendsto: a lower bound on the bipolar rate from lower bounds on maxLogGrowth.
• bipolarRate_eq_iInf_klDiv_of_forall_exists_forall_le: the theorem.

Roadmap coverage (EValues, Layer 6, item 1)

Covered: in the third bullet, d = KL_inf(Q₁, S₁) under lower semicontinuity of R ↦ KL_inf(R, S₁) at Q₁, in a form that needs no topology on 𝓧 and contains the weak-convergence case.

Left for later pull requests:

• the same statement written with LowerSemicontinuousAt on ProbabilityMeasure 𝓧 for the topology of weak convergence, and the case of a weakly compact null: both follow from the theorem here, by unfolding the neighbourhoods of the weak topology;
• the test supermartingale on blocks with rate KL_inf [RR26, Proposition 7.1], the strictness example [RR26, Proposition 5.4] and the convex weakly compact case [RR26, Proposition 4.5];
• the other bullets of item 1, and items 2 and 3.

This pull request shares no content with the open #399, #402 and #413.

Notes for reviewers

• The proof is a Sanov-type argument with blocks of length one, not the proof of [RR26]: condition P ^ m on the event that the empirical averages lie in the neighbourhood, use the superadditivity of the relative entropy over coordinates and its convexity to bound the probability of the event by exp (−m c), and turn the event into an m-sample e-variable.
• The theorem is stated with the ℝ≥0∞ infimum (⨅ P ∈ S, klDiv Q P : ℝ≥0∞), coerced to EReal, the form of the merged bipolarRate_le_iInf_klDiv, which gives the upper bound.

Roadmap: EValues
Paper: RemyDegenne/evalues_research
Item: R21

🤖 Generated with Claude Code

https://claude.ai/code/session_0196ftMVbgjSJzPQEwdek3kM

[RemyDegenne]

AI review — approved

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

⚠️ This review ran from a rubrics checkout that differs from the published rubrics (out of date, pinned, or locally edited), so its findings may reflect different rules.

	rubric	state	judge	summary
✅	correctness	approved	claude/claude-opus-5-5	The main theorem's hypothesis is lower semicontinuity at Q for the topology generated by integrals of bounded measurable functions, which is finer than the weak topology, so it implies [RR26, Theorem 4.1] and matches the on-main definitions of bipolarRate and maxLogGrowth. The helper lemmas (KL of a conditioned law, superadditivity over products, the Sanov-type bound, the Chebyshev WLLN, the indicator e-variable) state standard true facts with natural hypotheses, and none is vacuous or moves content into its assumptions.
✅	reuse	approved	claude/claude-opus-5-5	The earlier parallel API bipolarRate_le_iInf_coe_klDiv is gone, and the theorem now uses the existing bipolarRate_le_iInf_klDiv directly (Semicontinuity.lean:73). The new KL superadditivity, conditioning bound, Sanov-type bound and Chebyshev weak law build on Mathlib's meas_ge_le_variance_div_sq/variance_sum_pi and Statlib's maxUtility API, and I found no existing counterpart in Mathlib or LMLExplore (Statlib's source was not in the checkout to grep).
✅	scope	approved	claude/claude-opus-5-5	The PR proves the target statement of EValues Layer 6, item 1, third bullet (README.md:890-898): the bipolar rate equals KL_inf under neighbourhood lower semicontinuity, by the proof the roadmap outlines. Every helper (the Sanov-type bound, the KL superadditivity and conditioning lemmas, the weak law of large numbers, and the two BipolarRate lemmas) is a direct step of that proof, so the PR is one coherent unit.
✅	attribution	approved	claude/claude-opus-5-5	The PR credits [RR26, Theorem 4.1] for the theorem and now credits Csiszár [Csi84] in the code for the Sanov-type conditioning argument, which fixes the earlier finding. The Statlib declarations the proofs build on are named in the module docstrings.
✅	api-design	approved	claude/claude-opus-5-5	Prior findings are resolved: the duplicate EReal-form upper bound is gone, and the general relative-entropy and empirical-average lemmas now live in their own InformationTheory/Probability modules. The new surface is lemmas only, the one private helper is a proof-specific Fin step, and no definitions need characteristic API or annotations.
✅	generality	approved	claude/claude-opus-5-5	The earlier finding is fixed: sum_klDiv_map_eval_le now holds for any product law Measure.pi P over a finite index type. The other declarations are stated at a natural level, and their hypotheses (bounded test functions, 0 ≤ c, probability measures) are all used.
✅	placement	approved	claude/claude-opus-5-5	Each new declaration is now in its topic home: the relative-entropy lemmas in InformationTheory/KullbackLeibler/{Pi,Cond}.lean, the empirical-average lemmas in Probability/LargeDeviations/EmpiricalAverage.lean, the general bipolar-rate bounds in EValues/BipolarRate.lean, and only the theorem in BipolarRate/Semicontinuity.lean. No import is evidently unused or too broad.
✅	naming	approved	claude/claude-opus-5-5	The main theorem now states equality with the ℝ≥0∞ infimum, matching bipolarRate_le_iInf_klDiv, so the earlier iInf_klDiv naming clash is gone. The other new names describe their conclusions in standard Mathlib terms, sit in appropriate namespaces, and the PR adds no notation.
✅	documentation	approved	claude/claude-opus-5-5	All four new files have accurate module docstrings, and each public declaration's docstring matches its statement, including the hypotheses hm, 0 ≤ c and boundedness. The earlier finding on the e-variable in the implementation notes of Semicontinuity.lean is fixed.
✅	proof-quality	approved	claude/claude-opus-5-5	The earlier findings are resolved: the law of large numbers and the neighbourhood step are now separate lemmas, the long proofs carry structural comments, and the remaining rfl marginal identities are commented as holding by definition of piFinSuccAbove/piCongrLeft. The remaining proofs use short, robust automation steps.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head 880a8e9. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $3.14.}