Simplify via mathlib v4.30.0: replace upstreamed/missed helpers

[cameronfreer]

Summary

Post-upgrade audit: replace repo helpers that mathlib v4.30.0 now covers (recently upstreamed or previously missed). Survey first confirmed the major infrastructure must stay local — mathlib still has no de Finetti/exchangeability, no Lévy downward (reverse-martingale) convergence, no von Neumann mean ergodic theorem, no Koopman operator, and no finite-product kernels. InfiniteProduct.lean already wraps mathlib's Measure.infinitePi.

Deleted (mathlib equivalent exists)

Old helper	Mathlib replacement	Call sites patched
Finset.filter_val_lt_card	Fin.card_filter_val_lt (+ min_eq_right)	2 — and Util/FinsetHelpers.lean deleted (sole content)
Exchangeability.Probability.integrable_of_bounded	Integrable.of_bound	6
MeasureTheory.integrable_of_bounded_measurable	Integrable.of_bound	10
MeasureTheory.memLp_two_of_bounded	MemLp.of_bound	3
Exchangeability.Probability.condExp_mul_pullout (the Probability/CondExp.lean one)	intentional API break — public lemma removed with no wrapper kept (zero call sites in-repo). External users: migrate to mathlib's condExp_mul_of_stronglyMeasurable_right (right-factor form). The same-named ViaKoopman lemma (different statement, left-factor pull-out, already a thin wrapper over condExp_mul_of_aestronglyMeasurable_left) is the one in use and is unchanged	0

Shrunk (signature unchanged unless noted)

• injective_implies_strictMono_perm: 64-line orderIsoOfFin construction → one line via Tuple.sort + Monotone.strictMono_of_injective.
• eLpNorm_two_sq_eq_integral_sq: ~55 lines → 8 via MemLp.eLpNorm_eq_integral_rpow_norm. Statement change (approved): [IsFiniteMeasure μ] dropped — the new proof doesn't need it; strictly more general, call sites unaffected. Isolated in its own commit (refactor!).

Attempted and reverted (audit claim didn't survive contact)

aestronglyMeasurable_sub_of_tendsto_ae was slated for replacement by mathlib's aestronglyMeasurable_of_tendsto_ae, but that lemma only covers the m = m₀ case — its AEStronglyMeasurable is taken at the measure's own σ-algebra. The repo helper's entire point is AEStronglyMeasurable[m] for a strict sub-σ-algebra m < m₀ via a limsup witness. The helper stays, with a docstring note recording why; it's now the top upstream candidate.

Kept (verified absent from mathlib v4.30.0) — upstream candidates

aestronglyMeasurable_sub_of_tendsto_ae and aestronglyMeasurable_iInf_antitone (sub-σ-algebra measurability under limits/infima), abs_prod_sub_prod_le (telescoping product bound), measurable_measure_pi/aemeasurable_measure_pi (measurability of finite product-measure families — no Kernel.pi in mathlib), eLpNorm_one_eq_integral_abs, dist_toLp_eq_eLpNorm_sub, eLpNorm_lt_of_integral_sq_lt, eLpNorm_two_from_integral_sq_le, strictMono_Fin_ge_id, pushforward-integral wrappers, lintegral_fatou_ofReal_norm, condExp_L1_lipschitz (mathlib has only the one-function integral_abs_condExp_le).

Artifacts

Module count 103 → 102: import_graph_colored.{svg,png,html} regenerated (same procedure as #132; colors carried per module; embedded GEXF re-validated at 102 nodes / 151 edges; only the FinsetHelpers-incident edge dropped). File count and STATUS.md LOC table refreshed.

Verification

• lake build: clean, zero warnings
• sorry scan: 0 (gate run without --report-only)
• #print axioms deFinetti: exactly [propext, Classical.choice, Quot.sound] (CI gate keeps passing)
• lake exe checkdecls blueprint/lean_decls and blueprint/check_blueprint.py (52/52): pass
• No blueprint-cited declarations touched