refactor: Extract general-purpose lemmas to ForMathlib for upstream contribution

[cameronfreer]

Summary

This PR organizes general-purpose lemmas from the exchangeability project into a ForMathlib/ directory structure mirroring mathlib's hierarchy, preparing them for potential upstream contribution.

Changes

New ForMathlib Files (mathlib-only imports)

File	Main Lemmas	Description
Combinatorics/PermutationExtension.lean	exists_perm_extending_injective, exists_perm_extending_strictMono	Injective functions extend to permutations
MeasureTheory/MeasurableSpace/ComapInfima.lean	iInf_comap_eq_comap_iInf_of_surjective	Comap commutes with infima for surjective functions
MeasureTheory/MeasurableSpace/SigmaAlgebraHelpers.lean	aestronglyMeasurable_iInf_antitone	AEStronglyMeasurable preservation under infima
MeasureTheory/Constructions/Pi/Cylinders.lean	isPiSystem_prefixCylinders, measure_eq_of_fin_marginals_eq	π-system infrastructure for prefix cylinders
MeasureTheory/Function/ConditionalExpectation/Lipschitz.lean	condExp_L1_lipschitz	L¹-nonexpansivity of conditional expectation
MeasureTheory/Function/LpHelpers.lean	eLpNorm_two_sq_eq_integral_sq, abs_integral_mul_le_L2	Bridges ENNReal Lp norms and Real integrals
MeasureTheory/Function/AEHelpers.lean	finset_sum_ae_eq	Combine finitely many a.e. equalities
Probability/Kernel/ProductMeasurable.lean	measurable_measure_pi	Product measure kernel measurability via π-systems
Probability/Independence/Conditional.lean	condIndep_of_indicator_condexp_eq	Doob's characterization of conditional independence
Probability/ConditionalExpectation/Distributional.lean	condexp_indicator_eq_of_pair_law_eq	CE equality from distributional equality

Modified Project Files

• Exchangeability/Contractability.lean: Import ForMathlib, re-export exists_perm_extending_strictMono
• Exchangeability/Tail/TailSigma.lean: Import ForMathlib, re-export comap/infima lemmas

Recent Refinements

Generalized lemmas for better mathlib compatibility

PermutationExtension.lean:

• Created exists_perm_extending_injective as the main lemma using Function.Injective k
• Made exists_perm_extending_strictMono a corollary (proof only used injectivity, not order property)

ComapInfima.lean:

• Generalized index type from Type* to Sort* in iInf_comap_eq_comap_iInf_of_surjective
• Consistent with comap_iInf_le which already used Sort*

Removed nolint annotations and unused parameters

SigmaAlgebraHelpers.lean:

• aestronglyMeasurable_iInf_antitone: Removed unused _h_le : ∀ N, m N ≤ m₀ parameter
• aestronglyMeasurable_sub_of_tendsto_ae: Removed unused _hm : m ≤ m₀ parameter

LpHelpers.lean:

• eLpNorm_two_sq_eq_integral_sq: Removed false positive @[nolint unusedArguments]
• memLp_of_abs_le_const: Removed unused (_ : 1 ≤ p) (_ : p ≠ ∞) parameters (MemLp.of_bound doesn't require them)
• abs_integral_mul_le_L2: Removed false positive @[nolint unusedArguments]

All files now have zero nolint annotations and use only necessary parameters.

Module Summaries

Phase 3 Additions

Probability/Independence/Conditional.lean

Doob's characterization of conditional independence (reverse direction):

• condIndep_of_indicator_condexp_eq: If E[1_H | mF ⊔ mG] = E[1_H | mG] a.e. for all H ∈ mH, then mF ⊥⊥ mH | mG

MeasureTheory/Function/AEHelpers.lean

Utility for combining a.e. equalities:

• finset_sum_ae_eq: Combine finitely many a.e. equalities into sum equality

Probability/ConditionalExpectation/Distributional.lean

Bridge from distributional equality to conditional expectation equality:

• condexp_indicator_eq_of_pair_law_eq: If (Y,Z) and (Y',Z) have same law, then E[1_{Y∈B}|σ(Z)] = E[1_{Y'∈B}|σ(Z)] a.e.

Earlier Phases

MeasureTheory/Function/LpHelpers.lean

Bridges ENNReal-valued Lp norms and Real-valued integrals:

• eLpNorm_two_sq_eq_integral_sq: L² norm² = integral of square
• abs_integral_mul_le_L2: Cauchy-Schwarz for L² functions
• setIntegral_le_eLpNorm_mul_measure: |∫_A g| ≤ ‖g‖₂·√(μ A)

MeasureTheory/MeasurableSpace/SigmaAlgebraHelpers.lean

Support for AEStronglyMeasurable with respect to infima:

• aestronglyMeasurable_iInf_antitone: preservation under antitone infima

Probability/Kernel/ProductMeasurable.lean

Measurability of product measure kernels:

• measurable_measure_pi: ω ↦ ∏ᵢ ν(ω) is measurable

Design Decisions

1. Mathlib-only imports: All ForMathlib files import only from mathlib, no Exchangeability.* dependencies
2. Re-exports for backward compatibility: Original declarations re-exported so blueprint references and downstream code continue to work
3. Standard axioms only: All lemmas verified to use only propext, Classical.choice, Quot.sound
4. Style compliance: All lines < 100 chars, comprehensive module docstrings
5. Golfed proofs: Proofs simplified using existing mathlib lemmas:
   • isPiSystem_pi, generateFrom_pi (ProductMeasurable)
   • condExp_mul_of_stronglyMeasurable_right (Lipschitz)
   • Equiv.ofInjective (PermutationExtension)
   • inter_indicator_one (Conditional)
   • indicator_comp_right, setIntegral_indicator (Distributional)
   • Lighter imports where possible (AEHelpers uses MeasureSpace instead of ConditionalExpectation.Basic)

Axiom Verification

$ #print axioms Combinatorics.exists_perm_extending_injective
[propext, Classical.choice, Quot.sound]

$ #print axioms ProbabilityTheory.condIndep_of_indicator_condexp_eq
[propext, Classical.choice, Quot.sound]

$ #print axioms MeasureTheory.finset_sum_ae_eq
[propext, Classical.choice, Quot.sound]

$ #print axioms ProbabilityTheory.condexp_indicator_eq_of_pair_law_eq
[propext, Classical.choice, Quot.sound]

PR Sequencing (for future mathlib PRs)

Level 0 (independent - can be submitted in parallel):
  PR1: PermutationExtension - pure combinatorics
  PR2: ComapInfima - σ-algebra infrastructure
  PR3: TrimInstances - already essentially in mathlib

Level 1 (after Level 0):
  PR4: Cylinders - π-system infrastructure
  PR5: Lipschitz - conditional expectation helpers
  PR6: LpHelpers - Lp norm/integral bridges
  PR7: SigmaAlgebraHelpers - AEStronglyMeasurable for infima
  PR8: AEHelpers - finset_sum_ae_eq utility

Level 2 (after Level 1):
  PR9: ProductMeasurable - uses π-system infrastructure
  PR10: Independence/Conditional - Doob's characterization
  PR11: ConditionalExpectation/Distributional - CE equality from dist equality

Test plan

• lake build passes
• All ForMathlib files have mathlib-only imports
• Axiom verification passes for all main lemmas
• Line lengths < 100 chars
• Blueprint references still valid (declarations re-exported)
• Zero nolint annotations remaining

References

• Kallenberg (2005), Probabilistic Symmetries and Invariance Principles, Theorem 1.1
• Williams (1991), Probability with Martingales