chore: safe-subset mathlib cleanup batch (bdd_mul, iterate, pi prob, indicator) (−31 lines)

[cameronfreer]

Summary

Four small, independent mathlib-alignment cleanups, batched into one PR per agreed scope. All proof-body-only with statements unchanged.

Net diff: 6 files, +12 / −43 (−31 lines).

Items

1. Integrable.bdd_mul' → Integrable.bdd_mul (deprecated alias)

Mathlib deprecated the prime-suffixed alias; the canonical name has been available for some time. Straight string substitution at 7 sites across 3 files:

• DeFinetti/ViaMartingale.lean:281, 286
• DeFinetti/ViaKoopman/InfraGeneralized.lean:559
• Probability/TripleLawDropInfo/DropInfo.lean:153, 156, 159, 207

2. Delete local MeasurePreserving.iterate'

DeFinetti/ViaKoopman/CesaroL2ToL1.lean:100 defined a 5-line local lemma proving the iterate of a measure-preserving map is measure-preserving — which is exactly MeasurePreserving.iterate in mathlib (provable via hT.iterate k). The single caller at line 691 switches from MeasurePreserving.iterate' hσ k to hσ.iterate k.

3. Shorten hκ_prob block in Probability/MeasureKernels.lean

The per-ω probability-measure proof for the product kernel κ ω = Measure.pi (fun _ : Fin m => ν ω) was a 6-line tactic block that already used typeclass inference to find Measure.pi.instIsProbabilityMeasure. Collapse the surrounding plumbing (intro ω; classical; haveI; simp; infer_instance) to a 3-line fun ω => by haveI; simp only [κ]; infer_instance, and name the instance in a leading comment so the reader can see what's being inferred.

(Tried exact pi.instIsProbabilityMeasure _ directly but the FQN doesn't resolve in this scope; simp only [κ]; infer_instance is shorter than the FQN form here and clearer than the prior version.)

4. Delete mul_indicator_one_eq_indicator_inter private wrapper

Probability/CondIndep/Indicator.lean:61 defined a 20-line private lemma proving s.indicator 1 * t.indicator 1 = (s ∩ t).indicator 1. Mathlib's Set.inter_indicator_one is exactly this equation in the opposite direction. The single caller at line 162 switches to (Set.inter_indicator_one ..).symm.

Out of scope

DeFinetti/ViaMartingale/IndicatorAlgebra.lean:110 (indProd_mul) was flagged by the audit as "possibly" foldable, but it does manual case-splits on indicator membership inside a Finset.prod, and there's no clean single-named-lemma replacement. Leaving as-is.

The σ-finiteness wrapper trim (ForMathlib/MeasureTheory/Measure/TrimInstances.lean, Probability/CondExpBasic.lean:46) is the next planned PR — different shape (touches local export API), kept separate.

Verification

Check	Baseline (main = 7301d1b)	This branch
lake build	clean (3531 jobs)	clean (3531 jobs)
Axioms (11 theorem decls)	standard only	standard only
Sorries (Exchangeability + ForMathlib)	0	0
Proof-file churn	—	6 files, +12 / −43

Notes

• Built and rebased on top of refactor: delete dead local Kernel.IndepFun.comp duplicate (−41 lines) #22's merge (7301d1b5).
• Item 4 reduces a 20-line private wrapper to a one-call mathlib reference; clearest single win in this batch.