Repository navigation
chore: bump Mathlib to 2ddf59c - #80
Merged
Merged
Conversation
Move Mathlib from 6135ffb to 2ddf59c, the commit Tau Ceti's main pins, so that LML can require Statlib and LMLExplore can sync to it. - `EventuallyEqSet` refactor (mathlib4#45712): a.e. equality of sets is now pointwise `↔`; adapt three proofs. - `enorm` renamed to `eNorm` (mathlib4#45735): fix the `ENorm EReal` instance and the deprecated lemma names; rename `bayesBinaryRisk_eq_lintegral_enorm` to `bayesBinaryRisk_eq_lintegral_eNorm` and two private lemmas to match. - Fix the linter warnings, so that the build is warning-free. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0196ftMV379vy48QfzHBVNvo
Tau Ceti has a `MeasureTheory.Measure.AbsolutelyContinuous.pi` with the same statement, so the two cannot be imported together. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0196ftMV379vy48QfzHBVNvo
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Moves Mathlib from
6135ffbto2ddf59c(2026-11-10), the commit Tau Ceti'smainpins. This lets LML require Statlib, after which LMLExplore can update Tau Ceti, LML and Mathlib together.Fixes for Mathlib changes:
EventuallyEqSetrefactor ([Merged by Bors] - refactor: change the definition ofEventuallyEqSetleanprover-community/mathlib4#45712): a.e. equality of sets is now∀ᵐ x, x ∈ s ↔ x ∈ t. This adaptsIsEVarClass.exists_isLogNumeraireFor,renyiDiv_smul_leftandrenyiDiv_smul_right. It fixes the incompatibility reported in Bumping mathlib to 0867942 would break the build #76.enormrenamed toeNorm([Merged by Bors] - chore: renameenormtoeNormleanprover-community/mathlib4#45735): fixes the field of theENorm ERealinstance and the deprecated lemma names.try,any_goals): the build is now warning-free. Builds downstream run with--iofail, which fails on warnings in dependencies too.Also renames the one Statlib declaration whose name is taken in Tau Ceti
main(4d91513, on the same Mathlib). Two declarations with the same name can't be imported into the same file, so this unblocks using Statlib alongside Tau Ceti, as LMLExplore will. Tau Ceti's lemma has the same statement. I checked by a text scan of declaration names and instance heads.Renamed:
ProbabilityTheory.bayesBinaryRisk_eq_lintegral_enorm→ProbabilityTheory.bayesBinaryRisk_eq_lintegral_eNorm, following Mathlib's rename. It has no uses in Statlib.MeasureTheory.Measure.AbsolutelyContinuous.pi→MeasureTheory.Measure.AbsolutelyContinuous.pi', because the name clashes with Tau Ceti.Supersedes #75 and #77.
Checked locally:
lake build --iofail,lake lintandlake exe mk_all --checkpass. The two steps the Verso tutorial runs in this project also succeed:lake build subverso-extract-modandlake build +Statlib.Inference.Inference:highlighted +Statlib.Inference.QMD:highlighted. Every anchor the tutorial uses is still in place.🤖 Generated with Claude Code
https://claude.ai/code/session_0196ftMV379vy48QfzHBVNvo