[RemyDegenne]

Tau Ceti now defines good rate functions and the large deviation principle, in TauCeti/Probability/LargeDeviations/Basic.lean. This PR deletes LMLExplore's two definitions and restates LMLExplore's large-deviations API, including Cramér's theorem, on top of Tau Ceti's.

Why the definitions agree

• IsGoodRateFunction: both require lower semicontinuity and compact sublevel sets at every finite level. LMLExplore stated the levels as c : ℝ≥0 and Tau Ceti states them as α : ℝ≥0∞ with α ≠ ∞, so the proofs now begin with lift c to ℝ≥0 using hc.
• IsLDP P I is HasLDP atTop (fun n : ℕ ↦ (n : ℝ≥0)⁻¹) P I.
  • Speed: in EReal, ((n⁻¹ : ℝ≥0) : EReal) * a = a / n for every n, including n = 0, where both sides are 0. The public lemma EReal.coe_inv_mul (new file LMLExplore/Data/EReal/Inv.lean) proves ((x⁻¹ : ℝ) : EReal) * a = a / x for every x : ℝ, including x = 0; the use sites first rewrite ((n⁻¹ : ℝ≥0) : ℝ) with NNReal.coe_inv.
  • Sets: IsLDP stated its bounds for every set, through interiors and closures, while HasLDP states them only for open and closed sets. Monotonicity of the measure, of ENNReal.log and of multiplication by ε i ≥ 0 derives the every-set bounds from the open and closed ones. The new theorems below prove this for any filter and any speed.
• The speed is written (n : ℝ≥0)⁻¹ rather than 1 / n, because that is the simp normal form (one_div).

Removed or renamed public declarations

Before (LMLExplore)	After
LMLExplore.IsGoodRateFunction	TauCeti.Probability.IsGoodRateFunction (upstream)
LMLExplore.IsGoodRateFunction.lowerSemicontinuous	TauCeti.Probability.IsGoodRateFunction.lowerSemicontinuous (upstream)
LMLExplore.IsGoodRateFunction.isCompact_setOf_le c	TauCeti.Probability.IsGoodRateFunction.isCompact_sublevel c ENNReal.coe_ne_top (upstream)
LMLExplore.IsLDP P I	TauCeti.Probability.HasLDP atTop (fun n : ℕ ↦ (n : ℝ≥0)⁻¹) P I (upstream)
LMLExplore.IsLDP.lowerSemicontinuous	TauCeti.Probability.HasLDP.lowerSemicontinuous (upstream)
LMLExplore.IsLDP.neg_iInf_interior_le_liminf	TauCeti.Probability.HasLDP.neg_iInf_interior_le_liminf (new theorem here, any filter and speed)
LMLExplore.IsLDP.limsup_le_neg_iInf_closure	TauCeti.Probability.HasLDP.limsup_le_neg_iInf_closure (new theorem here, any filter and speed)
LMLExplore.IsLDP.of_isClosed_of_mem_nhds	TauCeti.Probability.HasLDP.of_isClosed_of_mem_nhds (any filter and speed)
LMLExplore.IsLDP.eventually_measure_le_exp	TauCeti.Probability.HasLDP.eventually_measure_le_exp (speed 1 / n)
LMLExplore.IsLDP.eventually_exp_le_measure	TauCeti.Probability.HasLDP.eventually_exp_le_measure (speed 1 / n)
LMLExplore.IsLDP.exists_eventually_measure_norm_ge_le_exp	TauCeti.Probability.HasLDP.exists_eventually_measure_norm_ge_le_exp (speed 1 / n)
LMLExplore.limsup_log_div_le_neg_of_le_mul_exp	LMLExplore.limsup_inv_mul_log_le_neg_of_le_mul_exp
LMLExplore.neg_le_liminf_log_div_of_mul_exp_le	LMLExplore.neg_le_liminf_inv_mul_log_of_mul_exp_le
LMLExplore.eventually_le_exp_of_limsup_log_div_le	LMLExplore.eventually_le_exp_of_limsup_inv_mul_log_le
LMLExplore.eventually_exp_le_of_neg_le_liminf_log_div	LMLExplore.eventually_exp_le_of_neg_le_liminf_inv_mul_log
LMLExplore.isLDP_cramer	LMLExplore.hasLDP_cramer
LMLExplore.isLDP_cramer_of_iIndepFun	LMLExplore.hasLDP_cramer_of_iIndepFun
MeasureTheory.Measure.isLDP_cramer_expFamily	MeasureTheory.Measure.hasLDP_cramer_expFamily

The HasLDP.* lemmas sit in the TauCeti.Probability.HasLDP namespace so that dot notation works on a HasLDP hypothesis; hasLDP_cramer uses .of_isClosed_of_mem_nhds. LMLExplore already extends Mathlib and LML namespaces in the same way, but this is the first time it extends a Tau Ceti namespace.

The four exponential-bound criteria are renamed because their statements now use HasLDP's normal form ((n⁻¹ : ℝ≥0) : EReal) * ENNReal.log (u n) instead of ENNReal.log (u n) / n, so they plug straight into HasLDP fields. Their hypotheses and proofs are otherwise unchanged. The upper and lower bounds of Cramér's theorem (limsup_log_measure_le_neg_iInf_rateFunction, neg_rateFunction_le_liminf_log_measure) keep their names and are restated in the same form.

What remains in LMLExplore

Tau Ceti has no counterpart to any of the following, so all of it stays:

• The constructor HasLDP.of_isClosed_of_mem_nhds from the closed-set upper bound and the lower bound on the neighbourhoods of points. It is now stated for any filter and speed.
• The bounds of the principle for every set, through interior and closure, also for any filter and speed.
• The exponential-bound criteria and their converses, the exponential bounds and exponential tightness, at the speed 1 / n.
• isGoodRateFunction_sum_mul.
• Cramér's theorems hasLDP_cramer, hasLDP_cramer_of_iIndepFun and hasLDP_cramer_expFamily, with isGoodRateFunction_rateFunction and isGoodRateFunction_expFamilyRate_left, which keep their names.

All uses were inside LMLExplore/Probability/LargeDeviations/. The module docstrings of LargeDeviations/Basic.lean and LargeDeviations/Cramer.lean are updated: the definitions section now points to Tau Ceti, the main-statements lists use the new names, and the speed is described as 1 / n, Tau Ceti's convention, instead of "speed n".

Checks

• scripts/build.sh --iofail succeeds on the whole library.
• #lint in LMLExplore, run on a scratch file importing the two changed modules, reports no errors.
• grep finds none of the removed names under LMLExplore/.

Fixes #342

Roadmap: none

🤖 Generated with Claude Code

https://claude.ai/code/session_0196ftMV379vy48QfzHBVNvo

[prevostad]

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

The canonical surface replaces IsGoodRateFunction and IsLDP cleanly with no compatibility layer. One general EReal arithmetic lemma is hidden as private and should be exported from a general home instead.

• LMLExplore/Probability/LargeDeviations/Basic.lean:81 — private lemma coe_inv_natCast_mul ((((n⁻¹ : ℝ≥0) : ℝ) : EReal) * a = a / n) mentions only Mathlib types and has a proof unrelated to large deviations. It is the bridge users need between the old log / n form and the new HasLDP normal form used by the four public renamed criteria, but it is hidden. Fix: Make it public in a general EReal arithmetic file, ideally generalized to r : ℝ≥0 ((((r⁻¹ : ℝ≥0) : ℝ) : EReal) * a = a / r), and consider @[simp] if it fits the existing simp set.

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 · 25s · 173.1k in (162.5k cache read, 10.6k cache write) / 2.3k out tokens · reviewing this diff · rubric}

[RemyDegenne]

Fixed in 5c5d0f9. The private coe_inv_natCast_mul is gone. It is replaced by the public EReal.coe_nnreal_inv_mul (r : ℝ≥0) (a : EReal) : (((r⁻¹ : ℝ≥0) : ℝ) : EReal) * a = a / ((r : ℝ) : EReal), generalised to any r : ℝ≥0 as you suggested. It lives in a new general file, LMLExplore/Data/EReal/Inv.lean, which mirrors Mathlib.Data.EReal.Inv. The four criteria in LargeDeviations/Basic.lean now use simp_rw [EReal.coe_nnreal_inv_mul, NNReal.coe_natCast, EReal.coe_natCast].

I left it without @[simp] because its LHS is not in simp normal form. NNReal.coe_inv is already a simp lemma and rewrites ((r⁻¹ : ℝ≥0) : ℝ) to (r : ℝ)⁻¹. I checked this on a scratch file: simp on the statement leaves ⊢ ↑(↑r)⁻¹ * a = a / ↑↑r. So the simpNF linter would flag the tag.

[RemyDegenne]

Re: your reply on api-design — re-reviewed on 5c5d0f9; this clears the finding ✅ — approved on 5c5d0f9.

_{claude/claude-opus-5-5 · addresses your replies through comment 4569074020.}

[prevostad]

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.

	rubric	state	judge	summary
✅	correctness	approved	claude/claude-opus-5-5	The restated API matches the old definitions: the speed coefficient equals division by n, including at n = 0, and the old every-set bounds are recovered from Tau Ceti's open/closed bounds by monotonicity. The finite-level sublevel condition is equivalent, and the Cramér statements are faithfully carried over.
✅	reuse	approved	claude/claude-opus-5-5	The PR deletes LMLExplore's IsGoodRateFunction and IsLDP in favour of Tau Ceti's, leaves no compatibility aliases, and its new lemmas reuse existing Mathlib monotonicity results; I found no duplicates under LMLExplore/ or in Mathlib. The Tau Ceti source isn't in this checkout, so the PR's claim that upstream has no HasLDP constructor or every-set bounds is unverified.
✅	scope	approved	claude/claude-opus-5-5	Single-topic refactor that moves LMLExplore's existing good-rate-function and LDP API, including Cramér's theorem, onto Tau Ceti's HasLDP/IsGoodRateFunction; all content already existed on main and is only renamed, restated, or modestly generalised, so roadmap fit is automatic.
✅	attribution	approved	claude/claude-opus-5-5	The Dembo–Zeitouni and Degenne2023Existence credits remain, with the Degenne credit narrowed to the exponential-bound criteria now that the definitions are deleted, and the upstream Tau Ceti definitions are named in the docstrings. The new every-set bounds are routine monotonicity arguments that draw on no particular source.
🟡	api-design	changes requested	claude/claude-opus-5-5	The canonical surface replaces IsGoodRateFunction and IsLDP cleanly with no compatibility layer. One general EReal arithmetic lemma is hidden as private and should be exported from a general home instead.
✅	generality	approved	claude/claude-opus-5-5	The reduction and every-set bounds are generalised to any filter and speed, and the speed-1 / n lemmas are derived from them. The exponential-bound lemmas stay at 1 / n because their content needs the explicit rate exp (-(n r)), and no unused or too-strong assumptions appear in the changed signatures.
✅	placement	approved	claude/claude-opus-5-5	The general HasLDP lemmas and the speed-1 / n criteria stay in LMLExplore's own large-deviations base file, next to their consumers, and the only new import (TauCeti.Probability.LargeDeviations.Basic) is needed for HasLDP/IsGoodRateFunction. No file is added or moved, and no import is unused or overly broad.
✅	naming	approved	claude/claude-opus-5-5	Renamed lemmas name their conclusions in standard terms (inv_mul_log, iInf_interior, iInf_closure, hasLDP), and the HasLDP lemmas sit at the top level in the upstream namespace so dot notation works. No notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	Module and declaration docstrings in both changed files were updated to the Tau Ceti HasLDP/IsGoodRateFunction API and the 1 / n speed, with no stale names or overclaims found. The attribution note was correctly narrowed to the exponential-bound criteria.
✅	proof-quality	approved	claude/claude-opus-5-5	Proofs are robust and readable: the speed normal form is bridged by one private lemma reused through simp_rw, and the every-set bounds share a private monotonicity helper. No change/show or undocumented defeq reliance.

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

_{Reviewing this diff at head 4acb9d4. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $1.36.}

[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	approved	claude/claude-opus-5-5	Tau Ceti's HasLDP (open/closed bounds of the form ε i * log) at speed (n : ℝ≥0)⁻¹, together with the new every-set lemmas, is equivalent to the removed IsLDP, and the upstream IsGoodRateFunction matches the removed one at every finite level. The restated criteria, the constructor and the Cramér theorems keep their mathematical content, with no weakening or vacuity.
✅	reuse	approved	claude/claude-opus-5-5	The PR deletes LMLExplore's IsGoodRateFunction and IsLDP and rebuilds every use on Tau Ceti's definitions, leaving no compatibility artifacts. EReal.coe_inv_mul is not in Mathlib (only its parts EReal.coe_inv and EReal.div_eq_inv_mul exist) and has four uses; Tau Ceti's source was not in the checkout, so whether Tau Ceti already has the HasLDP lemmas kept here was not verified and rests on the PR description.
✅	scope	approved	claude/claude-opus-5-5	Single-topic refactor moving LMLExplore's existing large-deviations API and Cramér's theorems onto Tau Ceti's upstream IsGoodRateFunction/HasLDP, so roadmap fit is automatic. The only additions are modest generalisations (any filter and speed) and the conversion lemma EReal.coe_inv_mul that the refactor requires.
✅	attribution	approved	claude/claude-opus-5-5	The DZ98, D23 and Degenne2023Existence credits remain for the material still in LMLExplore, and the Degenne credit is narrowed only because the definitions it covered were deleted in favour of Tau Ceti's, which the docstrings name. The new general-filter lemmas and EReal.coe_inv_mul are routine and need no further credit.
✅	api-design	approved	claude/claude-opus-5-5	The post-PR surface has no compatibility layer: all IsLDP, IsGoodRateFunction and *_log_div names are gone, and the general EReal.coe_inv_mul is public in its own Data file with no Mathlib duplicate. The HasLDP.* extensions are stated for any filter and speed and use HasLDP's normal form, and the only private helper is specific to the file.
✅	generality	approved	claude/claude-opus-5-5	The earlier finding is fixed: EReal.coe_inv_mul now holds for every real x. The LDP API is stated for any filter and speed, and only the exponential-bound lemmas use speed 1 / n, which their exp (-(n r)) statements require.
✅	placement	approved	claude/claude-opus-5-5	The new EReal.coe_inv_mul sits in LMLExplore/Data/EReal/Inv.lean, which mirrors the Mathlib file it extends and is the only EReal file in LMLExplore, and the HasLDP.* lemmas stay in the large-deviations file they replace. No import is unused or too broad: the removed Mathlib.Data.EReal.Inv still arrives through the new module, and the Tau Ceti import is required.
✅	naming	approved	claude/claude-opus-5-5	The renamed inv_mul_log criteria, the HasLDP.* lemmas, the hasLDP_cramer* theorems and EReal.coe_inv_mul describe their conclusions in standard terminology. Putting the lemmas in the TauCeti.Probability.HasLDP namespace enables dot notation on the upstream predicate, and the PR adds no notation.
✅	documentation	approved	claude/claude-opus-5-5	The new EReal/Inv.lean module docstring and the rewritten docstrings in LargeDeviations/Basic.lean and Cramer.lean are accurate, point to Tau Ceti's HasLDP/IsGoodRateFunction, and use the new names and the 1 / n speed. A grep under LMLExplore/ finds no stale IsLDP, isLDP or "speed n" mentions, and each new or renamed public declaration has a docstring that matches its statement.
🟡	proof-quality	changes requested	claude/claude-opus-5-5	The proofs are short and use no change or show, but the four-lemma simp_rw chain that turns the speed ((n⁻¹ : ℝ≥0) : ℝ) : EReal into a division by n is repeated in four lemmas instead of being one reusable lemma.

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

_{Reviewing this diff at head dbac84d. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $2.65.}

[RemyDegenne]

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

The proofs are short and use no change or show, but the four-lemma simp_rw chain that turns the speed ((n⁻¹ : ℝ≥0) : ℝ) : EReal into a division by n is repeated in four lemmas instead of being one reusable lemma.

• LMLExplore/Probability/LargeDeviations/Basic.lean:116 — The chain simp_rw [NNReal.coe_inv, EReal.coe_inv_mul, NNReal.coe_natCast, EReal.coe_natCast] appears in limsup_inv_mul_log_le_neg_of_le_mul_exp, neg_le_liminf_inv_mul_log_of_mul_exp_le, eventually_le_exp_of_limsup_inv_mul_log_le (at h) and eventually_exp_le_of_neg_le_liminf_inv_mul_log (at h). This is repeated reasoning, and a rename of any of the four lemmas breaks all four proofs. Fix: Add one lemma, e.g. EReal.coe_nnreal_inv_natCast_mul (n : ℕ) (a : EReal) : (((n⁻¹ : ℝ≥0) : ℝ) : EReal) * a = a / n, next to EReal.coe_inv_mul in LMLExplore/Data/EReal/Inv.lean. Then use simp_rw [EReal.coe_nnreal_inv_natCast_mul] (or ... at h) at the four sites.

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 · 17s · 65.9k in (60.7k cache read, 5.2k cache write) / 1.5k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}