[RemyDegenne]

Statlib's Statlib/ForMathlib/InformationTheory/KullbackLeibler/Bernoulli.lean defines the real binary relative entropy InformationTheory.klBerReal p q = p * log (p / q) + (1 - p) * log ((1 - p) / (1 - q)) with the same body as LMLExplore.klBerReal, and five of its basic lemmas. This PR makes LMLExplore/InformationTheory/KullbackLeibler/Bernoulli.lean import that Statlib file, deletes the LMLExplore copies, and moves every use to the Statlib declarations. The files that use klBerReal without already opening InformationTheory now open it: Bandits/Concentration.lean, Bandits/KLUCB.lean, InformationTheory/KrichevskyTrofimov.lean, Probability/Distributions/ExponentialFamily/Bernoulli.lean, Probability/Moments/KLChernoff.lean and SequentialLearning/BernoulliDeviation.lean.

Now that #354 has merged, the Statlib file can be imported: it imports Statlib's Bernoulli file, which used to clash with LMLExplore/Probability/Distributions/Bernoulli.lean.

Removed public declarations

Removed	Replacement
LMLExplore.klBerReal	InformationTheory.klBerReal (same body, so the two are definitionally equal)
LMLExplore.klBerReal_def	InformationTheory.klBerReal_apply
LMLExplore.klBerReal_self	InformationTheory.klBerReal_self (also @[simp])
LMLExplore.klBerReal_one_left	InformationTheory.klBerReal_one_left (also @[simp])
LMLExplore.klBerReal_one_sub_one_sub	InformationTheory.klBerReal_one_sub. Same statement, but Statlib's lemma is not @[simp]. No simp call in LMLExplore needed it.
LMLExplore.klBerReal_eq_neg_binEntropy_sub (right-hand side -binEntropy p - (p * log q + (1 - p) * log (1 - q)))	InformationTheory.klBerReal_eq_neg_binEntropy_sub (right-hand side -binEntropy p - p * log q - (1 - p) * log (1 - q)). The four uses, in the continuity, derivative and strict convexity proofs, recover the old form with .trans (sub_sub _ _ _).

Renamed public declarations

Old name	New name
LMLExplore.klBerReal_nonneg	LMLExplore.klBerReal_nonneg_of_klBer_ne_top (same statement; renamed so that a bare klBerReal_nonneg under open InformationTheory no longer has two candidates with different hypotheses)

klBer_add_klBer_le now uses Statlib's InformationTheory.klBerReal_eq_of_ne instead of re-deriving it.

What stays in LMLExplore

• The ℝ≥0∞-valued LMLExplore.klBer and its whole API: klDiv_bernoulliMeasure (klDiv Ber(x, y, p) Ber(x, y, q) = klBer p q for all p q : I, including the infinite cases, so Statlib's klDiv_bernoulliMeasure_eq_klBerReal, which assumes q ∉ {0, 1}, is a special case of it together with klBer_eq_ofReal_klBerReal), the data processing inequalities, klUpper, klLower, monotonicity, convexity, continuity and measurability. Statlib, LML, Tau Ceti and Mathlib have no klBer.
• LMLExplore.klBerReal_nonneg, renamed to LMLExplore.klBerReal_nonneg_of_klBer_ne_top (see below). It only assumes p, q ∈ [0, 1] and klBer p q ≠ ∞, so it is more general than Statlib's InformationTheory.klBerReal_nonneg (which assumes 0 < q < 1).
• The other klBerReal_* lemmas, which have no Statlib counterpart: klBerReal_eq_zero_iff, klBerReal_le_sq_sub_div, two_mul_sq_le_klBerReal, mul_klBerReal_div_eq_log, continuity, derivatives, strict monotonicity and convexity, klBerReal_one_sub_right, the limits at 0 and 1, mul_klFun_div_le_klBerReal, and so on. They are unchanged, but are now stated about InformationTheory.klBerReal.

The module docstring now names the Statlib definition and its basic API, and its list of definitions and main statements drops the removed declarations.

Checks run

• scripts/build.sh --iofail on the whole library (8551 jobs): succeeds, with no warnings.
• #lint in LMLExplore, run from a scratch file that imports the eight changed modules: all checks pass.
• lake exe axioms: no duplicate declarations against the 5613 dependency modules, and every declaration is within the allowlist.
• grep over LMLExplore/: klBerReal_def, klBerReal_one_sub_one_sub and LMLExplore.klBerReal no longer appear anywhere.

Fixes #331

Roadmap: none

🤖 Generated with Claude Code

[RemyDegenne]

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

The migration to Statlib's klBerReal is correct and leaves no compatibility surface; one edited proof step still re-derives Statlib's klBerReal_eq_of_ne by hand instead of using it.

• LMLExplore/InformationTheory/KullbackLeibler/Bernoulli.lean:721 — In klBer_add_klBer_le, h₃ : klBerReal q r = q * (log q - log r) + (1 - q) * (log (1 - q) - log (1 - r)) is re-proved with klBerReal_apply and two log_div rewrites. It is exactly Statlib's InformationTheory.klBerReal_eq_of_ne, from the module this PR now imports. Fix: Replace lines 721-722 with have h₃ := klBerReal_eq_of_ne (p := q) hr'.1.ne' hr'.2.ne (here hr' : r ∈ Set.Ioo 0 1).

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 · 49s · 227.6k in (209.9k cache read, 17.7k cache write) / 3.2k out tokens · reviewing this diff · rubric · ⚠️ rubrics checkout differs from published main}

[RemyDegenne]

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

Moving to Statlib's InformationTheory.klBerReal is right and leaves no compatibility layer behind. But the kept LMLExplore.klBerReal_nonneg now has the same name as Statlib's InformationTheory.klBerReal_nonneg, with different hypotheses, in files that open both namespaces.

• LMLExplore/InformationTheory/KullbackLeibler/Bernoulli.lean:316 — LMLExplore.klBerReal_nonneg (hyps p, q ∈ Icc 0 1, klBer p q ≠ ∞) has the same name as Statlib's InformationTheory.klBerReal_nonneg (hyp 0 < q < 1), and both are about the same definition InformationTheory.klBerReal. This PR opens InformationTheory inside namespace LMLExplore in six files, so a bare klBerReal_nonneg is ambiguous there and is only resolved by checking which lemma the hypotheses fit. That gives a confusing interface and fragile elaboration. Fix: Rename the LMLExplore lemma to name its hypothesis, e.g. klBerReal_nonneg_of_klBer_ne_top. Update its uses at Bernoulli.lean:474, 581, 706, 707, KLChernoff.lean:391 and BernoulliDeviation.lean:284, and the docstring reference at Bernoulli.lean:329.

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 · 98.2k in (91.4k cache read, 6.8k cache write) / 2.7k 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	approved	claude/claude-opus-5-5	The PR swaps LMLExplore.klBerReal and five basic lemmas for Statlib's matching declarations without changing any surviving statement; every changed proof site (klBerReal_apply, the sub_sub re-association, klBerReal_one_sub) closes the same goal as before. No faithfulness defect found.
🟡	reuse	changes requested	claude/claude-opus-5-5	The migration to Statlib's klBerReal is correct and leaves no compatibility surface; one edited proof step still re-derives Statlib's klBerReal_eq_of_ne by hand instead of using it.
✅	scope	approved	claude/claude-opus-5-5	Pure deduplication refactor replacing LMLExplore.klBerReal and five basic lemmas with Statlib's InformationTheory counterparts; no new mathematical content, single coherent topic.
✅	attribution	approved	claude/claude-opus-5-5	The PR replaces local declarations with imported Statlib ones, and the module docstring now names Statlib's InformationTheory.klBerReal and its basic API as their source. No new material is added, so no further credit is needed.
🟡	api-design	changes requested	claude/claude-opus-5-5	Moving to Statlib's InformationTheory.klBerReal is right and leaves no compatibility layer behind. But the kept LMLExplore.klBerReal_nonneg now has the same name as Statlib's InformationTheory.klBerReal_nonneg, with different hypotheses, in files that open both namespaces.
✅	generality	approved	claude/claude-opus-5-5	The PR replaces the local klBerReal and five basic lemmas with Statlib's identical declarations and changes no remaining statement's hypotheses. The retained LMLExplore.klBerReal_nonneg uses the weakest natural assumption (klBer p q ≠ ∞); without it klBerReal p 0 = (1 - p) log(1 - p) < 0 for 0 < p < 1.
✅	placement	approved	claude/claude-opus-5-5	The new Statlib Bernoulli import supplies the InformationTheory.klBerReal that the remaining lemmas are stated about, and the duplicated declarations are removed with no shims. The lemmas that stay are correctly placed next to klBer.
✅	naming	approved	claude/claude-opus-5-5	The PR introduces no new names or notation; the Statlib replacements (klBerReal_apply, klBerReal_self, klBerReal_one_left, klBerReal_one_sub, klBerReal_eq_neg_binEntropy_sub) follow standard suffix conventions, and the remaining LMLExplore lemmas keep conclusion-describing names in the LMLExplore namespace.
✅	documentation	approved	claude/claude-opus-5-5	The module docstring now correctly attributes the closed form and its basic API to Statlib's InformationTheory.klBerReal, and no docstring still refers to a removed declaration.
✅	proof-quality	approved	claude/claude-opus-5-5	The changes swap klBerReal_def for klBerReal_apply in single rewrite steps and add four one-line .trans (sub_sub _ _ _) adapters, which are needed where proofs rely on the grouped cross-entropy form (for example sub_concaveOn). No new change/show, defeq reliance, or brittle rewrite chains.

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

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