[RemyDegenne]

This pull request proves the two instances of the bipolar rate of Layer 6, item 1, of the EValues roadmap: on the circle with Lebesgue measure, a null against which one observation carries no evidence while the bipolar rate equals the smallest relative entropy log (1/ε), and a null whose bipolar rate is 0 while the smallest relative entropy is log (1/ε). It adds four new files, LMLExplore/EValues/BipolarRate/Circle.lean (355 lines), LMLExplore/EValues/BipolarRate/FiniteSupport.lean (241 lines), LMLExplore/InformationTheory/KullbackLeibler/Mixture.lean (79 lines) LMLExplore/MeasureTheory/Integral/IntervalIntegral/Periodic.lean (34 lines) and LMLExplore/EValues/Utility/Basic.lean (43 lines), and adds lemmas to two existing files, LMLExplore/MeasureTheory/Constructions/Pi.lean (+58 lines) and LMLExplore/EValues/EffectiveSet.lean (+12 lines). It removes and renames nothing.

Main declarations

• maxLogGrowth_one_coset_mixtures_eq_zero, bipolarRate_coset_mixtures, iInf_klDiv_coset_mixtures: for ε ≤ 1 and the null S = {(1 - ε) • uniformOn {x | x - x₀ ∈ AddSubgroup.zmultiples (((N : ℝ)⁻¹ : ℝ) : UnitAddCircle)} + ε • volume | (x₀ : UnitAddCircle) (N : ℕ)} on UnitAddCircle: maxLogGrowth volume S 1 = 0, bipolarRate volume S = ENNReal.log ε⁻¹, and ((⨅ P ∈ S, klDiv volume P : ℝ≥0∞) : EReal) = ENNReal.log ε⁻¹.
• maxLogGrowth_finitelySupported_mixtures_eq_zero, bipolarRate_finitelySupported_mixtures_eq_zero, iInf_klDiv_finitelySupported_mixtures: for any measurable space with measurable singletons, any probability measure Q, ε ≤ 1 and the null S = {(1 - ε) • F + ε • Q | (F : Measure 𝓧) (_ : IsProbabilityMeasure F) (_ : ∃ s : Set 𝓧, s.Finite ∧ F sᶜ = 0)}: maxLogGrowth Q S n = 0 for every n, bipolarRate Q S = 0, and, when Q has no atoms ([NullSingletonClass Q]), ((⨅ P ∈ S, klDiv Q P : ℝ≥0∞) : EReal) = ENNReal.log ε⁻¹.
• InformationTheory.klDiv_mixture_of_mutuallySingular: for probability measures μ, ν with ν ⟂ₘ μ and ε ≤ 1, ((klDiv μ ((1 - ε) • ν + ε • μ) : ℝ≥0∞) : EReal) = ENNReal.log ε⁻¹.
• ProbabilityTheory.maxUtility_eq_zero_of_mem_effectiveSet (in EffectiveSet.lean): for a probability measure P ∈ effectiveSet S, maxUtility P S logUtility = 0.
• In Pi.lean: MeasureTheory.Measure.pi_sum_smul (the product of finite mixtures ∑ k, w i k • μ i k is ∑ σ, (∏ i, w i (σ i)) • Measure.pi fun i ↦ μ i (σ i)), MeasureTheory.Measure.measurable_pi_comp (x ↦ Measure.pi fun i ↦ G i (x i) is measurable for measurable maps G i to finite measures) and MeasureTheory.Measure.pi_bind_pi ((Measure.pi μ).bind (fun x ↦ Measure.pi fun i ↦ G i (x i)) = Measure.pi fun i ↦ (μ i).bind (G i)).
• ProbabilityTheory.Utility.eintegral_comp_indicator_const (in EValues/Utility/Basic.lean, mirroring Statlib's EValues/Utility/Basic.lean): under a probability measure μ with μ Aᶜ = 0, ∫ᵉ x, (U ∘ A.indicator fun _ ↦ c) x ∂μ = U c for every utility U. It is the shared last step of klDiv_mixture_of_mutuallySingular and of the lower bound on the coset bipolar rate.
• An instance NullSingletonClass (volume : Measure (AddCircle T)), in MeasureTheory/Integral/IntervalIntegral/Periodic.lean, next to Mathlib's file of the same path where AddCircle.volume_closedBall lives. Mathlib does not infer it: its Haar-measure instance IsAddHaarMeasure.nullSingletonClass needs (𝓝[≠] 0).NeBot, which is not an instance on AddCircle.

Roadmap coverage (EValues, Layer 6, item 1)

Covered: the bullet "The inequality d ≤ KL_inf(Q₁, S₁) can be strict [RR26, Proposition 5.4], and one observation may carry no evidence when d = KL_inf(Q₁, S₁) > 0. Instances on the circle …": both instances. For the coset null, a 1 = 0 and d = KL_inf(Q₁, S₁) = log (1/ε). For the finitely supported null, d = 0 and KL_inf(Q₁, S₁) = log (1/ε), stated for any Q₁ and derived on the circle with Q₁ = volume (see below).

Left: [RR26, Proposition 5.4] itself and the other bullets of item 1. The two instances have no published source: the roadmap cites them [EVR26, Note 19]. The proofs here are their Lean proofs from the paper project, restated as described below.

Notes for reviewers

• The nulls are written in the statements, not defined. They are examples that no later target uses. Writing each set in the statements lets a reader check it against the roadmap without unfolding a definition, and adds no public definition that would need its own mem_*_iff API. The cost is that each set appears in its three statements. The proofs use private lemmas about one member, or about any null whose members have the properties the proof uses.
• The coset x₀ + (1/N) ℤ is written {x | x - x₀ ∈ AddSubgroup.zmultiples (((N : ℝ)⁻¹ : ℝ) : UnitAddCircle)}, and U is Mathlib's uniformOn. Since 0⁻¹ = 0, N = 0 gives the point x₀, as N = 1 does, so N needs no constraint.
• Generality and deviations from the roadmap's wording.
  • ε ≤ 1 instead of ε ∈ (0, 1]: for ε = 0 the bipolar rate and the smallest relative entropy of the coset null are both ⊤. For the finitely supported null, d = 0 and KL_inf = ⊤. The proofs cover this case.
  • The finitely supported null is stated for any probability measure Q on a measurable space with measurable singletons, since the proof uses nothing about the circle. The bound d = 0 holds for every such Q, and is proved in the stronger form maxLogGrowth Q S n = 0 for every n. The value log (1/ε) of the smallest relative entropy needs Q without atoms. The roadmap's instance is Q = volume on UnitAddCircle, with the NullSingletonClass instance of this pull request.
  • The smallest relative entropy is ⨅ P ∈ S, klDiv Q P in ℝ≥0∞, coerced to EReal to compare it with ENNReal.log ε⁻¹, as in bipolarRate_le_iInf_klDiv and the open feat: n observations are worth n times one when one observation attains the smallest relative entropy #421.
• How the proofs go.
  • a 1 = 0 for the coset null: Lebesgue measure is the average over x of the members (1 - ε) δ_x + ε volume (N = 1), so it lies in the effective null, and maxUtility_eq_zero_of_mem_effectiveSet (Jensen's inequality) applies.
  • The smallest relative entropies come from klDiv_mixture_of_mutuallySingular, whose proof is Statlib's variational form maxUtility_singleton_eq_klDiv: an e-variable for the mixture has mean at most 1/ε under μ, and ε⁻¹ times the indicator of a set charged by μ alone is an e-variable.
  • The lower bound on the coset bipolar rate: tuples with pairwise irrational differences have probability 1 under volume ^ n and at most n ε ^ (n - 1) under the n-fold product of a member. So their indicator divided by n ε ^ (n - 1) is an n-sample e-variable, with expected logarithm (n - 1) log (1/ε) - log n. The upper bound is bipolarRate_le_iInf_klDiv.
  • d = 0 for the finitely supported null: with G z = (1 - ε) δ_z + ε Q, the uniform mixture of the G (y k) over y : Fin m → 𝓧 is a member of the null. Its n-fold product expands along the maps σ : Fin n → Fin m (pi_sum_smul). For an injective σ, the average over y of Q ^ m of the products of the G (y (σ i)) is Q ^ n, by Statlib's Measure.pi_map_comp_of_injective and pi_bind_pi. Hence every n-sample e-variable has mean at most m ^ n / (m (m - 1) ⋯ (m - n + 1)) under Q ^ n for every m, so at most 1.
• Changes to existing files. Pi.lean is the canonical home of the three product lemmas. It gains the imports Mathlib.MeasureTheory.Measure.GiryMonad (public) and TauCeti.MeasureTheory.Integral.Pi (private, for TauCeti.lintegral_fintype_prod_eq_prod). EffectiveSet.lean gains one theorem at its end and one bullet in its docstring.
• Overlap with open pull requests. No declaration is shared, and no private copy was needed.
  • The open feat: merging functions for independent e-values, and for two e-values functions that no generalized martingale or precise merging function dominates #426 also edits Pi.lean: it adds Fin 2 integrals after end MeasureTheory.Measure and the same TauCeti.MeasureTheory.Integral.Pi import. Whichever lands second will have small textual conflicts in the imports, the docstring list and the end of the file, with no mathematical overlap.
  • The open feat: identifying numeraires through the effective null #410 edits EffectiveSet.lean in other places.
  • The open feat: nulls dense in total variation have the e-variables of all laws, and the mean-zero null has no power #432 proves maxLogGrowth Q S n = 0 from Q ^ n ∈ effectiveSet inline through the duality; maxUtility_eq_zero_of_mem_effectiveSet gives that step without hypotheses on S.
  • The open feat: e-processes for an i.i.d. null grow at most at the bipolar rate in expectation [RR26, Lemma 3.3] #413 moves LMLExplore/EValues/BipolarRate.lean to LMLExplore/EValues/BipolarRate/Basic.lean. If it lands first, the imports of Circle.lean and FiniteSupport.lean must follow, as for Semicontinuity.lean and feat: n observations are worth n times one when one observation attains the smallest relative entropy #421's SingleLetter.lean.
  • The open feat: n observations are worth n times one when one observation attains the smallest relative entropy #421 (SingleLetter.lean) is not needed.
• Not proved here. The module docstring of Circle.lean notes that, for ε < 1, the smallest relative entropy is not lower semicontinuous at volume for the topology of integrals of bounded measurable functions, so that bipolarRate_eq_iInf_klDiv_of_forall_exists_forall_le does not apply. That fact is stated as not proved here.
• Differences from the source theorems (EValuesResearch/Results/RateVersusKL.lean, commit dd4072f, credited in the module docstrings of Circle.lean, FiniteSupport.lean, Mixture.lean, Pi.lean and in the docstring of maxUtility_eq_zero_of_mem_effectiveSet):
  • The source defines cosetLaw, cosetNull and finiteSupportNull, and states each null's results as a conjunction. Here the sets are inline and each result is its own theorem.
  • The coset law is Mathlib's uniformOn of the coset written with zmultiples, instead of an average of Dirac masses over Finset.range N with 0 < N.
  • The source's finitely supported null is on the circle only, with F carried by a Finset. Here it is on any space, with F carried by a finite Set.
  • The source's general helpers are restated in more general forms and placed in their canonical homes: products of mixtures for dependent families, measurability for finite measures, the relative entropy to a mixture through ⟂ₘ, and the maximal expected logarithm through the effective null. The source's reindexing lemma is replaced by Statlib's Measure.pi_map_comp_of_injective, its count of injective maps by Fintype.card_embedding_eq, and its probability instance for the circle by Tau Ceti's.

Roadmap: EValues
Paper: RemyDegenne/evalues_research
Item: R35

🤖 Generated with Claude Code

https://claude.ai/code/session_0196ftMVbgjSJzPQEwdek3kM

[RemyDegenne]

🟡 proof-quality — request_changes claude/claude-opus-5-5

Several steps in Circle.lean and FiniteSupport.lean are long named-lemma rw chains that a single simp call would make robust to Mathlib renames. The argument that the infimum of a constant klDiv over the null equals that constant is written out twice instead of being factored into one lemma.

• LMLExplore/EValues/BipolarRate/Circle.lean:300 — Brittle eight-lemma rwa [measure_univ, uniformOn_coset_one, lintegral_add_measure, lintegral_smul_measure, lintegral_smul_measure, lintegral_dirac, smul_eq_mul, smul_eq_mul] at h. The same pattern recurs at line 305 (rw [lintegral_add_right _ measurable_const, lintegral_const_mul _ hX.measurable, lintegral_const, measure_univ, mul_one, add_mul]), at line 351 (rw [add_apply, smul_apply, (uniformOn_eq_zero_iff ..).2 .., smul_zero, zero_add, smul_apply, smul_eq_mul]) and in the cast chains of log_inv_le_bipolarRate (lines ~220-233). Fix: Replace each chain with one simpa [uniformOn_coset_one, lintegral_add_measure] using h / simp [lintegral_add_right, lintegral_const_mul, add_mul] / simp [(uniformOn_eq_zero_iff (finite_coset x₀ N)).2 (Set.inter_compl_self _)]-style call, keeping only the non-simp lemmas explicit.
• LMLExplore/EValues/BipolarRate/FiniteSupport.lean:205 — Brittle six-lemma chain rw [ENNReal.ofReal_div_of_pos .., ENNReal.ofReal_natCast, ENNReal.ofReal_pow .., ENNReal.ofReal_natCast, div_eq_mul_inv, ENNReal.inv_pow] used to move the descFactorial limit from ℝ to ℝ≥0∞. Fix: Close the cast step with simp [ENNReal.ofReal_div_of_pos, ENNReal.ofReal_pow, div_eq_mul_inv, ENNReal.inv_pow] or push_cast, or state the limit directly in ℝ≥0∞ through ENNReal.tendsto_toReal_iff-style transfer.
• LMLExplore/EValues/BipolarRate/Circle.lean:328 — The proof that the infimum of klDiv over the null equals a constant (rw [← hkl ..]; congr 1; refine (biInf_congr ?_).trans (biInf_const ⟨..⟩); ... EReal.coe_ennreal_injective (...)) is written out twice. The second copy is in iInf_klDiv_finitelySupported_mixtures at FiniteSupport.lean:241. Fix: Factor a lemma, e.g. (∀ P ∈ S, ((f P : ℝ≥0∞) : EReal) = c) → S.Nonempty → ((⨅ P ∈ S, f P : ℝ≥0∞) : EReal) = c, next to klDiv_mixture_of_mutuallySingular in Mixture.lean, and use it in both theorems.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5-5 · 43s · 135.1k in (90.5k cache read, 44.6k cache write) / 4.3k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

AI review — changes requested

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	stale (re-run pending) (approved in @RemyDegenne's review of 1b9be11)	—
♻️	reuse	stale (re-run pending) (approved in @RemyDegenne's review of 1b9be11)	—
♻️	scope	stale (re-run pending) (approved in @RemyDegenne's review of 1b9be11)	—
♻️	attribution	stale (re-run pending) (approved in @RemyDegenne's review of 1b9be11)	—
♻️	api-design	stale (re-run pending) (approved in @RemyDegenne's review of 1b9be11)	—
♻️	generality	stale (re-run pending) (approved in @RemyDegenne's review of 1b9be11)	—
♻️	placement	stale (re-run pending) (approved in @RemyDegenne's review of 1b9be11)	—
♻️	naming	stale (re-run pending) (approved in @RemyDegenne's review of 1b9be11)	—
♻️	documentation	stale (re-run pending) (approved in @RemyDegenne's review of 1b9be11)	—
🟡	proof-quality	changes requested	claude/claude-opus-5-5	Several steps in Circle.lean and FiniteSupport.lean are long named-lemma rw chains that a single simp call would make robust to Mathlib renames. The argument that the infimum of a constant klDiv over the null equals that constant is written out twice instead of being factored into one lemma.

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

_{Reviewing this diff at head 496c1e6. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $0.33.}