[RemyDegenne]

This PR adds p-to-e calibrators to the EValues library [RW, Definition 2.3, Propositions 2.5–2.6, (2.1)–(2.2); VW21, Proposition 2.1]. It covers the definition, its validity for every null on every measurable space, its converse, and the characterization of admissible calibrators. It also adds the rescaling, mixtures, and the power calibrators with their mixture in closed form. Everything is in ℝ≥0∞ and lives in the namespace ProbabilityTheory, next to IsPVar and Statlib's IsEVar, as the roadmap's Conventions ask.

Roadmap: EValues

Milestone: EValues Layer 0.2, Calibrators. Here is how each item is covered (new file EValues/Calibrator.lean):

• IsPToECalibrator f: an antitone f : ℝ≥0∞ → ℝ≥0∞, zero on (1, ∞], with ∫⁻ x in Icc 0 1, f (ENNReal.ofReal x) ≤ 1. As the roadmap asks, the characterization of [RW, Proposition 2.5] is the definition. It also provides IsPToECalibrator.measurable.
• Validity, IsPToECalibrator.isEVar_comp: for a null of probability measures, f ∘ p is an e-variable for every p-variable p [VW21, Proposition 2.1]. The proof goes through two public lemmas:
  • IsPVar.measure_preimage_le: a p-variable charges every lower set of ℝ≥0∞ at most as much as the uniform law on [0, 1] does.
  • IsPVar.lintegral_comp_le: for every antitone f, ∫⁻ f ∘ p ∂P ≤ ∫⁻ x in Icc 0 1, f (ofReal x), under any measure of mass at most 1. This uses the layer cake formula on both sides.
• The converse, isPToECalibrator_iff_isEVar: an antitone f vanishing on (1, ∞] is a calibrator exactly when f applied to the identity of [0, 1] under Lebesgue measure is an e-variable. This uses the existing isExactPVar_ofReal_volume.
• IsPToECalibrator.le_inv: f x ≤ x⁻¹ ([RW], text after (2.5)).
• Admissibility:
  • IsAdmissiblePToECalibrator: every calibrator g ≥ f is f [RW, Definition 2.3(iii)].
  • isAdmissiblePToECalibrator_iff: a calibrator is admissible exactly when it is UpperSemicontinuous, f 0 = ∞ and ∫₀¹ f = 1 [RW, Proposition 2.5].
  • Necessity: an admissible f equals each of three calibrators that dominate it. They are f plus the constant 1 - ∫₀¹ f on [0, 1]; f set to ∞ at 0; and Mathlib's left limit Function.leftLim f. The last differs from f only at its countably many discontinuities (Antitone.countable_not_continuousAt).
  • Sufficiency: a dominating calibrator agrees with f almost everywhere (ae_eq_of_ae_le_of_lintegral_le), and upper semicontinuity rules out a gap to the left of any point.
• Rescaling [RW, Proposition 2.6]: IsPToECalibrator.const_mul_comp_mul and IsAdmissiblePToECalibrator.const_mul_comp_mul show that x ↦ a f (a x), for a : ℝ≥0 with 1 ≤ a, is a calibrator, resp. an admissible one.
• Mixtures, isPToECalibrator_lintegral: x ↦ ∫⁻ i, f i x ∂π is a calibrator for a probability measure π and a jointly measurable family that is π-a.e. a calibrator (Tonelli, no integrability).
• Instances:
  • powCalibrator κ: x ↦ κ x ^ (κ - 1) on [0, 1], zero above. It comes with powCalibrator_def, simp lemmas powCalibrator_of_le_one / powCalibrator_of_one_lt, measurable_powCalibrator and setLIntegral_powCalibrator.
  • It is a calibrator for 0 < κ ≤ 1 and admissible for 0 < κ < 1 (isAdmissiblePToECalibrator_powCalibrator) [RW, (2.1)].
  • powMixCalibrator, its mixture over κ uniform on (0, 1), is a calibrator (derived from isPToECalibrator_lintegral). powMixCalibrator_ofReal gives its closed form (1 - x + x log x) / (x (log x) ^ 2) on (0, 1) [RW, (2.2)], by the fundamental theorem of calculus.

Two general lemmas go to their natural homes:

• Antitone.upperSemicontinuous_leftLim, in the new file Topology/Order/LeftRightLim.lean, next to Mathlib's Topology/Order/LeftRightLim.lean: the left limit of an antitone function is upper semicontinuous.
• UpperSemicontinuous.ennreal_const_mul, in Topology/Semicontinuity/ENNReal.lean, beside the existing LowerSemicontinuous.ennreal_const_mul (whose docstring is adapted).

Reuse: before writing, I searched Mathlib, Tau Ceti, LML, Statlib and LMLExplore/ for calibrators (calibrat), for integral comparisons under stochastic dominance, and for semicontinuity of leftLim. None of these exist. Tau Ceti's Probability/StochasticOrder.lean compares cdfs and couplings of real laws and has no integral comparison of antitone functions in ℝ≥0∞. The proofs reuse:

• Tau Ceti's ℝ≥0∞ layer cake formula TauCeti.lintegral_rpow_eq_lintegral_meas_ofReal_lt_mul (at exponent 1), TauCeti.setLIntegral_comp_mul_left_mul_rpow (the change of variables of the rescaling) and TauCeti.lintegral_ofReal_rpow_Ioo (the integral of x ^ (κ - 1));
• Mathlib's Function.leftLim API, Antitone.countable_not_continuousAt, ae_eq_of_ae_le_of_lintegral_le, lintegral_lintegral_swap, Real.hasStrictDerivAt_const_rpow and intervalIntegral.integral_eq_sub_of_hasDerivAt.

No proof is longer than 35 lines. No public declaration is removed or renamed.

What remains of Layer 0.2 after this PR: the e-to-p direction, that t ↦ min 1 t⁻¹ is the only admissible e-to-p calibrator [RW, Proposition 2.4], and the representation of e-variables for an atomless law as calibrated exact p-variables [RW, Proposition 2.7]. The admissibility of the mixture powMixCalibrator is also not proved here: its integral is 1 and it is ∞ at 0, but its upper semicontinuity needs a monotone-convergence argument.

Local checks (not CI): tauceti-local-checks verify --policy ordinary exited 0 on the pushed head.

• scope: scoped: against 9c0ace1dc80645e20b280043bb50daf007ee6723
• Whole-library lake build --iofail succeeded (8625 jobs).
• local-axioms: checked 3 changed module(s), 58 declaration(s); 0 violation(s)
• The module-system, header-style and local-lint checks (3 changed modules, 58 declarations) passed.

🤖 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	The definitions and statements match the roadmap's Calibrators milestone and the cited results [RW, Prop. 2.5, 2.6, (2.1)–(2.2); VW21, Prop. 2.1]; the closed form F(1)−F(0) = (1 − x + x log x)/(x log² x) checks by hand, and the power calibrators witness both predicates non-degenerately.
✅	reuse	approved	claude/claude-opus-5-5	Calibrators, the left-limit upper-semicontinuity lemma, the derivative lemma, and the p-variable stochastic-dominance lemmas have no counterpart in Mathlib (Mathlib's only countable leftLim ≠ f result, StieltjesFunction.countable_leftLim_ne, does not apply to antitone ℝ≥0∞ maps) or in LMLExplore; the new code reuses Mathlib's leftLim, Continuous.comp_upperSemicontinuous and Antitone.countable_not_continuousAt, and moves the existing uniform-cdf computation out into a public lemma instead of copying it.
✅	scope	approved	claude/claude-opus-5-5	The PR implements the first two bullets of EValues Layer 0.2 'Calibrators' (roadmap README.md:253-263): the definition, validity and its converse, the admissibility characterization, rescaling, and the power calibrators with their mixture and its closed form. The helper lemmas (the rpow antiderivative, upper semicontinuity of leftLim, the USC const_mul lemma, the p-variable stochastic-dominance lemmas and the extracted uniform distribution function) are all used directly toward that target, so this is one coherent unit.
✅	attribution	approved	claude/claude-opus-5-5	The calibrator file cites its informal sources (RW Definition 2.3, Propositions 2.5–2.6, (2.1)–(2.2); VW21 Proposition 2.1) in the module docstring and on each central declaration, and these match the roadmap's attributions. The roadmap is credited only in the PR description, and the auxiliary lemmas are routine and need no credit.
✅	api-design	approved	claude/claude-opus-5-5	The calibrator predicates are data-free Prop structures, powCalibrator/powMixCalibrator keep their bodies hidden behind (rfl) _def lemmas, and the case lemmas for powCalibrator are correctly tagged @[simp]. The new general lemmas are public in their natural homes, and the remaining private helpers serve only the calibrator proofs.
✅	generality	approved	claude/claude-opus-5-5	Every hypothesis is used or required: the probability-null assumption is forced by IsEVar's ≤ P univ form, 1 ≤ a and c ≠ ∞ are necessary, and the comparison lemmas already assume only P univ ≤ 1. Special cases (power mixture, admissible rescaling) are derived from the general mixture lemma and the general admissibility characterization, not re-proved.
✅	placement	approved	claude/claude-opus-5-5	Calibrator material lives in EValues/Calibrator.lean, the p-variable comparison lemmas sit in EValues/PVariable.lean beside the uniform-law results, and the general lemmas land in existing topic directories (Topology/Order, Topology/Semicontinuity, Analysis/SpecialFunctions/Pow). No import is evidently unused or overly broad.
✅	naming	approved	claude/claude-opus-5-5	Names describe their conclusions in standard Mathlib terminology, match the roadmap's suggested IsPToECalibrator/IsPToECalibrator.isEVar_comp, and are consistent with the sibling IsPVar/IsEVar and LowerSemicontinuous.ennreal_const_mul API. No notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	The two remaining overclaims from the prior round are fixed: both now state the probability-measure hypothesis that isEVar_comp needs. Every new file has an accurate module docstring, and every public definition and main theorem is documented without overclaiming.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are short, use no change/show or undocumented defeq, and factor reusable steps into named lemmas (measure_preimage_le, setLIntegral_Icc_ofReal_of_eq_zero, setLIntegral_const_mul_comp_mul, the three dominating-calibrator lemmas). The longest proof, eq_of_le_of_upperSemicontinuous, is about 35 lines and has comments explaining its structure.

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

_{Reviewing this diff at head 842529b. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $3.73.}