[RemyDegenne]

This PR starts the EValues roadmap with its Layer 0.1 milestone, P-variables, tests and Markov's inequality [RW, Definition 1.2, Fact 1.3, Proposition 2.1]. It adds LMLExplore/EValues/EVariable.lean and LMLExplore/EValues/PVariable.lean, both in the namespace ProbabilityTheory next to Statlib's IsEVar, as the roadmap's Conventions ask. Nulls are arbitrary sets of measures and values are in ℝ≥0∞.

Here is how each item of the milestone is covered:

• IsPVar p S (P {ω | p ω ≤ α} ≤ α for every P ∈ S and α : ℝ≥0∞), exact p-variables IsExactPVar (= α for α ≤ 1) and exact e-variables IsExactEVar (∫⁻ E ∂P = P univ, which is = 1 for probability measures: IsExactEVar.lintegral_eq_one, isExactEVar_iff). P univ is used so that the definition matches Statlib's IsEVar, which asks ∫⁻ E ∂P ≤ P univ.
• Markov's inequality IsEVar.measure_inv_le_le (P {ω | α⁻¹ ≤ E ω} ≤ α, including α = 0 through IsEVar.ae_lt_top). From it come the e-to-p calibration IsEVar.isPVar_inv, the level-α test IsEVar.lintegral_indicator_le and IsEVar.lintegral_min_mul_le (∫⁻ min (α * E) 1 ∂P ≤ α).
• Finite products of e-variables that are independent under every P ∈ S are e-variables: isEVar_finsetProd, and the exact version isExactEVar_finsetProd. Statlib's IsEVar.prod is the case of the two coordinates of a product space. It stays where it is and is not restated.
• Completion-check API: measurability (the structure fields), monotonicity in the null (anti_set), congruence (congr) and composition with measurable maps (comp) for every new definition. For IsPVar there are also mono, union, isPVar_union_iff and the simple-null form isPVar_singleton_iff. There is also isEVar_iff_lintegral_le_one, the ∫⁻ form of Statlib's IsEVar for nulls of probability measures.
• Non-degenerate witnesses for the exactness predicates:
  • isExactEVar_rnDeriv: a likelihood ratio Q.rnDeriv P with Q ≪ P and Q univ = P univ is exact for {P}.
  • isExactPVar_ofReal_volume: the identity of [0, 1] under Lebesgue measure is an exact p-variable.
  • isExactPVar_ofReal_of_map_eq: so is every real random variable uniformly distributed on [0, 1], which Layer 0.3 (U / E) will consume.
  • IsExactPVar.ae_le_one.

Before writing, I checked for duplicates. I searched the pinned Mathlib, Tau Ceti, LML, Statlib and LMLExplore/ for p-variables (PVar, pValue, p-value), exact e-variables, and Markov-type bounds on IsEVar (⁻¹ ≤, meas_ge_le). Statlib's EValues/ has IsEVar, IsEVar.prod, IsEVar.comp, IsEVar.congr and IsEVar.ae_lt_top, which are consumed here, and nothing else on these topics. The proofs reuse Mathlib's meas_ge_le_lintegral_div, lintegral_prod_eq_prod_lintegral_of_indepFun with iIndepFun.precomp, Measure.lintegral_rnDeriv and Real.volume_Icc. No proof is longer than 25 lines. No public declaration is removed or renamed.

Milestone: EValues Layer 0.1. After this PR, nothing remains of Layer 0.1 (Statlib's IsEVar.prod cannot be re-derived here, since Statlib is a pinned dependency). The next milestones are Layer 0.2 (p-to-e calibrators, which consume IsPVar and isExactPVar_ofReal_volume) and Layer 0.3 (the randomized Markov inequality).

Roadmap: EValues

🤖 Prepared with Claude Code

[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	IsPVar, IsExactPVar and IsExactEVar match the roadmap's Layer 0.1 and RW Definition 1.2, and each has a non-trivial witness (rnDeriv, uniform on [0,1]). Markov, E⁻¹ calibration, the level-α tests and the independent-product theorems state the intended results with correct edge cases at α = 0 and α = ∞; the probability-measure assumptions are necessary (P = 2·δ, E = 1 breaks Markov for finite measures).
✅	reuse	approved	claude/claude-opus-5-5	The new p-variable, exact p-variable and exact e-variable APIs have no located duplicate in Mathlib, LMLExplore or the Statlib API listed in the roadmap, and the proofs reuse Mathlib's Markov, rnDeriv and independence lemmas. lintegral_prod_eq_prod_lintegral_of_indepFun' relaxes the all-factors-measurable hypothesis of Mathlib's lintegral_prod_eq_prod_lintegral_of_indepFun and is derived from it via iIndepFun.precomp.
✅	scope	approved	claude/claude-opus-5-5	The PR builds all of EValues Layer 0.1 (README.md:243-252) as one coherent unit: IsPVar, exact e- and p-variables, Markov's inequality and its consequences, and products of independent e-variables. Its extras (the product-expectation helper and the exactness witnesses) are direct prerequisites for Layer 0.1 itself or for the next milestones, Layers 0.2 and 0.3.
✅	attribution	approved	claude/claude-opus-5-5	Both e-value files cite Ramdas–Wang (Def. 1.2, Fact 1.3, Prop. 2.1), EVariable.lean also cites Vovk–Wang and Statlib's IsEVar/IsEVar.prod, and Integration.lean names the Mathlib lemma it generalizes. The roadmap is credited only in the PR description, as required.
✅	api-design	approved	claude/claude-opus-5-5	The public surface covers EValues Layer 0.1 (IsPVar, IsExactPVar, IsExactEVar, Markov, e-to-p calibration, independent finite products), and each predicate has anti_set/congr/comp and the probability-measure iff forms, with no private helpers, exposed bodies or compatibility artifacts. The general lemma lintegral_prod_eq_prod_lintegral_of_indepFun' is public and in its canonical file, mirroring Mathlib's Probability/Independence/Integration.lean.
✅	generality	approved	claude/claude-opus-5-5	Every hypothesis matches what its result needs: probability measures for Markov and the e-to-p calibration (as the roadmap's Suggested.lean signatures say), finiteness for the rnDeriv witness (needed for Statlib's eintegral_ne_bot field), and the finset-product helper weakens Mathlib's measurability assumption to the factors in s. Nothing duplicates a special case, and no abstraction lacks a use.
✅	placement	approved	claude/claude-opus-5-5	The e- and p-variable files are in the roadmap-suggested LMLExplore/EValues/, and the general independence lemma sits in LMLExplore/Probability/Independence/Integration.lean, next to the Mathlib module it extends. Every import is used by a declaration in its file and none is unnecessarily broad.
✅	naming	approved	claude/claude-opus-5-5	Names describe conclusions in standard Mathlib terminology (measure_inv_le_le, isPVar_inv, finsetProd as in Mathlib's coeFn_finsetProd), _iff/_eq match statement strength, and declarations sit in ProbabilityTheory alongside IsEVar. No notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	Each new file has a module docstring that describes its content and purpose, with mathematical references and no process narrative. The definitions and main theorems have accurate docstrings that match their statements without overclaiming.
✅	proof-quality	approved	claude/claude-opus-5-5	The earlier fragile simpa only in IsEVar.isPVar_inv is replaced by an explicit set equality (h_set) and a rewrite. The remaining proofs are short and robust, with no change/show or undocumented definitional-equality steps.

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

_{Reviewing this diff at head 54c7ed4. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $2.93.}