[RemyDegenne]

This pull request describes the admissible e-variables of a null generated by finitely many measurable constraints [LRR26, Corollary 3.3], and proves that every e-variable is dominated by an admissible bet with no constraint qualification. It adds one new file, LMLExplore/EValues/ConstraintNull/Admissible.lean (281 lines), and changes no existing file. It builds on the complete class theorem merged in #402 and the admissible e-variables merged in #404.

Main declarations

For measurable constraints g : ι → 𝓧 → ℝ with [Fintype ι], the null constraintNull (range g) and its bets constraintBets g:

• IsAdmissibleEVar.exists_mem_constraintBets_ae_eq: every admissible e-variable is equal to a bet 1 + ∑ i, π i * g i, almost surely under every member of the null [LRR26, Corollary 3.3, first part].
• isAdmissibleEVar_ofReal_one_add_iff: a bet is admissible exactly when every bet whose combination of the constraints is at least its own, almost surely under every member of the null, has a combination at most its own.
• isAdmissibleEVar_ofReal_one_add_of_mem_constraintBets: under the constraint qualification of [LRR26, Corollary 3.3] (a nonnegative combination of the constraints that is at most another one, almost surely under every member of the null, is equal to it), every bet is admissible.
• isAdmissibleEVar_constraintNull_iff: under the constraint qualification, the admissible e-variables are the measurable functions equal to a bet almost surely under every member of the null.
• IsEVar.exists_mem_constraintBets_isAdmissibleEVar_ae_le: every e-variable is dominated by an admissible bet, with no constraint qualification.

Supporting statements:

• forall_ae_iff_of_noArbitrageOn: on a set Y without arbitrage that carries the null, a property holds almost surely under every member of the null exactly when it holds on Y; from exists_mem_constraintNull_measure_singleton_ne_zero, every point of Y is an atom of a member of the null.
• isCompact_nonredundantWeights_inter_nonneg: without arbitrage on Y, the nonredundant weights π with 1 + ∑ i, π i * a i nonnegative on Y form a compact set [LRR26, Lemma 7.2].
• exists_finset_forall_sum_mul_eq_zero: finitely many points of Y detect the combinations of the a i that vanish on Y.

Roadmap coverage (EValues, Layer 1, item 4)

Covered, in the bullet "Complete class": "characterize the admissible ones [LRR26, Corollary 3.3]", in both directions, and the compact set of [LRR26, Lemma 7.2] that the bullet "Optimal bets" uses.

Beyond the roadmap's wording, on the same target: the last main declaration. [LRR26, Theorem 6.5] proves that the bets form a minimal complete class under the constraint qualification, and [LRR26, Section 6] conjectures that minimal complete classes exist without it. By [LRR26, Lemma 6.2] a minimal complete class exists exactly when every e-variable is dominated by an admissible one, which is what IsEVar.exists_mem_constraintBets_isAdmissibleEVar_ae_le proves for finitely many constraints. The statement of [LRR26, Lemma 6.2] itself (complete classes as sets of e-variables, and their minimality) is not formalized here.

Left for later pull requests: the optimality of the dual class of properly constrained hypotheses [Cle24, Theorem 1] as a corollary, the relaxed null [LRR26, Theorem 9.2], the other bullets of item 4.

No open pull request touches LMLExplore/EValues/ConstraintNull/ or the admissible e-variables of a constraint null.

Notes for reviewers

• The domination by an admissible bet is not in [LRR26]. Its proof works on a measurable set Y that carries the null and on which the constraints admit no arbitrage (exists_measurableSet_noArbitrageOn, merged). The weights that have a nonredundant support, keep the bet nonnegative on Y and dominate on Y the weights given by the complete class theorem form a compact set; a maximizer of the sum of the combinations at finitely many points of Y that detect the combinations vanishing on Y is admissible: a bet that dominates it has, by [LRR26, Lemma 3.2] (exists_mem_nonredundantWeights_sum_mul_eq), weights in the compact set, so by maximality the two combinations agree at the detecting points, hence on Y.
• forall_ae_iff_of_noArbitrageOn assumes no measurability of the property: a point of Y is an atom of a finitely supported member of the null, and the measure of a set that contains an atom is positive for any set.
• The constraint qualification is written as a hypothesis, with weights in ℝ≥0 as in [LRR26, Corollary 3.3], and not as a definition.

Roadmap: EValues
Paper: RemyDegenne/evalues_research
Item: R36

🤖 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	All new statements match [LRR26, Corollary 3.3] and the stated domination result. The constraint qualification hypothesis is satisfiable non-trivially, and the supporting lemmas (atoms on Y, compactness, finitely many detecting points) are correctly stated, including when the null is empty.
✅	reuse	approved	claude/claude-opus-5-5	The new declarations are genuinely new and reuse Mathlib (Submodule.exists_finset_span_eq_linearIndepOn, Finset.sum_eq_sum_iff_of_le) and the existing complete-class API (isCompact_nonredundantWeights_inter, exists_charging_family_of_noArbitrageOn). The earlier hand-derived sum step now uses Finset.sum_eq_sum_iff_of_le.
✅	scope	approved	claude/claude-opus-5-5	The PR advances the EValues Layer 1 item 4 "Admissible bets" bullet, which lists every main statement here and the same proof route; the edits to CompleteClass.lean and the new finite-dimensional lemma file are prerequisites that proof uses directly. It is a single coherent topic.
✅	attribution	approved	claude/claude-opus-5-5	The new file and the additions to CompleteClass.lean cite [LRR26] for Corollary 3.3, Lemmas 3.2, 6.2 and 7.2, Theorem 6.5 and the Section 6 conjecture, and the new result is correctly marked as not taken from the paper. The linear-algebra helper is routine and needs no credit.
✅	api-design	approved	claude/claude-opus-5-5	The new surface consists only of theorems, with no definitions that would need a characteristic API or automation annotations. The general linear-algebra lemmas are public in a LinearAlgebra file, the constraint-null lemmas are public in their subject files, and there is no compatibility layer or exposed body.
✅	generality	approved	claude/claude-opus-5-5	The statements sit at their natural level: the linear-algebra lemmas are over a general field or ordered ring, the compactness lemma and the constraint-qualification hypothesis match their one use in the PR, and no special case duplicates a general proof.
✅	placement	approved	claude/claude-opus-5-5	The admissibility results sit in the existing ConstraintNull directory, the new no-arbitrage helpers sit in CompleteClass.lean next to the lemmas they build on, and the generic linear-algebra lemmas sit in LMLExplore/LinearAlgebra. No import is evidently unused or too broad.
✅	naming	approved	claude/claude-opus-5-5	New names are read from the conclusion, match adjacent declarations, claim no more than the statements prove, and sit in the correct namespaces; no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	Both new files have module docstrings that match their contents, and every new public theorem has an accurate docstring that promises no more than its statement; the minimal-complete-class remarks are worded as consequences of [LRR26, Lemma 6.2], not as claims proved here.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are short, use purpose-built lemmas, avoid change/show and defeq reliance, and the longest proof (~45 lines) is commented step by step. No proof-quality findings.

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

_{Reviewing this diff at head 2ae5b9c. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $1.80.}

[RemyDegenne]

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

The main statements sit at their natural level; one generic linear-algebra lemma carries field and linear-order assumptions its proof never uses.

• LMLExplore/LinearAlgebra/FiniteDimensional/Lemmas.lean:59 — forall_sum_mul_eq_of_forall_le_of_sum_le assumes [Field K] [LinearOrder K] [IsStrictOrderedRing K], but the proof only uses ring arithmetic and order (sub_mul, Finset.sum_sub_distrib, Finset.sum_eq_sum_iff_of_le, le_antisymm); the detecting property is a hypothesis, so no division or totality is needed. Fix: Weaken to [Ring K] [PartialOrder K] [IsOrderedRing K] (or [IsOrderedAddMonoid K]), keeping [Field K] only on exists_finset_forall_sum_mul_eq_zero, which needs spans over a field.

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 · 30s · 81.3k in (70.6k cache read, 10.7k cache write) / 2.3k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

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

Names describe their conclusions consistently with the adjacent ConstraintNull files and suffixes match statement strength, but the two new linear-algebra lemmas sit in the root namespace instead of LMLExplore.

• LMLExplore/LinearAlgebra/FiniteDimensional/Lemmas.lean:39 — exists_finset_forall_sum_mul_eq_zero is declared in the root namespace; it is not dot notation on a Lean/Mathlib type (first explicit argument is a plain function a : ι → 𝓧 → K), so it belongs in LMLExplore. Fix: Wrap the file's declarations in namespace LMLExplore … end LMLExplore; Admissible.lean already has open ... LMLExplore, so call sites are unaffected.
• LMLExplore/LinearAlgebra/FiniteDimensional/Lemmas.lean:61 — Same problem for forall_sum_mul_eq_of_forall_le_of_sum_le: it is in the root namespace, and its first explicit argument is a hypothesis, so this is not dot notation either. Fix: Move it into namespace LMLExplore together with the lemma above.

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 · 27s · 113.2k in (90.5k cache read, 22.7k cache write) / 2.2k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}