[RemyDegenne]

Statlib's new Statlib/ForMathlib/Probability/Distributions/Bernoulli.lean provides several lemmas that LMLExplore/Probability/Distributions/Bernoulli.lean also had, three of them under the same fully qualified name, so the two files could not be imported together. This PR makes LMLExplore/Probability/Distributions/Bernoulli.lean import the Statlib file (in place of TauCeti.Probability.Distributions.Bernoulli.Measurability and the redundant Mathlib.Probability.Distributions.Bernoulli), deletes the LMLExplore copies, and moves every use to the Statlib declarations.

Removed or renamed public declarations

Removed or renamed	Replacement
ProbabilityTheory.lintegral_bernoulliMeasure (LMLExplore)	ProbabilityTheory.lintegral_bernoulliMeasure (Statlib). Same name and statement, so the use in SequentialLearning/BernoulliDeviation.lean needs no change.
ProbabilityTheory.bernoulliMeasure_symm x y p : Ber(x, y, σ p) = Ber(y, x, p)	ProbabilityTheory.bernoulliMeasure_swap y x p (Statlib)
ProbabilityTheory.bernoulliMeasure_eq_smul_add_smul (LMLExplore: weights a b : ℝ≥0 with a + b = 1, acting through ℝ≥0∞)	ProbabilityTheory.bernoulliMeasure_eq_smul_add_smul (Statlib: weights t and 1 - t with t ≤ 1). Its only use, LMLExplore.klBer_mul_add_mul_le, now passes t := a and rewrites 1 - a = b.
ProbabilityTheory.bernoulliMeasure_absolutelyContinuous (LMLExplore)	renamed to ProbabilityTheory.bernoulliMeasure_absolutelyContinuous_of_imp, since Statlib owns the name (see below).

What stays in LMLExplore

• bernoulliMeasure_absolutelyContinuous_of_imp: Ber(x, y, p) ≪ Ber(x, y, q) from q = 0 → p = 0 and q = 1 → p = 1, with no MeasurableSingletonClass and no x ≠ y. Statlib's bernoulliMeasure_absolutelyContinuous assumes [MeasurableSingletonClass 𝓧], x ≠ y, q ≠ 0 and q ≠ 1. Both implications then hold vacuously, so Statlib's lemma is a special case of this one. Its docstring now names the difference.
• bernoulliMeasure_absolutelyContinuous_iff, integrableExpSet_bernoulliMeasure, tilted_bernoulliMeasure, LMLExplore.ae_mem_uIcc_bernoulliMeasure and LMLExplore.hasSubgaussianMGF_bernoulliMeasure, which have no Statlib counterpart. They are unchanged.
• LMLExplore.bernoulliKernel : Kernel ℝ ℝ, x ↦ Ber(1, 0, projIcc x), with bernoulliKernel_apply (still rfl), its IsMarkovKernel instance and bernoulliKernel_comp for laws on ℝ supported on [0, 1]. LMLExplore.klBer_integral_le_klDiv uses this statement. The kernel is now defined as (ProbabilityTheory.bernoulliKernel (1 : ℝ) 0).comap (Set.projIcc 0 1 zero_le_one) _. bernoulliKernel_comp is now proved from Statlib's bernoulliKernel_comp_eq_bernoulliMeasure, applied to the image of ρ under the clamp, which replaces the earlier hand computation of the two masses. The kernel is still a separate object from Statlib's, because it is defined on ℝ rather than on I.

The module docstring now says what the file adds to the Statlib file, and its list of main statements drops the removed lemmas.

Checks run

• scripts/build.sh --iofail on the whole library: succeeds, with no warnings.
• #lint in LMLExplore, run from a scratch file that imports the two changed modules: no errors.
• grep over LMLExplore/: bernoulliMeasure_symm no longer appears anywhere. bernoulliMeasure_absolutelyContinuous appears only in the new docstring, which names Statlib's lemma on purpose.

Fixes #330

Roadmap: none

🤖 Generated with Claude Code

https://claude.ai/code/session_0196ftMV379vy48QfzHBVNvo

[prevostad]

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

Undocumented defeq: bernoulliKernel_apply is still (rfl) even though bernoulliKernel is now Kernel.comap of Statlib's kernel; other proofs are acceptable.

• LMLExplore/Probability/Distributions/Bernoulli.lean:163 — bernoulliKernel_apply is closed by (rfl), which unfolds both Kernel.comap and Statlib's ProbabilityTheory.bernoulliKernel definition. Changing either wrapper upstream would break it. Fix: Prove it by rewriting with the API lemmas instead: by rw [bernoulliKernel, Kernel.comap_apply, ProbabilityTheory.bernoulliKernel_apply] (or simp [bernoulliKernel]).

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 · 20s · 99.6k in (89.7k cache read, 9.8k cache write) / 1.9k out tokens · reviewing this diff · rubric}

[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	No public statement changes: klBer_mul_add_mul_le, klBer_one_sub_one_sub, bernoulliKernel_comp and the absolute-continuity lemmas keep their statements, and bernoulliKernel_apply still holds by rfl, so the kernel built with comap is the same object as before. The renamed bernoulliMeasure_absolutelyContinuous_of_imp has the same hypotheses and conclusion as before, and nothing in it is vacuous or narrowed.
✅	reuse	approved	claude/claude-opus-5-5	The PR deletes LMLExplore's copies of the Bernoulli lemmas that Statlib now provides, moves every use to the Statlib declarations, and reproves bernoulliKernel_comp from Statlib's kernel lemma. What remains (bernoulliMeasure_absolutelyContinuous_of_imp, which is more general than Statlib's lemma, and the ℝ-indexed LMLExplore.bernoulliKernel, defined from Statlib's kernel by comap and used by klBer_integral_le_klDiv) does not duplicate anything located in Mathlib or LMLExplore.
✅	scope	approved	claude/claude-opus-5-5	Single-topic refactor that replaces duplicated Bernoulli lemmas and the kernel construction with Statlib's versions; it adds no new mathematical content, so it fits the roadmap by default.
✅	attribution	approved	claude/claude-opus-5-5	The PR swaps duplicated lemmas for the upstream Statlib declarations, and the module and declaration docstrings name the Statlib file and the lemmas used (bernoulliMeasure_swap, bernoulliMeasure_eq_smul_add_smul, bernoulliKernel, bernoulliKernel_comp_eq_bernoulliMeasure). It brings in no new outside material that would need further credit.
✅	api-design	approved	claude/claude-opus-5-5	Duplicated Bernoulli lemmas are deleted with no compatibility layer, every in-repo use is migrated, and the one clashing name becomes bernoulliMeasure_absolutelyContinuous_of_imp. LMLExplore.bernoulliKernel keeps its characterizing @[simp] bernoulliKernel_apply (proved by (rfl)), its Markov instance and bernoulliKernel_comp, with its body still unexposed.
✅	generality	approved	claude/claude-opus-5-5	Special-case LMLExplore lemmas are replaced by Statlib's general versions; the retained bernoulliMeasure_absolutelyContinuous_of_imp is strictly weaker in hypotheses than Statlib's, and the ℝ-indexed kernel and its composition lemma are now derived from Statlib's general kernel rather than reproved.
✅	placement	approved	claude/claude-opus-5-5	The PR deletes the copies Statlib now provides and leaves only what Statlib lacks (the more general absolute-continuity lemma and the ℝ-indexed kernel) in its existing Bernoulli file; the new Statlib import replaces the Tau Ceti measurability import and the now-transitive Mathlib Bernoulli import. The remaining imports are still used: unitInterval.toNNReal_eq_zero comes from LMLExplore.Topology.UnitInterval and integral_id_mem_Icc_of_ae_mem_Icc from LMLExplore.Analysis.Convex.Integral.
✅	naming	approved	claude/claude-opus-5-5	The renamed bernoulliMeasure_absolutelyContinuous_of_imp names its conclusion and implication hypotheses using the of/imp convention, avoids clashing with Statlib's name and does not overstate the statement. The PR switches to Statlib's existing names and introduces no notation.
✅	documentation	approved	claude/claude-opus-5-5	The module docstring now accurately splits what Statlib provides from what the file adds. The renamed bernoulliMeasure_absolutelyContinuous_of_imp, the redefined bernoulliKernel and bernoulliKernel_comp have accurate, non-overclaiming docstrings, and no stale references to removed lemmas remain in the main-statements list.
🟡	proof-quality	changes requested	claude/claude-opus-5-5	Undocumented defeq: bernoulliKernel_apply is still (rfl) even though bernoulliKernel is now Kernel.comap of Statlib's kernel; other proofs are acceptable.

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

_{Reviewing this diff at head 852487d. rubrics @ 7d59664. CLI @ 7d59664. Review spend: $1.13.}