[RemyDegenne]

This pull request adds the null generated by a set of constraints and the bets on finitely many
constraints, with their basic API, and proves the complete class theorem of Larsson, Ramdas and
Ruf for finitely many constraints [LRR26, Theorem 3.1]. The theorem is proved in both of the
roadmap's forms: for real functions with nonpositive integrals, and for e-variables.

The proof does not use the paper's weak topology and bipolar theorem. It is finite-dimensional:

1. a set Y carrying the null, a measurable set that carries every member and on which the
   constraints admit no arbitrage, built by induction on the dimension of the span of the
   constraint vectors;
2. a separation step on finite subsets of Y, through geometric_hahn_banach_compact_closed;
3. a compactness argument with the nonredundant weights [LRR26, Lemma 3.2 and proof of Lemma 7.2].

Roadmap target

EValues, Layer 1, item 4, "Nulls generated by constraints and the dual formula for KL_inf".

Covered:

• the first bullet: the definitions constraintNull Φ and the bets Π g (constraintBets g) for
  finitely many constraints g : ι → 𝓧 → ℝ, [Fintype ι];
• the complete class part of the second bullet, for finitely many constraints, in both forms:
  • a measurable f has ∫ f ∂μ ≤ 0 for every μ ∈ constraintNull (range g) exactly when
    f ≤ ∑ i, π i * g i quasi-surely for some π ≥ 0. No integrability of f is assumed: the
    paper asks f ∈ L^Φ, but with the Bochner integral the equivalence holds without it;
  • the e-variables are the measurable functions that are quasi-surely dominated by a bet
    1 + ∑ i, π i * g i. In this form π is a bet (π ∈ constraintBets g), not only π ≥ 0.

Left for later pull requests:

• the rest of the second bullet: the admissible e-variables [LRR26, Corollary 3.3], the relaxed
  null [LRR26, Theorem 9.2], the pointwise form on a standard Borel space [Cle26b, Proposition 1]
  and arbitrary Φ [LRR26, Theorem 2.2];
• optimal bets, the dual formula for KL_inf, its corollaries, and infinitely many constraints.
  Lagrange duality, the other tool of the item, is already on main
  (Analysis/Convex/LagrangeDuality.lean).

Main declarations

LMLExplore/EValues/ConstraintNull/Basic.lean, in namespace ProbabilityTheory:

• constraintNull Φ [LRR26, Definition 2.1] and constraintBets g [LRR26, Corollary 3.3];
• membership and projections:
  • mem_constraintNull_iff, mem_constraintNull_range_iff;
  • isProbabilityMeasure_of_mem_constraintNull, integrable_of_mem_constraintNull,
    integral_nonpos_of_mem_constraintNull;
• constraintNull_anti (@[gcongr]), constraintNull_union, constraintNull_empty;
• the finitely supported members, for measurable constraints:
  • sum_smul_dirac_mem_constraintNull_iff, dirac_mem_constraintNull_iff;
  • sum_mul_nonpos_of_forall_integral_nonpos, sum_ofReal_mul_le_one_of_isEVar;
• the bets:
  • mem_constraintBets_iff, zero_mem_constraintBets, convex_constraintBets;
  • lintegral_ofReal_one_add_sum_mul, lintegral_ofReal_one_add_of_mem_constraintBets,
    lintegral_ofReal_one_add_le_one_of_mem_constraintBets;
  • isEVar_ofReal_one_add_of_mem_constraintBets (bets give e-variables).

LMLExplore/EValues/ConstraintNull/CompleteClass.lean, in namespace ProbabilityTheory:

• NoArbitrageOn a Y and nonredundantWeights a Y [LRR26, (3.1)], with
  isClosed_nonredundantWeights, smul_mem_nonredundantWeights,
  exists_mem_nonredundantWeights_sum_mul_eq [LRR26, Lemma 3.2],
  isCompact_nonredundantWeights_inter and exists_finset_sum_le_of_noArbitrageOn
  [LRR26, proof of Lemma 7.2];
• exists_mem_nonredundantWeights_le_of_noArbitrageOn: the finite-dimensional complete class
  theorem on a set without arbitrage, and exists_charging_family_of_noArbitrageOn;
• exists_measurableSet_noArbitrageOn: a measurable set carrying the null, without arbitrage;
• lt_top_of_isEVar_of_noArbitrageOn: e-variables are finite on the support;
• exists_mem_nonredundantWeights_le_of_forall_integral_nonpos and
  exists_mem_nonredundantWeights_toReal_le_of_isEVar: the domination on the support, with
  nonredundant weights;
• forall_integral_nonpos_iff_exists_ae_le, IsEVar.exists_mem_constraintBets_ae_le and
  isEVar_constraintNull_iff: the complete class theorem [LRR26, Theorem 3.1].

The later pull requests of the item reuse NoArbitrageOn, nonredundantWeights, the set carrying
the null and the compactness lemmas.

Notes for reviewers

• The definitions take [MeasurableSpace 𝓧] as an instance argument, since Φ : Set (𝓧 → ℝ)
  does not determine it.
• constraintNull asks no measurability of the constraints: integrability already contains almost
  everywhere strong measurability. The theorems that need measurable constraints assume it.
• No declaration is removed or renamed.

Roadmap: EValues
Paper: RemyDegenne/evalues_research
Item: R4

🤖 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	constraintNull, constraintBets and both forms of the complete class theorem match the roadmap's suggested statements and [LRR26, Def. 2.1, Cor. 3.3, Thm. 3.1], the e-variable form being slightly stronger (π is a bet). Dropping integrability of f is sound under the Bochner convention, and NoArbitrageOn and nonredundantWeights are used by the main theorems and are not vacuous.
✅	reuse	approved	claude/claude-opus-5-5	The constraint null, bets, no-arbitrage and nonredundant-weight material is new and builds on Mathlib's separation and compactness API and the existing LMLExplore LinearMap.prod_pi_apply_eq_sum_univ. The thin AE wrapper flagged in the prior round is gone, and integral_sum_smul_dirac is more general than Mathlib's integral_sum_dirac (no MeasurableSingletonClass or FiniteDimensional), so it does not duplicate it.
✅	scope	approved	claude/claude-opus-5-5	The PR defines constraintNull and constraintBets and proves LRR26 Theorem 3.1 in both forms, which are the first bullet and the Complete class part of EValues Layer 1 item 4 (roadmap README.md:381-401). Every helper lemma is used directly in those proofs, so this is one coherent topic.
✅	attribution	approved	claude/claude-opus-5-5	Both new ConstraintNull files credit [LRR26] (arXiv:2504.02974v5) and cite the exact results they follow (Definition 2.1, Corollary 3.3, (3.1), Lemma 3.2, proof of Lemma 7.2, Theorem 3.1); the departures from the paper are standard techniques and are disclosed in the module docstring, and the roadmap is credited only in the PR description.
✅	api-design	approved	claude/claude-opus-5-5	The characteristic API for constraintNull, constraintBets, NoArbitrageOn and nonredundantWeights is complete, bodies stay unexposed, general helpers are public in their natural homes and the one private lemma is specific to the proof. There are no compatibility artifacts, and no Mathlib duplicates turned up for the new general lemmas.
✅	generality	approved	claude/claude-opus-5-5	The constraint-null, bet and complete-class statements, and the helper lemmas (le_of_forall_nat_le_add_one_div at Mathlib's ExistsAddOfLE semifield level, integral_sum_smul_dirac without a MeasurableSingletonClass assumption), sit at the natural level. No hypotheses are unused or stronger than needed, and no proof is duplicated for a special case.
✅	placement	approved	claude/claude-opus-5-5	Generic helpers live in Mathlib-mirroring LMLExplore files (integral_sum_smul_dirac beside integral_weightedMeasure_eq_sum, which it generalises), and the roadmap-specific material lives in the new EValues/ConstraintNull/ directory. No import is evidently unused or unnecessarily broad.
✅	naming	approved	claude/claude-opus-5-5	Names describe their conclusions in standard Mathlib terminology, every _iff is a genuine Iff, and namespaces match the repo's precedent (root-namespace order lemmas as in Algebra/Order/Field/Basic.lean and Algebra/Order/Ring/Abs.lean, IsEVar.* dot notation, material filed under the organisational ProbabilityTheory namespace); no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	Each new or extended file has a module docstring describing its material and references, and every public definition and main theorem has an accurate docstring matching its statement, without overclaiming or process narrative.
✅	proof-quality	approved	claude/claude-opus-5-5	The long proofs are commented to explain their structure, reusable facts are split into helper lemmas, and there is no change/show or undocumented reliance on definitional equality.

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

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