[RemyDegenne]

This pull request defines admissible e-processes as [RRLK, §4.2] does, with a sufficient condition for admissibility, and proves that the sub-Gaussian exponential process exp (∑ i ≤ n, X i - (n + 1) / 2) is an admissible e-process for Filtration.piLE and the i.i.d. laws whose marginal is 1-sub-Gaussian and has no atom, which [RRLK] conjectures. It adds two new files, LMLExplore/EValues/EProcess/Admissible.lean (111 lines: the definition and its API) and LMLExplore/EValues/SubGaussian/AdmissibleEProcess.lean (the instance). It also adds the proof's general helpers, as public declarations, to five existing files (listed below).

Main declarations

• IsAdmissibleEProcess E ℱ S: a structure extending IsEProcess E ℱ S with the field ae_le_of_ae_le: every e-process F with E n ≤ᵐ[P] F n for every P ∈ S and every n has F n ≤ᵐ[P] E n for every P ∈ S and every n. It has the shape of IsAdmissibleEVar.
• IsAdmissibleEProcess.ae_le, IsAdmissibleEProcess.ae_eq: an e-process that dominates an admissible one is at most it, and equal to it, at every time, almost surely under every member of the null.
• IsAdmissibleEProcess.congr: an adapted process equal to an admissible e-process at every time, almost surely under every member of the null, is an admissible e-process (the counterpart of IsAdmissibleEVar.congr; it needs no finiteness of the null).
• isAdmissibleEProcess_iff_measure_lt_eq_zero: E is admissible exactly when it is an e-process and, for every e-process F that dominates it, P {ω | E n ω < F n ω} = 0 for every P ∈ S and every n. This is the roadmap's wording: no e-process dominates E strictly.
• IsEProcess.isAdmissibleEProcess_of_exists_lintegral_eq: for a null of finite measures, an e-process E is admissible if every ℱ n-measurable set charged by a member of the null is charged by a member P with ∫⁻ E n ∂P = P univ. It is the e-process counterpart of IsStronglyAdmissibleEVar.isAdmissibleEVar, applied at each time to the events of that time.
• isAdmissibleEProcess_ofReal_exp_sum_sub_iid: the process fun n ω ↦ ENNReal.ofReal (Real.exp (∑ i ∈ Finset.range (n + 1), ω i - (n + 1) / 2)) is an admissible e-process for Filtration.piLE (X := fun _ : ℕ ↦ ℝ) and the null (fun μ ↦ Measure.infinitePi fun _ : ℕ ↦ μ) '' {μ : Measure ℝ | IsProbabilityMeasure μ ∧ NullSingletonClass μ ∧ HasSubgaussianMGF id 1 μ}.

Moved modules

• The module LMLExplore.EValues.EProcess is moved to LMLExplore.EValues.EProcess.Basic (file LMLExplore/EValues/EProcess.lean → LMLExplore/EValues/EProcess/Basic.lean), so that the e-process files share the directory EValues/EProcess/. Its declarations are unchanged; every in-repository import is updated and there is no forwarding module. Downstream projects should replace import LMLExplore.EValues.EProcess by import LMLExplore.EValues.EProcess.Basic.

General helpers added to existing files

• LMLExplore.add_mul_add_mul_sq_le_of_le_deriv2 (Analysis/Calculus/MeanValue.lean): if c ≤ f'' on a convex set I containing a, then f a + f' a (x - a) + c / 2 (x - a) ^ 2 ≤ f x on I.
• ProbabilityTheory.indep_piLE_comap_eval_succ, ProbabilityTheory.setLIntegral_infinitePi_comp_eval_succ (Probability/ProductMeasure.lean): under an i.i.d. law, coordinate n + 1 is independent of Filtration.piLE n, and ∫⁻ ω in s, f (ω (n + 1)) ∂μ^ℕ = μ^ℕ s * ∫⁻ f ∂μ for s in Filtration.piLE n.
• LMLExplore.lintegral_ofReal_exp_mul_gaussianReal (Probability/Distributions/Gaussian/Real.lean): the moment generating function of 𝒩(μ, v) as a lower integral.
• ProbabilityTheory.HasSubgaussianMGF.of_lintegral_le (Probability/Moments/SubGaussian/Basic.lean): if ∫⁻ exp (t X) ≤ exp (c t ^ 2 / 2) for every t, then HasSubgaussianMGF X c μ, for any c and any a.e.-measurable X.
• LMLExplore.integrable_pow_mul_exp_of_ae_abs_le, LMLExplore.hasDerivAt_integral_pow_mul_exp_of_ae_abs_le (Probability/Moments/IntegrableExpMul.lean): if |X| ≤ b a.s. under a finite measure, every X ^ n exp (t X) is integrable, and t ↦ E[X ^ n exp (t X)] has derivative E[X ^ (n + 1) exp (t X)]. These are stated for a random variable X with |X| ≤ b a.s., which is more general than a measure carried by [-b, b]. The former private lintegral_ofReal_exp_of_measure_compl was only Mathlib's ofReal_integral_eq_lintegral_ofReal applied once, so its one use now calls that lemma directly.

Roadmap coverage (EValues, Layer 3, item 7)

Covered: the definition of admissibility in the first bullet ("E' dominates E when … ; E is admissible when no e-process dominates it strictly"), and the second sentence of the bullet "Instance": the exponential process is admissible for the i.i.d. laws whose marginal is 1-sub-Gaussian and has no atom, with Filtration.piLE.

Left for later pull requests: in the first bullet, domination by an admissible e-process for locally dominated nulls [RRLK, Proposition 9], admissible e-processes as essential infima of martingales [RRLK, Corollary 26], the simple-null case [RRLK, Theorem 18] and composite nonnegative martingales [RRLK, Corollary 29]; and the first sentence of the bullet "Instance", admissibility for the null of conditionally 1-sub-Gaussian increments [RRLK, Theorem 35].

Notes for reviewers

• Why the definition is here. LMLExplore had no admissible e-processes, and the roadmap states the result as "is admissible". The definition is the first sentence of item 7, it costs one structure and three short lemmas, and it has the shape of the existing IsAdmissibleEVar, so the rest of item 7 can build on it. Stating the instance with domination and equality written out would have needed a restatement once item 7 is built. The definition uses E n ≤ᵐ[P] F n rather than P {E n ≤ F n} = 1: the two agree for probability measures and the first one needs no measurability. isAdmissibleEProcess_iff_measure_lt_eq_zero states the roadmap's wording ("no e-process dominates E strictly"). The sufficient condition is general, and it is the step of the proof that does not depend on sub-Gaussian laws, so it sits with the definition in EProcess/Admissible.lean.
• No published source. [RRLK] proves admissibility for the larger null of conditionally 1-sub-Gaussian increments [RRLK, Theorem 35] and conjectures it for the nonatomic laws. The roadmap cites the proof here to the notes of the paper project RemyDegenne/evalues_research. The proof in this pull request is a rewrite of that project's Lean proof.
• How the proof goes. The process is M₀ * ∏ k < n, F k with M₀ = exp (X 0 - 1 / 2) and F k = exp (X (k + 1) - 1 / 2). Under an i.i.d. law the factor F k is independent of the first k + 1 coordinates, so isTestSupermartingale_mul_prod makes the process a test supermartingale under the null, hence an e-process (IsTestSupermartingale.isEProcess). Call a law ν touching when it is nonatomic, 1-sub-Gaussian, and ∫ exp (x - 1 / 2) ∂ν = 1. Under the i.i.d. law of a touching ν the process is a test martingale (isTestMartingale_mul_prod), so it has expectation 1 at every time. By the sufficient condition above it remains to show that every event of time n charged by μ^ℕ, for a nonatomic probability law μ, is charged by ν^ℕ for some touching ν. That event is a Borel set of the first n + 1 coordinates, and by Measure.AbsolutelyContinuous.pi' it is enough that every finite nonatomic measure m carried by [-b, b] is absolutely continuous with respect to a touching law. That law is ν₀ + c₀ (m - ∑ j, c j N_j):
  • The base law ν₀ = ∑ j, w j N_j mixes four Gaussian laws N_j = N (j - 3 p, 6 p - 2) with binomial weights, for p = 1 / (1 + √e).
  • Its moment generating function is exp (t ^ 2 / 2 - 3 g t), where g vanishes at 0 and 1 and is otherwise positive with a quadratic margin: this is the Kearns–Saul inequality, proved here.
  • The coefficients c j match the mass, mean, ∫ exp x and ∫ x exp x of m. The four moment vectors of the components form a basis of ℝ ^ 4, which is proved by an explicit inverse.
  • So the perturbation vanishes to second order at 0 and 1, and for small c₀ > 0 the slack of the base law absorbs it.
• The null. The roadmap's marginal condition ($\int e^{\lambda x},d\mu\le e^{\lambda^2/2}$ for every real λ) is Mathlib's HasSubgaussianMGF id 1 μ, with IsProbabilityMeasure μ, as in the open feat: the complete class for the two-sided sub-Gaussian null #428. "No atom" is Mathlib's NullSingletonClass μ (μ {x} = 0 for every x). For a finite Borel measure on ℝ this is the same as being atomless. The null is written out in the statement, and no definition is introduced for it.
• Indexing (a deviation from the roadmap's wording). The bullet writes the process as exp (∑ k < n, X k - n / 2), which is the indexing of the natural filtration of the past. With Filtration.piLE, which the roadmap asks for here, time n has seen n + 1 observations, so the statement uses exp (∑ i ≤ n, X i - (n + 1) / 2): the same process, shifted by one time step. The unshifted process is not an e-process for Filtration.piLE. A stopping time can look at X n before deciding to stop at n, for example τ = 0 if X 0 < 0 and τ = 1 otherwise, and under the standard Gaussian law this has expectation 1 / 2 + Φ(1) > 1 at τ.
• Reuse. Optional stopping is IsTestSupermartingale.isEProcess, and the wealth processes are isTestSupermartingale_mul_prod and isTestMartingale_mul_prod. The product of absolutely continuous measures is Statlib's Measure.AbsolutelyContinuous.pi', Measure.infinitePi_map_restrict and Filtration.piLE_eq_comap_frestrictLe come from Mathlib, the derivatives of t ↦ ∫ x ^ n exp (t x) from Mathlib's hasDerivAt_integral_pow_mul_exp_real, and the Gaussian moment generating function from mgf_fun_id_gaussianReal. The file imports neither Tau Ceti's nor LML's sub-Gaussian file, so the duplicate HasSubgaussianMGF.mono reported in feat: the complete class for the two-sided sub-Gaussian null #428 does not arise.
• The helpers that remain private in the instance file are specific to this proof: the factorization of the process, the Kearns–Saul gap for p = 1 / (1 + √e), the base law, moment matching, and the perturbation.
• Sources. The module docstring cites [EVR26, Note 02] (the notes of RemyDegenne/evalues_research) as the source of the argument, names the Lean file it is adapted from (EValuesResearch/Results/SubGaussian.lean, commit dd4072f), and cites Kearns–Saul [KS98] for the Bernoulli sub-Gaussian bound.
• Overlaps with open pull requests: none found (gh pr list on 2026-11-15). feat: the complete class for the two-sided sub-Gaussian null #428 and feat: e-processes for the one-sided conditionally sub-Gaussian null are dominated by predictable products of mixtures of exponentials #430 treat sub-Gaussian nulls but share no declaration with this one. feat: e-processes for an i.i.d. null grow at most at the bipolar rate in expectation [RR26, Lemma 3.3] #413 has lemmas on the first n observations of an i.i.d. sequence, but they are not used here.

Roadmap: EValues
Paper: RemyDegenne/evalues_research
Item: R16

🤖 Generated with Claude Code

https://claude.ai/code/session_0196ftMVbgjSJzPQEwdek3kM

[RemyDegenne]

🟡 api-design — request_changes claude/claude-opus-5-5

All the general helpers flagged earlier are now public in their proper homes, and the helpers still private are specific to this proof. The new admissibility API lacks the congr lemma that the existing IsAdmissibleEVar API has.

• LMLExplore/EValues/EProcess/Admissible.lean:78 — IsAdmissibleEProcess has no congr lemma (admissibility is preserved by an a.s. change of the process), unlike IsAdmissibleEVar.congr, so consumers who swap in an a.e.-equal version must unfold the definition. Fix: Add IsAdmissibleEProcess.congr (hE : IsAdmissibleEProcess E ℱ S) (hF : Adapted ℱ F) (hEF : ∀ P ∈ S, ∀ n, E n =ᵐ[P] F n) : IsAdmissibleEProcess F ℱ S, proving the e-process part with IsEProcess.mono_ae and the domination part as in IsAdmissibleEVar.congr.

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 · 32s · 260.7k in (247.1k cache read, 13.6k cache write) / 2.4k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

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

The general helpers now sit public in their proper earlier files, and every import I checked is used. But the PR creates the directory EValues/EProcess/ while leaving EValues/EProcess.lean beside it, against the repo's Foo/Basic.lean layout.

• LMLExplore/EValues/EProcess/Admissible.lean — The PR creates the directory EValues/EProcess/ while the base module stays outside it as EValues/EProcess.lean. The two files share the subject EProcess but are not grouped in one directory. Fix: git mv LMLExplore/EValues/EProcess.lean LMLExplore/EValues/EProcess/Basic.lean, then update every in-repository import (including public import LMLExplore.EValues.EProcess in EProcess/Admissible.lean) in this PR, with no forwarding module.

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 · 69s · 527.9k in (513.4k cache read, 14.4k cache write) / 3.4k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

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

The proofs are commented in sections, but two lemmas are 110–150 lines long and hide facts that could stand alone, and there is one fragile non-terminal simp, one long chain of named rewrites, and some small facts proved twice.

• LMLExplore/EValues/SubGaussian/AdmissibleEProcess.lean:745 — exists_touching_absolutelyContinuous is about 150 lines. It builds the moment-matched D and its derivatives, the global bound hL₀, the mixture identity hreal/hle, and the four properties of the law all inline. Fix: Split it into lemmas: one that D vanishes to second order at 0 and 1 with the bound hL₀, one for the mixture inequality hreal/hle given c₀, and one for the probability, no-atom and sub-Gaussian properties of the perturbed law. The main proof should then just put them together.
• LMLExplore/EValues/SubGaussian/AdmissibleEProcess.lean:367 — exists_mul_min_le_ksGap is about 110 lines. It proves several facts about ksGap inline: G2 is monotone on [1/2, ∞), the quadratic growth hnear near 1, the antitonicity hanti on [1/2, 1], and the right-half bound hright. Fix: Factor out ksGap_antitoneOn_Icc_half_one and a lemma giving a quadratic lower bound on ksGap near 1. Then the main proof only combines them using the symmetry ksGap_one_sub.
• LMLExplore/EValues/SubGaussian/AdmissibleEProcess.lean:635 — In exists_coeffs_four, an unrestricted simp [Fin.sum_univ_four] is followed by field_simp; ring. Its output on the explicit ![…] coefficient vector is not fixed, so a change to the simp set can break the field_simp/ring steps after it. Fix: Use simp only [Fin.sum_univ_four, Matrix.cons_val_zero, Matrix.cons_val_one, …, Fin.val_zero, …], or norm_num [Fin.sum_univ_four] as the closing step.
• LMLExplore/EValues/SubGaussian/AdmissibleEProcess.lean:727 — lintegral_ofReal_exp_mul_mixture uses a chain of eight named rewrites (lintegral_add_measure, lintegral_finsetSum_measure, lintegral_smul_measure, ← ofReal_integral_eq_lintegral_ofReal, ENNReal.ofReal_add, ENNReal.ofReal_sum_of_nonneg, ENNReal.ofReal_mul, smul_eq_mul). This breaks easily when Mathlib renames lemmas. Fix: Split the linear-in-measure step (simp only [lintegral_add_measure, lintegral_finsetSum_measure, lintegral_smul_measure]) from the ofReal arithmetic, and use simp/push_cast-style normalisation for the ENNReal.ofReal sums and products.
• LMLExplore/EValues/SubGaussian/AdmissibleEProcess.lean:274 — Some small facts are proved twice. ksParam * (1 + exp (1/2)) = 1 appears at lines 274 and 335, and exp (-(1/2)) * exp (1/2) = 1 at lines 189 and 868. The integrability step simpa using integrable_pow_mul_exp_of_ae_abs_le … 0 t is also repeated in exp_neg_mul_integral_exp_le and lintegral_ofReal_exp_mul_mixture. Fix: Add private lemmas ksParam_mul_one_add_exp_half and integrable_exp_mul_of_measure_compl (from hb), and use them at each of these places.

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 · 38s · 121.8k in (114.7k cache read, 7.1k cache write) / 3.9k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

AI review — changes requested

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	stale (re-run pending) (approved in @RemyDegenne's review of b4f7cb4)	—
♻️	reuse	stale (re-run pending) (approved in @RemyDegenne's review of b4f7cb4)	—
♻️	scope	stale (re-run pending) (approved in @RemyDegenne's review of b4f7cb4)	—
♻️	attribution	stale (re-run pending) (approved in @RemyDegenne's review of b4f7cb4)	—
✅	api-design	approved	claude/claude-opus-5-5	The public surface is minimal and complete: IsAdmissibleEProcess mirrors IsAdmissibleEVar with intro/elim (ae_le, ae_eq), congr, a characterization iff and a sufficient condition; general helpers are exported in their topical homes, and the module move leaves no forwarding import or alias.
♻️	generality	stale (re-run pending) (approved in @RemyDegenne's review of b4f7cb4)	—
✅	placement	approved	claude/claude-opus-5-5	New files sit in topic directories (EValues/EProcess/ after a clean move with no forwarding module, EValues/SubGaussian/), general helpers go into the existing files whose topics fit them, and the private helpers left in the instance file are specific to the proof. No import is evidently unused or overly broad.
♻️	naming	stale (re-run pending) (approved in @RemyDegenne's review of b4f7cb4)	—
♻️	documentation	stale (re-run pending) (approved in @RemyDegenne's review of b4f7cb4)	—
🟡	proof-quality	changes requested	claude/claude-opus-5-5	The proofs are commented in sections, but two lemmas are 110–150 lines long and hide facts that could stand alone, and there is one fragile non-terminal simp, one long chain of named rewrites, and some small facts proved twice.

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

_{Reviewing this diff at head 2794ebd. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $0.79.}