[RemyDegenne]

This PR proves the randomized Markov inequality and the randomized e-to-p calibration, closing EValues Layer 0.3 (The randomized Markov inequality [RW, Theorem 2.9, Corollary 2.10; RM26, Theorem 1.2]).

For a measurable Y : Ω → ℝ≥0∞ and U uniform on [0, 1] and independent of Y under P, measure_ofReal_le_mul_eq_lintegral_min proves P {U ≤ α * Y} = ∫⁻ min (α * Y) 1 ∂P, and IsPVar.measure_le_mul_le_mul_lintegral proves ≤ α * ∫⁻ Y ∂P. Both are stated for any p-variable p in place of U, an inequality P {p ≤ Z} ≤ ∫⁻ min Z 1 ∂P (IsPVar.measure_le_le_lintegral_min) that is an equality for exact p-variables (IsExactPVar.measure_le_eq_lintegral_min). The uniform variable is then the exact p-variable isExactPVar_ofReal_of_map_eq, which is already on main. Two consequences follow. The randomized e-test {p ≤ α * E} has level α (IsEVar.measure_le_mul_le). And p / E is a p-variable for a p-variable and an e-variable that are independent under every member of the null (IsEVar.isPVar_div), and so is U / E (IsEVar.isPVar_ofReal_div), with no truncation and the ℝ≥0∞ conventions p / 0 = ∞, p / ∞ = 0. These are [RW, Corollary 2.10].

The proof freezes the independent variable. A new general lemma ProbabilityTheory.IndepFun.measure_prodMk_mem_eq_lintegral (in LMLExplore/Probability/Independence/Basic.lean) states that for a.e.-measurable X, Y independent under a finite measure, μ {(X, Y) ∈ s} = ∫⁻ ω, μ {ω' | (X ω', Y ω) ∈ s} ∂μ. It follows from Mathlib's IndepFun.map_prod_eq_prod_map_map and Measure.prod_apply_symm. PVariable.lean gains two lemmas: IsExactPVar.measure_le_eq_min (the distribution function of an exact p-variable is min α 1) and isProbabilityMeasure_of_map_eq_volume_restrict_Icc. The second one means the uniform-variable statements need no separate IsProbabilityMeasure hypothesis.

Files: LMLExplore/EValues/RandomizedMarkov.lean (new, 165 lines), LMLExplore/Probability/Independence/Basic.lean (new, 51 lines), LMLExplore/EValues/PVariable.lean (+21). No declarations are removed or renamed. No Mathlib infrastructure is vendored. The mathematical sources are [RW] (Ramdas–Wang, arXiv:2410.23614v6, Theorem 2.9 and Corollary 2.10) and [RM26] (Ramdas–Manole, arXiv:2304.02611v3, Theorem 1.2), cited in the module docstring.

After this PR, Layer 0.3 has nothing left. Its consumer is the randomized Ville inequality of Layer 2.3 [RM26, Corollary 4.1.1], the sequential form of the same randomized threshold.

Quality pass:

• Duplicates in Mathlib, Tau Ceti, Statlib, LML and LMLExplore: checked. I grepped for randomized or uniformly randomized Markov, for IndepFun lemmas computing measures or lower integrals by freezing (IndepFun/lintegral/prodMk), and for p-variable division lemmas. I found nothing; the open PRs (feat: the exact Ville identity, the extended Ville inequality and Ville's inequality in ℝ≥0∞ #399, feat: e-processes, the definition IsEProcess and its first closure properties #401, feat: nulls generated by constraints, their bets, and the complete class theorem for finitely many constraints #402, feat: admissible e-variables, strong admissibility, and the simple null #404, feat: the discrete-time Snell envelope of an ℝ≥0∞-valued process #405, feat: e-merging functions, their domination by weighted means, and the admissible ones #409) do not touch Layer 0.3.
• Hypotheses: IsProbabilityMeasure P is dropped from the uniform statements because it follows from P.map U = volume.restrict (Icc 0 1). IndepFun is kept in IsEVar.isPVar_div. Counterexample: with p = U and E = 2 · 𝟙{U ≤ 1/2} (an e-variable), p / E ≤ 1/4 holds on {U ≤ 1/2}, which has probability 1/2 > 1/4.
• declined: hS : ∀ P ∈ S, IsProbabilityMeasure P is kept in IsEVar.isPVar_div, as in the neighbouring IsEVar.isPVar_inv. Independence alone only forces P univ ∈ {0, 1, ∞}, and Statlib's IsEVar gives no bound ∫⁻ E ∂P ≤ 1 under an infinite measure. Removing hS would need a separate argument for that case.
• Proof length: checked. No proof is over 15 lines.

Local checks (not CI): scope: scoped: against a890e2a10db9833d692cc4872b4b9114e3605534. local-axioms: checked 3 changed module(s), 53 declaration(s); 0 violation(s). Whole-library lake build succeeded; the module-system, header-style and environment lint checks passed.

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	All new statements faithfully formalize RW Theorem 2.9/Corollary 2.10 and RM26 Theorem 1.2; the freezing lemma is the correct Tonelli identity and the ℝ≥0∞ edge cases (E = 0, E = ∞, α = ∞) in IsEVar.isPVar_div are handled soundly.
✅	reuse	approved	claude/claude-opus-5-5	No Mathlib or LMLExplore declaration matches the new freezing lemma, the min-form distribution function of exact p-variables, or the randomized Markov and calibration results. The new code builds on IndepFun.map_prod_eq_prod_map_map, Measure.prod_apply_symm, Measure.isProbabilityMeasure_of_map, IsEVar.lintegral_min_mul_le and isExactPVar_ofReal_of_map_eq rather than re-deriving them.
✅	scope	approved	claude/claude-opus-5-5	The PR proves EValues Layer 0.3 as specified (README.md:270-274; the stub at Suggested.lean:85 matches measure_ofReal_le_mul_eq_lintegral_min up to its name) along with its stated p / E and U / E deductions. The independence-freezing lemma and the two PVariable lemmas are prerequisites used directly in those proofs, so the PR is one coherent topic.
✅	attribution	approved	claude/claude-opus-5-5	The module and theorem docstrings credit the central sources [RW, Theorem 2.9, Corollary 2.10] and [RM26, Theorem 1.2] with arXiv versions, matching the roadmap's Layer 0.3 citation; the roadmap is credited only in the PR description's Roadmap line. The freezing lemma is a routine Tonelli argument whose docstring names the Mathlib lemma it builds on.
✅	api-design	approved	claude/claude-opus-5-5	The general freezing lemma is public in a general independence module, the private helper is a one-line case specific to this file, and the new p-variable lemmas fit the existing exact-p-variable and uniform-law API. No definitions, exposed bodies, annotations or compatibility artifacts are at issue.
✅	generality	approved	claude/claude-opus-5-5	The prior AEMeasurable finding is fixed: IndepFun.measure_prodMk_mem_eq_lintegral now takes AEMeasurable hypotheses like the Mathlib lemma it wraps. The uniform-variable results are derived from the general p-variable lemmas, and hS matches IsEVar.isPVar_inv and the IsProbabilityMeasure hypothesis of IsEVar.lintegral_min_mul_le.
✅	placement	approved	claude/claude-opus-5-5	Each new declaration is in its natural home: the independence lemma in Probability/Independence/Basic.lean, matching Mathlib's file that holds IndepFun.map_prod_eq_prod_map_map; the p-variable and uniform-law lemmas next to their neighbours in PVariable.lean; and the randomized Markov results in a new EValues file with no clashing sibling names. Both new imports are used and narrow.
✅	naming	approved	claude/claude-opus-5-5	The uniform-variable identity is now measure_ofReal_le_mul_eq_lintegral_min, which fixes the earlier missing-ofReal finding. All new names describe their conclusions, use _eq/_le correctly, match the neighbouring IsEVar/IsPVar lemmas, and sit in the namespaces needed for dot notation.
✅	documentation	approved	claude/claude-opus-5-5	Both new files open with module docstrings that state their content and purpose, and every public theorem has an accurate docstring whose cross-references resolve. The prior finding about the reversed event in IsPVar.measure_le_le_lintegral_min is fixed.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are short and robust: the rewrite chains are at most three steps, the calc blocks make the reasoning clear, and the two rfl steps only unfold Set.preimage into its set-builder form. No proof-quality issues found.

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

_{Reviewing this diff at head 2898b3d. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $2.29.}