[RemyDegenne]

This pull request generalizes one statement of LMLExplore/EValues/ConstraintNull/CompleteClass.lean (merged in #402): the measurable set without arbitrage that carries a null generated by finitely many constraints can be made to carry a given measure Q as well, unless a nonnegative combination of the constraints separates Q from the null. It changes that file only (49 lines added, 17 removed), adds one declaration and removes or renames none.

The statement

exists_measurableSet_noArbitrageOn_or_exists_sum_mul_pos: for measurable constraints g : ι → 𝓧 → ℝ with [Fintype ι] and any measure Q on 𝓧, one of the following holds.

• There is a measurable set Y with μ Yᶜ = 0 for every μ ∈ constraintNull (range g), Q Yᶜ = 0, and NoArbitrageOn g Y.
• There are weights ρ ≥ 0 such that ∑ i, ρ i * g i is nonnegative almost surely under every member of the null and under Q, and positive on a set of positive Q-measure.

exists_measurableSet_noArbitrageOn keeps its statement and is now the case Q = 0.

Why

The proof is the induction that was already there, on the dimension of the span of the values of the constraints on Y: each step removes the set where a nonnegative combination, nonnegative on Y, is positive. The new statement stops at the first removed set that Q charges. No second induction is added: the existing theorem is derived from the new one.

The alternative is what the dual formula for KL_inf needs when no constraint qualification is assumed (EValues, Layer 1, item 4, "The dual formula for KL_inf", and the remark "the dual formula of KL_inf for any finite set of measurable constraints on any measurable space"). For an alternative Q:

• in the second case, the multiples 1 + t ∑ i, ρ i * g i are bets with unbounded expected logarithms under Q, and both sides of the formula are ⊤;
• in the first case, Q is carried by Y, where the complete class theorem holds pointwise and e-variables are finite.

The dual formula itself is a separate pull request, to be opened once this one is merged: it needs this statement, and stacked pull requests are not allowed.

No open pull request changes LMLExplore/EValues/ConstraintNull/CompleteClass.lean. The open #415 adds a new file in the same folder and uses exists_measurableSet_noArbitrageOn, whose statement is unchanged.

Roadmap: EValues
Paper: RemyDegenne/evalues_research
Item: R37

🤖 Generated with Claude Code

https://claude.ai/code/session_0196ftMVbgjSJzPQEwdek3kM

[RemyDegenne]

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

The new theorem's name says it produces a nonzero measure, but Q is an input and what the statement produces is weights ρ whose combination is positive on a set that Q charges.

• LMLExplore/EValues/ConstraintNull/CompleteClass.lean:462 — In exists_measurableSet_noArbitrageOn_or_exists_measure_ne_zero, the suffix exists_measure_ne_zero reads as an existential over a nonzero measure. The statement actually quantifies over weights ρ : ι → ℝ and ends with Q {x | 0 < ∑ i, ρ i * g i x} ≠ 0 for the given Q. The module-doc bullet at line 70 repeats the name. Fix: Rename the existential after the sum, e.g. exists_measurableSet_noArbitrageOn_or_exists_measure_setOf_sum_mul_pos_ne_zero, or more briefly exists_measurableSet_noArbitrageOn_or_exists_sum_mul_pos, and update the module-doc bullet to match.

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 · 21s · 53.6k in (36.7k cache read, 16.9k cache write) / 1.9k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

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

The generalized induction is readable and has comments; the derived exists_measurableSet_noArbitrageOn closes its contradiction by an undocumented rfl that relies on the zero measure unfolding through its function coercion.

• LMLExplore/EValues/ConstraintNull/CompleteClass.lean:535 — exact absurd rfl h proves (0 : Measure 𝓧) {x | …} = 0 by rfl, which relies on the zero measure unfolding through its FunLike coercion rather than on a lemma. Fix: Replace the branch with simp at h (or exact absurd (by simp) h).

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 · 40s · 186.3k in (173.1k cache read, 13.2k cache write) / 2.9k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[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 new alternative is stated correctly and is not vacuous: ρ = 0 cannot satisfy the second disjunct, which together with the null constraints gives a separation of Q from the null, and the old theorem is recovered unchanged at Q = 0.
✅	reuse	approved	claude/claude-opus-5-5	The new theorem generalizes the existing induction, and exists_measurableSet_noArbitrageOn is now derived from it at Q = 0 instead of being proved separately. Grep found no existing Mathlib or LMLExplore declaration with this content, and the proof refactor removes the old duplicated hnn block.
✅	scope	approved	claude/claude-opus-5-5	This modestly generalizes the merged exists_measurableSet_noArbitrageOn into the alternative that the EValues roadmap (Layer 1.4, dual formula for KL_inf, README.md:458) explicitly asks for. It is one coherent unit in a single file.
✅	attribution	approved	claude/claude-opus-5-5	The new alternative is the file's existing induction stopped early at the first removed set that Q charges; it follows no separate identifiable source, and the file header already credits LRR26 as its central reference. The roadmap is credited only in the PR description, as required.
✅	api-design	approved	claude/claude-opus-5-5	The PR adds one public theorem; the old exists_measurableSet_noArbitrageOn remains as a genuine specialization (Q = 0) with in-file uses, not a compatibility shim. No new definitions, annotations, or visibility issues.
✅	generality	approved	claude/claude-opus-5-5	The general alternative is proved once by the existing induction, and exists_measurableSet_noArbitrageOn is derived as the Q = 0 case, so no proof is duplicated. Q is an arbitrary measure with no extra hypotheses, and it is the parameter the planned KL_inf dual formula needs.
✅	placement	approved	claude/claude-opus-5-5	The new theorem generalizes exists_measurableSet_noArbitrageOn and sits right before it in the same file (CompleteClass.lean), which is its natural home. The imports are unchanged, and no file or module is added or moved.
✅	naming	approved	claude/claude-opus-5-5	The new theorem's name describes its two-case conclusion in standard Mathlib terms and matches neighbouring names in CompleteClass.lean; no notation or namespace changes are introduced.
✅	documentation	approved	claude/claude-opus-5-5	The new theorem's docstring and the module-docstring additions (proof-sketch bullet, main-results entry) state exactly the two alternatives the theorem proves, without overclaiming. The retained exists_measurableSet_noArbitrageOn docstring remains accurate for its unchanged statement.
✅	proof-quality	approved	claude/claude-opus-5-5	The Q-alternative is added as one early by_cases exit in the existing induction, the nonnegativity fact hnn is factored out and reused, and the old theorem now follows from the new one at Q = 0 without a second induction. No defeq manipulation or brittle rewrite chains; the slightly-over-50-line proof keeps comments marking its steps.

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

_{Reviewing this diff at head 5964106. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $0.70.}