[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]

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	Replacing LMLExplore.klBerReal and its basic lemmas with Statlib's leaves every surviving statement as it was: the proofs that expand klBerReal_apply confirm both definitions have the same closed form, and the sub_sub and klBerReal_one_sub changes close the same goals as before. No faithfulness defect found.
✅	reuse	approved	claude/claude-opus-5-5	The PR moves to Statlib's klBerReal API, adds no compatibility surface, and the prior hand-written re-proof of klBerReal_eq_of_ne in klBer_add_klBer_le now uses Statlib's lemma. No remaining LMLExplore declaration duplicates a Statlib one (klBerReal_nonneg_of_klBer_ne_top is strictly more general than Statlib's klBerReal_nonneg).
✅	scope	approved	claude/claude-opus-5-5	Pure deduplication refactor: LMLExplore.klBerReal and five basic lemmas are replaced by Statlib's InformationTheory counterparts, with one rename to avoid a name clash; no new mathematics. Single coherent topic.
✅	attribution	approved	claude/claude-opus-5-5	The PR swaps local declarations for imported Statlib ones, and the module docstring names Statlib's InformationTheory.klBerReal and its basic API as their source. It adds no new material, so no further credit is required.
✅	api-design	approved	claude/claude-opus-5-5	The PR switches to Statlib's InformationTheory.klBerReal and its basic API with no compatibility layer left behind, and renaming the kept lemma to klBerReal_nonneg_of_klBer_ne_top fixes the earlier name clash with Statlib's klBerReal_nonneg. The rest of the klBer/klBerReal API keeps its surface and characteristic lemmas.
✅	generality	approved	claude/claude-opus-5-5	The PR moves usage to Statlib's identical klBerReal and its basic lemmas without changing any remaining statement's hypotheses. The renamed klBerReal_nonneg_of_klBer_ne_top keeps the weakest natural assumption (klBer p q ≠ ∞), which is more general than a 0 < q < 1 version, so no generality issue arises.
✅	placement	approved	claude/claude-opus-5-5	The new Statlib.ForMathlib.InformationTheory.KullbackLeibler.Bernoulli import supplies InformationTheory.klBerReal, which every remaining lemma in the file uses; the duplicated declarations are deleted with no forwarding shims. The klBerReal_* lemmas that stay sit next to klBer, which they relate to, and the added open InformationTheory lines are only namespace opens, not placement changes.
✅	naming	approved	claude/claude-opus-5-5	The only new name, klBerReal_nonneg_of_klBer_ne_top, follows the conclusion-then-distinguishing-hypothesis convention, and the adopted Statlib names use standard _apply/_self/_one_left/_one_sub suffixes; no notation is introduced.
✅	documentation	approved	claude/claude-opus-5-5	The module docstring correctly attributes the real closed form and its basic API to Statlib's InformationTheory.klBerReal, and no docstring still names a removed or renamed declaration. The renamed klBerReal_nonneg_of_klBer_ne_top keeps an accurate docstring and the cross-reference in klBerReal_eq_zero_iff was updated.
✅	proof-quality	approved	claude/claude-opus-5-5	The proof changes are single-step swaps from klBerReal_def to klBerReal_apply and four one-line .trans (sub_sub _ _ _) adapters to the grouped cross-entropy form; h₃ now comes from Statlib's klBerReal_eq_of_ne. The diff adds no brittle rewrite chains, no change/show, and no undocumented defeq reliance.

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

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