bump Lean to v4.30.0-rc2 + mathlib v4.30.0-rc2 by cameronfreer · Pull Request #17 · cameronfreer/exchangeability

cameronfreer · 2026-05-18T00:50:36Z

Summary

Bumps the toolchain from leanprover/lean4:v4.27.0-rc1 to leanprover/lean4:v4.30.0-rc2 and the
mathlib pin to the matching tag.

Scope: bump + minimal source changes needed to compile. No refactors, no linting cleanup, no proof
golfing. Refactor-against-new-mathlib-APIs work (stieltjesOfMeasurableRat,
IsCondKernelCDF.toKernel, Equiv.Perm.exists_extending_pair, condExpKernel,
Kernel.IndepFun.comp) will land as a stream of small targeted PRs on top of this baseline.

Commits

Commit	Scope
`chore(bump)`	`lean-toolchain` + `lakefile.toml` mathlib rev + `lake-manifest.json`
`fix(bump): tier 0-1`	`Tail/TailSigma.lean`
`fix(bump): tier 2`	`Probability/Martingale/Crossings.lean`
`fix(bump): tier 4`	`DeFinetti/ViaL2/{AlphaConvergence,AlphaIicCE,CesaroConvergence,DirectingMeasu
reIntegral,MoreL2Helpers}.lean`,` DeFinetti/ViaMartingale/FutureFiltration.lean`,
`DeFinetti/ViaKoopman/ContractableFactorization.lean`

Tier 3 (CommonEnding / Ergodic / Contractability) skipped — nothing broke there.

Mathlib breakage clusters

Renames:

Adapted → StronglyAdapted (mathlib renamed on 2026-01-13; the new Adapted requires plain
Measurable, while the pre-rename Adapted is now StronglyAdapted)
integral_mul_left → integral_const_mul
Set.indicator_of_not_mem → Set.indicator_of_notMem; Set.not_mem_compl_iff →
Set.notMem_compl_iff
hasFiniteIntegral_of_bounded → HasFiniteIntegral.of_bounded
Ne.lt_or_lt → Ne.lt_or_gt
StrictAnti.lt_iff_lt → StrictAnti.lt_iff_gt
le_of_not_lt (generic) removed; use not_lt.mp

Behavior changes:

simp only [name] no longer unfolds opaque defs reliably; two call sites replaced with
show-of-the-unfolded-form. Affected: futureFiltration and TailSigma.tailFamily.
One simp only [ξ, p, q] produces a different normal form, so a calc LHS no longer matches;
collapsed three pure-ring calc steps into one bridging step (CesaroConvergence.lean:1119).
congr 1; ext k; rw [MeasurableSpace.comap_comp] no longer closes; replaced with
iSup_congr-driven step plus rfl (TailSigma.lean).

Verification

Check	Baseline (main)	Post-bump	Match?
`lake build`	clean (3296 jobs)	clean (3531 jobs)	✓
Axiom set (theorem files, 11 decls)	standard only (`propext`, `Quot.sound`, `Classical.choice`)
standard only	✓
Sorries (`Exchangeability` + `ForMathlib`)	0	0	✓
Proof-file churn (`*.lean`)	—	9 files, +32 / −36 (net −4)	well within no-refactors budget
Manifest/toolchain churn	—	3 files, +20 / −19	expected (transitive deps re-pinned by `lake
update mathlib`)

Notes for review

Do not carry over PR chore: autoGolf proof bodies across 61 files (−841 lines) #16 (auto-golf) changes. PR chore: autoGolf proof bodies across 61 files (−841 lines) #16 has a blocker at Probability/CondExpExtras.lean:1842 (broken suffices syntax) and an unsolved condExp_project_of_condIndepFun at line 354; it stays parked as a mined-suggestion source. This bump branch does not touch CondExpExtras.lean because the bump itself did not require it.
The bigger refactor opportunities — Route B against MeasurableStieltjes / CondCDF / CDFToKernel, Adapted/StronglyAdapted cleanup, permutation extension via Equiv.Perm.exists_extending_pair (mathlib #34599) — are out of scope here. They are the planned follow-up PRs.

Test plan

Reviewer confirms lake build is clean on a fresh clone of this branch.
Reviewer spot-checks the 9 proof-file changes against the rename rationale in the tier commit messages.
Reviewer confirms no unexpected behavior changes (e.g. the StronglyAdapted rename's semantic consequences in Crossings.lean).
Do not merge before review.

Bumps the toolchain from v4.27.0-rc1 to v4.30.0-rc2 and the mathlib pin to the matching tag. No source changes in this commit; build fixups for breakage introduced by the bump follow in subsequent tier commits. - lean-toolchain: leanprover/lean4:v4.27.0-rc1 -> v4.30.0-rc2 - lakefile.toml: mathlib rev v4.27.0-rc1 -> v4.30.0-rc2 - lake-manifest.json: regenerated via `lake update mathlib`

`comap_shift_eq_iSup_comap_coords` no longer closes via `congr 1; ext k; rw [MeasurableSpace.comap_comp]` at v4.30.0-rc2: after the rewrite a residual `comap ((eval k) ∘ shift n) inst = comap (eval (n+k)) inst` is left, which is definitionally true but not closed by `congr` alone. Use `iSup_congr (fun k => ?_)` for the supremum, then `rw [MeasurableSpace.comap_comp]; rfl`. - Exchangeability/Tail/TailSigma.lean: replace `congr 1; ext k` step

mathlib renamed `Adapted` -> `StronglyAdapted` on 2026-01-13 (see Mathlib/Probability/Process/Adapted.lean header note); the new `Adapted` requires plain `Measurable`, while the pre-rename `Adapted` (which the local proofs target) is now `StronglyAdapted`. The body `stronglyMeasurable_condExp.mono (h_le n)` already produces `StronglyMeasurable`, so only the annotation needs the rename. - Exchangeability/Probability/Martingale/Crossings.lean: rename two `have h_adapted : Adapted ℱ ...` annotations to `StronglyAdapted ℱ ...` (lines 594 and 621).

Mathlib API renames between v4.27.0-rc1 and v4.30.0-rc2: - `integral_mul_left` -> `integral_const_mul` (ViaKoopman/ContractableFactorization.lean:752, ViaL2/AlphaConvergence.lean:320, ViaL2/MoreL2Helpers.lean:1386, ViaL2/DirectingMeasureIntegral.lean:1933) - `Set.indicator_of_not_mem` -> `Set.indicator_of_notMem` `Set.not_mem_compl_iff` -> `Set.notMem_compl_iff` (15 occurrences in ViaL2/DirectingMeasureIntegral.lean) - `hasFiniteIntegral_of_bounded` -> `HasFiniteIntegral.of_bounded` (ViaL2/MoreL2Helpers.lean:1307) - `Ne.lt_or_lt` -> `Ne.lt_or_gt` (signature renamed) (ViaL2/CesaroConvergence.lean:376) - `StrictAnti.lt_iff_lt` -> `StrictAnti.lt_iff_gt` (ViaL2/AlphaIicCE.lean:438) - `le_of_not_lt` -> `not_lt.mp` (generic lemma removed; use `not_lt` iff) (ViaL2/CesaroConvergence.lean:1526) Two `simp only` calls on `def`s no longer make progress at v4.30 (simp no longer auto-unfolds opaque `def`s). Replace with `show` of the unfolded form: - `simp only [futureFiltration]` -> `show … comap (shiftRV …) _` (ViaMartingale/FutureFiltration.lean:130) - `simp only [TailSigma.tailFamily]` -> `show … iSup (fun j => …)` (ViaL2/CesaroConvergence.lean:1995) One `calc` step LHS no longer matches the goal LHS after `simp only [ξ, p, q]` (different normal form in v4.30); collapse the three pure-`ring` calc steps into one bridging step from the new goal LHS form: - ViaL2/CesaroConvergence.lean:1119

Two open-coded initial-segment inclusions are replaced with the mathlib spelling `Fin.castLE`. Both substitutions are in let-bindings inside proof bodies (statements unchanged): - Exchangeability/Contractability.lean:470 — `contractable_of_exchangeable` call site: `let ι := fun i => ⟨i.val, Nat.lt_of_lt_of_le i.isLt hmn⟩` -> `let ι := Fin.castLE hmn`. Existing `simpa [ι]` and `simp [..., ι]` unfold the new RHS the same way; no other proof changes needed. - Exchangeability/Util/FinsetHelpers.lean:32 — `filter_val_lt_card`: same substitution; the inline `hf_inj` proof collapses to `Fin.castLE_injective h`, and the `Finset.image` branch's `simp only [f]` steps simplify directly via `Fin.ext rfl` / `rintro ⟨j, rfl⟩`. (`Contractability.lean:408` was deliberately left alone — that `let` is inside a lemma statement, not the proof body, and the agreed scope is proof-body-only churn.) README.md:51 was still claiming `lean-toolchain` was pinned to 4.27.0-rc1; the v4.30.0-rc2 bump (#17) missed updating it. Rather than re-pin and re-drift, point at the file itself: "(see `lean-toolchain` for the pinned version)".

After the v4.30.0-rc2 bump (#17) the project had a few dozen deprecation warnings sitting in the build output. This sweep zeroes them out. Tactic rename: - push_neg at h -> push Not at h (25 sites across 10 files) Deprecated import path: - Mathlib.Probability.Independence.Kernel -> Mathlib.Probability.Independence.Kernel.IndepFun (Exchangeability/DeFinetti/ViaKoopman/InfraCore.lean:12). The old path was a `deprecated_module` stub that just re-imported the new one, so this is a transparent swap. Theorem name renames: - eLpNorm_eq_lintegral_rpow_enorm -> eLpNorm_eq_lintegral_rpow_enorm_toReal (Exchangeability/Probability/LpNormHelpers.lean:71). Same signature. - Fin.lt_iff_val_lt_val -> Fin.lt_def (Exchangeability/DeFinetti/ViaMartingale/FutureRectangles.lean:57). - Nat.lt_succ removed from a simp arg in Exchangeability/DeFinetti/ViaKoopman/CesaroL2ToL1.lean:284 — was both deprecated and (per the linter) unused; surrounding `omega` closes the goal regardless. - measureReal_univ_eq_one -> probReal_univ (6 sites, all in Exchangeability/DeFinetti/ViaL2/DirectingMeasureIntegral.lean). Not in the original audit list but the same character of fix; folded in so this PR is a complete deprecation sweep. After this change: `lake build` is clean and produces zero "has been deprecated" warnings (verified by grep over the build log). Build remains 3527 jobs (one fewer than baseline, because the deprecated `Independence.Kernel` stub is no longer pulled in). Statements, axioms, sorries all unchanged.

cameronfreer added 4 commits May 17, 2026 17:54

cameronfreer merged commit 8ab88df into main May 18, 2026

This was referenced May 18, 2026

docs(blueprint): article-class restructure, narrative, examples, conclusion #19

Open

refactor: thin exists_perm_extending_strictMono via mathlib API (−46 lines) #18

Merged

chore: Fin.castLE consistency + README version drift fix #21

Merged

cameronfreer mentioned this pull request May 18, 2026

chore: clear all 4.30 deprecation warnings (push_neg, deprecated names + import) #26

Merged

cameronfreer mentioned this pull request Jun 10, 2026

Upgrade to Lean v4.30.0 + mathlib v4.30.0 (stable) #133

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

bump Lean to v4.30.0-rc2 + mathlib v4.30.0-rc2#17

bump Lean to v4.30.0-rc2 + mathlib v4.30.0-rc2#17
cameronfreer merged 4 commits into
mainfrom
bump-4.30.0-rc2

cameronfreer commented May 18, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

cameronfreer commented May 18, 2026

Summary

Commits

Mathlib breakage clusters

Verification

Notes for review

Test plan

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant