[RemyDegenne]

This pull request proves the instance "two samples with a common nuisance parameter" of the exponential-families item of the EValues roadmap: for two independent exponential observations and the null of the products Exp(l) ⊗ Exp(l), the numeraire is the likelihood ratio of the alternative to the law under which the sum has its law under the alternative and, given the sum s, the first observation is uniform on [0, s]; that law is the reverse information projection, the mixture of the members of the null whose mean is uniform between the two means, and no finite combination of members of the null; the same construction gives the numeraire for two geometric observations. It adds three new files, LMLExplore/EValues/Numeraire/Conditional.lean (133 lines, the general conditional e-variable, shared by the two instances), LMLExplore/EValues/TwoSample/Exponential.lean (580 lines) and LMLExplore/EValues/TwoSample/Geometric.lean (392 lines), and changes no existing file.

Main declarations

General (Numeraire/Conditional.lean), for a measurable statistic T : Ω → 𝓨, a finite kernel κ : Kernel 𝓨 Ω with κ y carried by T ⁻¹' {y} for Q.map T-almost every y, and a finite measure Q with Q ≪ κ ∘ₘ Q.map T:

• map_comp_eq_of_ae_eq: for a Markov kernel carried by the fibers, (κ ∘ₘ ν).map T = ν.
• ae_lintegral_rnDeriv_comp_map_eq_one: ∫⁻ x, Q.rnDeriv (κ ∘ₘ Q.map T) x ∂κ y = 1 for Q.map T-almost every y.
• lintegral_rnDeriv_comp_map, isEVar_rnDeriv_comp_map: under every P with κ ∘ₘ P.map T = P and P.map T ≪ Q.map T, the likelihood ratio Q.rnDeriv (κ ∘ₘ Q.map T) has expectation P univ; so it is an e-variable for every null of finite measures of which κ is the conditional law given T (the conditional e-variable of [HGLLA24]).

Two exponential observations (TwoSample/Exponential.lean), with Q = (expMeasure l₁).prod (expMeasure l₂) and the null Set.range fun l : Ioi (0 : ℝ) ↦ (expMeasure l).prod (expMeasure l):

• Kernel.segmentUniform : Kernel ℝ (ℝ × ℝ), the law of (u * s, (1 - u) * s) for u uniform on [0, 1] (Tau Ceti's uniformMeasure 0 1), with Kernel.isMarkovKernel_segmentUniform, Kernel.segmentUniform_apply, Kernel.segmentUniform_comp and Kernel.ae_add_segmentUniform.
• isNumeraire_rnDeriv_segmentUniform_comp (0 < l₁, 0 < l₂): IsNumeraire (Q.rnDeriv (Kernel.segmentUniform ∘ₘ Q.map (fun x ↦ x.1 + x.2))) S Q.
• ripr_prod_expMeasure (0 < l₁, 0 < l₂): ripr Q S = Kernel.segmentUniform ∘ₘ Q.map (fun x ↦ x.1 + x.2).
• segmentUniform_comp_map_add_prod_expMeasure (0 < l₁, 0 < l₂, l₁ ≠ l₂): Kernel.segmentUniform ∘ₘ Q.map (fun x ↦ x.1 + x.2) = (uniformMeasure (min l₁⁻¹ l₂⁻¹) (max l₁⁻¹ l₂⁻¹)).bind fun m ↦ (expMeasure m⁻¹).prod (expMeasure m⁻¹).
• sum_smul_prod_expMeasure_ne_ripr (0 < l₁, 0 < l₂, l₁ ≠ l₂): ∑ l ∈ s, w l • (expMeasure l).prod (expMeasure l) ≠ ripr Q S for every s : Finset ℝ and w : ℝ → ℝ≥0∞.

Two geometric observations (TwoSample/Geometric.lean), with Mathlib's geometricMeasure and the null Set.range fun p : unitInterval ↦ (geometricMeasure p).prod (geometricMeasure p):

• Kernel.antidiagonalUniform : Kernel ℕ (ℕ × ℕ), the uniform law (uniformOn) on the pairs (j, k) with j + k = s, with Kernel.antidiagonalUniform_apply, Kernel.isMarkovKernel_antidiagonalUniform, Kernel.antidiagonalUniform_singleton and Kernel.ae_add_antidiagonalUniform.
• isNumeraire_rnDeriv_antidiagonalUniform_comp ((p₁ ≠ 0 ∧ p₁ ≠ 1) ∨ (p₂ ≠ 0 ∧ p₂ ≠ 1)): the likelihood ratio of Geom(p₁) ⊗ Geom(p₂) to Kernel.antidiagonalUniform ∘ₘ Q.map (fun x ↦ x.1 + x.2) is the numeraire.

Roadmap coverage (EValues, Layer 1, item 5)

Covered: the bullet "Instance, two samples with a common nuisance parameter [HGLLA24]", that is, the numeraire for two exponential observations, the identification of the law as the reverse information projection, its description as the mixture of the members of the null whose mean 1 / l is uniform between 1 / l₁ and 1 / l₂, the fact that no finite combination of members of the null is equal to it (against the conjecture of [HGLLA24, §5.2]), and the numeraire for two geometric observations with the uniform law on {0, …, s}.

Left: the rest of item 5 (the mean-value parametrization of vector exponential families, the equivalences of [GLHBdJ24, Theorem 1], and the Gaussian scale instance).

Notes for reviewers

• How the proof goes. The general file proves that the likelihood ratio X = Q.rnDeriv (κ ∘ₘ Q.map T) integrates to one against κ y for Q.map T-almost every y, by comparing (Q.map T).withDensity (fun y ↦ ∫⁻ X ∂κ y) with Q.map T on every set; under a member P = κ ∘ₘ P.map T of the null this gives ∫⁻ X ∂P = P univ. The numeraire then comes from main's isNumeraire_of_ae_eq_rnDeriv ([LRR25, Theorem 4.1]) and the reverse information projection from ripr_eq_of_isEVar_rnDeriv, once the law is in the effective null (comp_mem_effectiveSet, as a mixture of members of the null).
• Exponential case. That every member of the null has the conditional law Kernel.segmentUniform given the sum, and that the sum has the law Gamma(2, l), is Tau Ceti's beta–gamma algebra (map_div_add_prod_gammaMeasure, betaMeasure_one_one). The law of the sum under Q is Tau Ceti's hypoexponentialMeasure ![l₁, l₂], whose density l₁ l₂ (exp (- l₁ x) - exp (- l₂ x)) / (l₂ - l₁) is computed by hypoexponentialPDFReal_of_injective; the mixture of the Gamma(2, 1 / m) over the uniform mean has the same density (Tau Ceti's Measure.bind_withDensity and the antiderivative exp (- x / m)), and the mixture identity in the plane follows by associativity of the composition with Kernel.segmentUniform. The equivalences Q ≪ Qᶜ ≪ Q and the absolute continuity of the laws of the sum need no density: every product of exponential laws with positive rates is equivalent to Exp(1) ⊗ Exp(1), which is its own Qᶜ. For the last statement, a finite combination equal to the reverse information projection would give the law of the sum the density ∑ w l * l ^ 2 * x * exp (- l x); comparing with exp (- min l₁ l₂ * x) at infinity shows that the terms with l ≤ min l₁ l₂ vanish and that the other ones decay too fast.
• Geometric case. The masses of the points under Geom(p) ⊗ Geom(p) depend only on the sum, which gives the conditional law; the mixture over m uniform between 1 / p₁ and 1 / p₂ of the laws Geom(1 / m) ⊗ Geom(1 / m) (the mean m - 1 uniform between the two means) is computed on points through the antiderivative (1 - 1 / m) ^ (s + 1) / (s + 1), and is private.
• What has no published source. The general conditional e-variable is the construction of [HGLLA24]. Its identification as the numeraire and the reverse information projection in these two families, the mixture, the failure of finite combinations and the geometric case have no published source: the roadmap cites them [EVR26, Note 28]. The proofs are new; they replace the paper project's direct optimality argument by the effective-null criterion, and its uniqueness of the mixing law (through moment-generating functions) by the asymptotic argument above, which is all the roadmap's statement needs.
• Deviations from the roadmap's wording. The numeraire and the reverse information projection of two exponential observations are stated for all positive rates, l₁ = l₂ included (then Q is in the null and is its own Qᶜ); only the mixture and the last statement need l₁ ≠ l₂. The geometric statement assumes that one of the two laws is not a point mass, (p₁ ≠ 0 ∧ p₁ ≠ 1) ∨ (p₂ ≠ 0 ∧ p₂ ≠ 1) (Mathlib's geometricMeasure 0 is the point mass at 0, as is geometricMeasure 1): when Q is the point mass at (0, 0), Q.rnDeriv is not determined off (0, 0) and need not be an e-variable. The geometric reverse information projection is not stated (the roadmap asks only for the numeraire; it differs from the law above when one of the laws is a point mass). The "law under which the sum has its law under the alternative and, given the sum, the first observation is uniform" is written κ ∘ₘ Q.map (fun x ↦ x.1 + x.2) with the kernels Kernel.segmentUniform and Kernel.antidiagonalUniform.
• Small additions. A private instance SFinite (expMeasure l) (Mathlib has none; inferInstanceAs through gammaMeasure 1 l).
• Open pull requests. None covers this item. feat: merging functions for independent e-values, and for two e-values functions that no generalized martingale or precise merging function dominates #426 and feat: two mixture nulls separating one observation, the bipolar rate and the relative entropy #435 add lemmas to LMLExplore/MeasureTheory/Constructions/Pi.lean; none of them is needed here. The branch is on top of feat: identifying numeraires through the effective null #410 (merged), whose isNumeraire_of_ae_eq_rnDeriv and ripr_eq_of_isEVar_rnDeriv it uses.

Roadmap: EValues
Paper: RemyDegenne/evalues_research
Item: R31

🤖 Generated with Claude Code

https://claude.ai/code/session_0196ftMVbgjSJzPQEwdek3kM