[RemyDegenne]

This pull request proves the dual formula for the smallest relative entropy from a probability measure to a null generated by finitely many constraints, KL_inf, with no constraint qualification. It adds the file LMLExplore/EValues/ConstraintNull/KLInf.lean and the general files LMLExplore/Analysis/SpecialFunctions/Integrability/PosLog.lean and LMLExplore/MeasureTheory/Measure/MeasureSpaceDef.lean, and adds small lemmas to ConstraintNull/Basic.lean and ConstraintNull/CompleteClass.lean. It uses the statement merged in #416. The statements and the proof follow [EVR26, Note 20] (RemyDegenne/evalues_research), which the file cites.

The statements

For measurable constraints g : ι → 𝓧 → ℝ on any measurable space, the null constraintNull (range g) and its bets constraintBets g:

• maxUtility_constraintNull_eq_iSup_eintegral_log: for every finite measure Q, maxUtility Q (constraintNull (range g)) logUtility is the supremum over the bets π of ∫ᵉ x, ENNReal.log (ENNReal.ofReal (1 + ∑ i, π i * g i x)) ∂Q.
• iInf_klDiv_constraintNull_eq_maxUtility: for a probability measure Q under which every log⁺ |g i| is integrable, ⨅ P ∈ constraintNull (range g), klDiv Q P = maxUtility Q (constraintNull (range g)) logUtility.
• iInf_klDiv_constraintNull_eq_iSup_eintegral_log: the two together, the dual formula.

No member of the null is asked to satisfy the constraints strictly, the null may be empty, and both sides may be ⊤.

Supporting statements: noArbitrageOn_add_integral_div_of_lintegral_le (the constraints shifted by their means divided by the missing mass admit no arbitrage), exists_add_sum_smul_dirac_mem_constraintNull (on a set without arbitrage that carries the null, a finite measure under which every e-variable has mean at most c < 1 is completed into a member of the null by a finitely supported measure), iInf_klDiv_constraintNull_le_maxUtility_of_noArbitrageOn, maxUtility_constraintNull_le_iSup_eintegral_log_of_noArbitrageOn, iSup_eintegral_log_ofReal_one_add_eq_top.

Roadmap coverage (EValues, Layer 1, item 4)

Covered:

• in the bullet "Optimal bets", its last sentence (maxUtility Q (constraintNull Φ) logUtility is the supremum over the bets), for every finite Q, without Q ≪ constraintNull Φ;
• in the bullet "The dual formula for KL_inf", the two equalities, and the item's generalization "the dual formula of KL_inf for any finite set of measurable constraints on any measurable space".

The hypothesis differs from the roadmap's: the roadmap assumes Slater's condition (a probability measure P with klDiv Q P < ∞, the g i P-integrable and ∫ g i ∂P < 0), this pull request assumes that every log⁺ |g i| is Q-integrable. Slater's condition implies that hypothesis, by the Donsker–Varadhan inequality ∫ f ∂Q ≤ klDiv Q P + log ∫ exp f ∂P applied to f = log⁺ |g i|; this implication is not formalized here.

Left for later pull requests: the statement under Slater's condition as a corollary; that the supremum over the bets is attained, by a bet equal to the numeraire; the corollaries of the item ([HT15], [AJK21], [WSJ26], maxUtility_bernoulli).

Notes for reviewers

• The proof does not use the Lagrange duality of LMLExplore/Analysis/Convex/LagrangeDuality.lean, which needs Slater's condition. It compares both sides with maxUtility, which Statlib's numeraire attains, and splits along exists_measurableSet_noArbitrageOn_or_exists_sum_mul_pos. If a nonnegative combination of the constraints charges Q, its multiples are bets with unbounded expected logarithms. Otherwise Q is carried by a set Y without arbitrage; the measure with density 1 / E with respect to Q, for the numeraire E, is damped by 1 + δ ∑ i, |g i|, so that it integrates the constraints, scaled by 1 - ε, and completed into a member of the null by a finitely supported measure on Y. The completion applies the complete class theorem to the constraints shifted by multiples of their means. The relative entropy from Q to that member is at most maxUtility + E_Q[log (1 + δ ∑ i, |g i|)] - log (1 - ε), and δ, ε go to 0 by dominated convergence.
• The infimum of the relative entropies is taken in EReal, ⨅ P ∈ S, ((klDiv Q P : ℝ≥0∞) : EReal), since maxUtility is EReal-valued.
• iInf_klDiv_constraintNull_eq_maxUtility assumes [Finite κ] where the other statements assume [Fintype ι]: its statement contains no sum over the constraints.
• New general lemmas: Real.abs_log_one_add_mul_le, MeasureTheory.integrable_log_one_add_sum_abs, MeasureTheory.Integrable.log_one_add_const_mul, MeasureTheory.Integrable.tendsto_integral_log_one_add_mul (new file Analysis/SpecialFunctions/Integrability/PosLog.lean); MeasureTheory.exists_gt_measure_setOf_le_ne_zero (new file MeasureTheory/Measure/MeasureSpaceDef.lean); ProbabilityTheory.isFiniteMeasure_of_mem_constraintNull, ProbabilityTheory.toNNReal_mem_constraintBets (Basic.lean); ProbabilityTheory.IsEVar.exists_mem_constraintBets_le_of_noArbitrageOn (CompleteClass.lean), from which IsEVar.exists_mem_constraintBets_ae_le is now derived. No declaration is removed or renamed.
• The bound for fixed δ and ε, and four facts about the damped reverse information projection (its integrability of the constraints, its means, the logarithm of its likelihood ratio, its completion into a member of the null), are private.

Roadmap: EValues
Paper: RemyDegenne/evalues_research
Item: R15

🤖 Generated with Claude Code

https://claude.ai/code/session_0196ftMVbgjSJzPQEwdek3kM

[RemyDegenne]

🟡 reuse — request_changes claude/claude-opus-5-5

The Dirac-sum integral computation in exists_add_sum_smul_dirac_mem_constraintNull repeats the existing integral_sum_smul_dirac. Every other new declaration is new or reuses Mathlib's posLog and dominated-convergence lemmas.

• LMLExplore/EValues/ConstraintNull/KLInf.lean:194 — The proof rewrites with integral_finsetSum_measure (hdirac _ (hg i)) and then simp_rw [integral_smul_measure, integral_dirac' _ _ (hg i).stronglyMeasurable, ENNReal.toReal_ofReal ..., smul_eq_mul]. The hdirac helper (line 180) exists for that rewrite. Together they repeat the proof of LMLExplore.integral_sum_smul_dirac. Fix: Replace the rewrite chain with rw [integral_sum_smul_dirac (fun k ↦ mul_nonneg hm0.le (hw0 k)) (hg i).stronglyMeasurable]. Keep hdirac only for the integrability term, or inline it.

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 · 44s · 238.4k in (219.7k cache read, 18.8k cache write) / 3.7k 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	approved	claude/claude-opus-5-5	The dual formula iInf_klDiv_constraintNull_eq_iSup_eintegral_log matches the roadmap's iInf_klDiv_constraintNull_eq (Suggested.lean:158) in hypotheses (Real.posLog (g i x) integrable, i.e. log⁺|g i|), objects and klDiv argument order; the companion equalities and supporting lemmas have real hypotheses and conclusions, and degenerate cases (empty null, ⊤ on both sides, a combination positive on a set of positive Q-measure) are handled correctly.
🟡	reuse	changes requested	claude/claude-opus-5-5	The Dirac-sum integral computation in exists_add_sum_smul_dirac_mem_constraintNull repeats the existing integral_sum_smul_dirac. Every other new declaration is new or reuses Mathlib's posLog and dominated-convergence lemmas.
✅	scope	approved	claude/claude-opus-5-5	The PR proves the roadmap target EValues Layer 1 item 4, the dual formula for KL_inf under log⁺-integrability with no constraint qualification (README.md:446-469, Suggested.lean:155-164), and every added general lemma and the CompleteClass extraction are direct prerequisites of that one proof.
✅	attribution	approved	claude/claude-opus-5-5	KLInf.lean credits [EVR26, Note 20] and its EValuesResearch library for the statements and adapted proofs, [LRR26, Theorem 3.1] inline wherever the complete class theorem is used, [LRR25] for the numeraire and reverse information projection, and [HT15] for the special cases; the roadmap is credited only in the description. The new helper lemmas in PosLog.lean and MeasureSpaceDef.lean are routine and need no credit.
✅	api-design	approved	claude/claude-opus-5-5	The exported surface is minimal: the private declarations are specific to the damped reverse-information-projection proof, and the general lemmas are public in general files without duplicating Mathlib. There are no compatibility artifacts and no new public definitions that would need a characteristic API.
✅	generality	approved	claude/claude-opus-5-5	The public statements are at the natural level: the dual formula assumes the weaker log⁺-integrability instead of Slater's condition, every hypothesis is used, and special cases are derived from the general results rather than proved twice. The new general lemmas do not duplicate Mathlib and build on Real.posLog_sum and Real.log_one_add_le_posLog.
🟡	placement	changes requested	claude/claude-opus-5-5	File placement and imports are sound, but Real.abs_log_one_add_mul_le, a plain real-logarithm inequality, is in an integrability file instead of the existing log-bounds file LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean.
✅	naming	approved	claude/claude-opus-5-5	New public names describe their conclusions in the terminology of the sibling ConstraintNull files (constraintNull, constraintBets, maxUtility, noArbitrageOn) and match statement strength. Dot-notation lemmas sit in the Integrable/Real namespaces, the rest in the organisational ProbabilityTheory namespace like the siblings, and no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	Module docstrings of the three new files and the docstrings of every public declaration accurately describe their statements, hypotheses and sources; the CompleteClass header was updated for the new declaration. No overclaiming, process narrative or stale documentation found.
✅	proof-quality	approved	claude/claude-opus-5-5	Substantial reasoning is factored into separate lemmas (no-arbitrage shift, completion, damped-density facts, PosLog bounds), and the remaining long proofs carry comments explaining their structure. No proof uses change/show or undocumented definitional equality, and the rewrite chains are short and local.

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

_{Reviewing this diff at head 47fb2c7. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $3.12.}

[RemyDegenne]

🟡 placement — request_changes claude/claude-opus-5-5

File placement and imports are sound, but Real.abs_log_one_add_mul_le, a plain real-logarithm inequality, is in an integrability file instead of the existing log-bounds file LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean.

• LMLExplore/Analysis/SpecialFunctions/Integrability/PosLog.lean:41 — Real.abs_log_one_add_mul_le (|log (1 + δ t)| ≤ log (1 + t) for t ≥ 0, δ ∈ [0, 1]) has nothing to do with measures or integrability, yet it sits in an integrability file under namespace Real. Fix: Move it to LMLExplore/Analysis/SpecialFunctions/Log/Basic.lean, add it to that file's main-statements list, and import that module here.

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 · 34s · 184.3k in (170.5k cache read, 13.8k cache write) / 3.2k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}