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

[cameronfreer]

Summary

Careful upgrade from Lean/mathlib v4.30.0-rc2 to the stable v4.30.0 tags, following the same pattern as the previous bump (#17): one pure bump commit, one fixup commit, one deprecation sweep.

Bump (chore(bump))

• lean-toolchain: leanprover/lean4:v4.30.0-rc2 → v4.30.0
• lakefile.toml: mathlib rev → v4.30.0 (c5ea0035)
• lake-manifest.json regenerated via lake update mathlib. Dependency movements: aesop/Qq/Cli → v4.30.0 tags, proofwidgets v0.0.98 → v0.0.99, batteries → main pin per mathlib's manifest, plausible/importGraph bumped; checkdecls and LeanSearchClient unchanged.
• Mathlib cache: hit for the stable tag (8,459 files).

Fixups (fix(bump)) — one file, three root causes

All breakage was confined to Exchangeability/DeFinetti/ViaL2/CesaroConvergence/L2.lean:

1. zero_le (ENNReal/canonically-ordered) no longer takes its argument explicitly — 2 sites.
2. tendsto_setIntegral_of_L1' now takes AEStronglyMeasurable f μ where it previously took Integrable f μ.
3. integral_finset_sum deprecation in the same file (renamed in the sweep family below).

Deprecation sweep (chore) — 45 warnings → 0

• camelCase renames across 27 files: integral_finset_sum → integral_finsetSum, integrable_finset_sum → integrable_finsetSum, condExp_finset_sum → condExp_finsetSum, tendsto_finset_sum → tendsto_finsetSum, tendsto_finset_prod → tendsto_finsetProd, Measurable.ennreal_tsum → Measurable.tsum.
• Attribute migration: @[measurability, fun_prop] on Measurable lemmas → @[fun_prop]. The 3 MeasurableSet lemmas keep @[measurability]. No measurability tactic call sites exist in the repo, so this is tag hygiene only.

Why the attribute churn? v4.30.0 reimplements mathlib's measurability tactic on top of fun_prop (see Mathlib/Tactic/Measurability.lean). The @[measurability] attribute is now a compatibility shim that branches on the statement's shape:

• For function-property statements (Measurable f, AEMeasurable f, StronglyMeasurable f, AEStronglyMeasurable f μ) it silently registers the lemma as @[fun_prop] and warns "Use @[fun_prop] instead" — the old spelling is just an alias there, so this PR writes the tag the machinery actually uses.
• For MeasurableSet s statements — set-level facts outside fun_prop's function-composition model — it still registers an aesop rule in the Measurable rule set, with no deprecation. Tagging these with @[fun_prop] is a hard error (unrecognized function property, verified during this upgrade), which is why extendSet_measurable, cylinder_measurable, and firstRCylinder_measurable_ambient keep @[measurability].

Docs

• DEVELOPMENT_CHRONOLOGY.md Phase 11 bullet notes the stable bump.

Import graph

No regeneration needed: lake exe graph --to Exchangeability output matches the committed artifacts exactly (103 nodes / 152 edges, zero node or edge diff) — fixups touched proof bodies and attributes only, no import lines.

Verification

• lake build: clean, zero warnings (was 45 post-bump)
• sorry_analyzer: 0 sorries
• #print axioms deFinetti: [propext, Classical.choice, Quot.sound] — exact line, so the CI axiom gate added in Quality pass: comment hygiene, helper consolidation, golf, docs+CI axiom check #132 keeps passing
• lake exe checkdecls blueprint/lean_decls: pass
• python3 blueprint/check_blueprint.py: 52/52 consistent
• No theorem statements, docstrings, or axioms changed