Quality pass: comment hygiene, helper consolidation, golf, docs+CI axiom check#132
Merged
Conversation
Per the project style rule (describe what code is, not what it was): - AlphaIicCE.lean: the 'BorelSpace synthesis issue' note described a problem the proof below no longer has - L2Helpers.lean, DirectingMeasureIntegral.lean, AlphaIicEq.lean, CommonEnding.lean: drop 'previously'/'earlier drafts' phrasing
…into shared Probability helpers
Intentional API cleanup (breaking for external users of these names):
- condExp_const_mul: removed; the two call sites in CesaroHelpers now use
mathlib's condExp_smul directly
- condExp_sum_finset: now a private lemma in its only consumer,
CesaroHelpers.lean
- integrable_of_bounded_measurable, eLpNorm_one_le_eLpNorm_two_toReal:
moved to Probability/LpNormHelpers.lean (namespace MeasureTheory)
- lintegral_fatou_ofReal_norm: moved from MartingaleExtras.lean into
Probability/IntegrationHelpers.lean
Module count 105 -> 103: regenerated import_graph_colored {svg,png}
(same procedure as 722fba0, colors carried over per module) and
refreshed file counts in README.md / home_page/index.md.
- Contractability.lean: strictMono_all_lt_succ_last to term mode; inline h_mono into the calc; inline hf/hg into the obtain - Core.lean: cylinder_subset_prefixCylinders uses the definitional equality directly instead of an explicit rfl-transport Statements unchanged; remaining find_golfable candidates skipped where the existing structure is clearer.
- DEVELOPMENT_CHRONOLOGY.md: header recounted from git (4,247 commits, 3,373 non-merge, through June 8 2026); new Phase 11 covering the Jan 9 - June 8 maintenance period - blueprint.yml: after the build, #print axioms output for deFinetti is diffed against the expected single line, so any added axiom fails CI
…unt convention - import_graph_colored.html: re-embed the GEXF from the current import graph (lake exe graph; 103 modules, includes the new LpNormHelpers->CesaroHelpers and IntegrationHelpers->AntitoneLimit edges). The page's own JS computes colors, so the proof-palette view is unchanged. - import_graph_full_declarations.html: drop the 5 declaration nodes (and their 5 edges) for the deleted ViaKoopman/LpCondExpHelpers from the Feb snapshot; arrays re-validated (426 nodes / 468 edges, no dangling ids). The live copy is rebuilt by docgen CI on push to main. - DEVELOPMENT_CHRONOLOGY.md: Phase 11 count was time-of-day dependent (bare --since date); now 226 commits (208 non-merge) with the explicit --since="2026-01-09 00:00" convention stated inline.
This was referenced Jun 10, 2026
cameronfreer
added a commit
that referenced
this pull request
Jun 11, 2026
* refactor: replace 4 helpers with mathlib v4.30.0 equivalents - Finset.filter_val_lt_card -> Fin.card_filter_val_lt (2 sites); Util/FinsetHelpers.lean deleted (sole content) - integrable_of_bounded (Probability/CondExp.lean) -> Integrable.of_bound (6 sites in CesaroL1Bounded) - integrable_of_bounded_measurable (LpNormHelpers) -> Integrable.of_bound (10 sites across ViaKoopman) - memLp_two_of_bounded (LpNormHelpers) -> MemLp.of_bound (3 sites) NOT migrated (audit claim didn't survive contact with the real call sites): aestronglyMeasurable_sub_of_tendsto_ae stays — mathlib's aestronglyMeasurable_of_tendsto_ae only covers the m = m0 case, while this helper's purpose is AEStronglyMeasurable[m] for m < m0 via a limsup witness; its docstring now records that. * refactor: collapse injective_implies_strictMono_perm onto Tuple.sort; drop dead condExp_mul_pullout - injective_implies_strictMono_perm: 64-line orderIsoOfFin construction -> one-liner via Tuple.sort + Monotone.strictMono_of_injective (signature unchanged) - Probability/CondExp.lean condExp_mul_pullout: deleted — zero call sites; the same-named ViaKoopman/InfraGeneralized lemma (the one actually used, already a thin wrapper over mathlib's condExp_mul_of_aestronglyMeasurable_left) is unchanged * refactor!: eLpNorm_two_sq_eq_integral_sq — shrink proof, drop IsFiniteMeasure The new proof goes through MemLp.eLpNorm_eq_integral_rpow_norm and does not need [IsFiniteMeasure μ]; the hypothesis is dropped (user-approved signature weakening — strictly more general, call sites unaffected). ~55 lines of lintegral manipulation -> 8 lines. * chore(artifacts): regenerate import graph (103 -> 102 modules) + refresh counts Util/FinsetHelpers.lean deletion drops one module: SVG/PNG/HTML regenerated via the PR #132 procedure (colors carried per module; 102 clickable SVG nodes; embedded GEXF re-validated, 102 nodes / 151 edges); home_page file count and STATUS.md LOC table refreshed. * style: drop blank line at EOF in SigmaAlgebraHelpers Also recording here (per review): commit ccc9c6c's removal of the public lemma Exchangeability.Probability.condExp_mul_pullout is an intentional breaking API change — it had zero call sites in this repo and no wrapper is kept; external users should migrate to mathlib's condExp_mul_of_stronglyMeasurable_right (right-factor form) or the ViaKoopman condExp_mul_pullout (left-factor, shift-invariant form).
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
1 participant
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.
Summary
A four-part quality pass over the completed formalization (0 sorries and standard axioms before and after; full
lake build,checkdecls, andcheck_blueprint.pyall pass).1. Comment hygiene
Rewrote 5 historical comments to describe current state per the project style rule, including the stale "BorelSpace synthesis issue" note on
alphaIicCE_measurable(the proof below it already works) and "previously"/"earlier drafts" phrasing inL2Helpers.lean,DirectingMeasureIntegral.lean,AlphaIicEq.lean,CommonEnding.lean.2. Helper consolidation — intentional API break
Exchangeability.DeFinetti.ViaKoopman.LpCondExpHelpersno longer exists as an importable module, andExchangeability.Probability.MartingaleExtrasis gone too. Migration:condExp_const_mulMeasureTheory.condExp_smulcondExp_sum_finsetprivatein its only consumer,ViaKoopman/CesaroHelpers.leanintegrable_of_bounded_measurableMeasureTheory.integrable_of_bounded_measurableinProbability/LpNormHelpers.leaneLpNorm_one_le_eLpNorm_two_toRealMeasureTheory.eLpNorm_one_le_eLpNorm_two_toRealinProbability/LpNormHelpers.leanExchangeability.Probability.lintegral_fatou_ofReal_normExchangeability.Probability.IntegrationHelpers.lintegral_fatou_ofReal_normOnly 3 proof-call-site lines changed library-wide. Module count 105 → 103:
import_graph_colored.{svg,png}regenerated with the same procedure as 722fba0, with each surviving module keeping its color; file counts refreshed inREADME.md/home_page/index.md/STATUS.md. As in 722fba0,import_graph_colored.htmlandimport_graph_full_declarations.htmlare not regenerated here (interactive viewer coloring / doc-gen4 CI artifact).3. Proof golf
4 of 9
find_golfablecandidates applied (Contractability.lean,Core.lean); statements untouched (the two blueprint-cited theorems' citations verified viacheckdecls). The remaining 5 were skipped where the existing structure was clearer or the golf broke elaboration.4. Docs + CI
DEVELOPMENT_CHRONOLOGY.md: header recounted from git (4,247 commits / 3,373 non-merge through June 8, 2026) and a new Phase 11 covering Jan 9 – June 8 (toolchain to v4.30.0-rc2, dead-code sweeps, linter-suppression cleanup to zero, blueprint/CI refresh).blueprint.yml: new Check axioms step diffs the full#print axioms Exchangeability.DeFinetti.deFinettioutput against the expected single line — exact match, so any added axiom or extra output fails CI. Simulated locally end-to-end.Verification
lake build: 3525/3525 jobssorry_analyzer: 0 sorries#print axioms deFinetti:[propext, Classical.choice, Quot.sound]lake exe checkdecls blueprint/lean_decls: passpython3 blueprint/check_blueprint.py: 52/52 consistent.leanfiles compile individually