Note: optional CondIndep alignment with mathlib's ProbabilityTheory.CondIndepFun

[cameronfreer]

Tracking a second design observation surfaced during the post-#50 review. Not a planned PR — recording for future reference, paralleling #51.

Observation

Exchangeability/Probability/CondIndep/Basic.lean:78 defines a project-local CondIndep μ Y Z W as a conditional-expectation factorization on indicator products:

def CondIndep (μ : Measure Ω) (Y : Ω → α) (Z : Ω → β) (W : Ω → γ) : Prop :=
  ∀ (A : Set α) (B : Set β), MeasurableSet A → MeasurableSet B →
    μ[ (Set.indicator (Y ⁻¹' A) 1) * (Set.indicator (Z ⁻¹' B) 1)
       | MeasurableSpace.comap W (by infer_instance) ]
    =ᵐ[μ]
    μ[ Set.indicator (Y ⁻¹' A) 1 | … ] * μ[ Set.indicator (Z ⁻¹' B) 1 | … ]

Mathlib (Mathlib/Probability/Independence/Conditional.lean:155) has ProbabilityTheory.CondIndepFun:

def CondIndepFun (f : Ω → β) (g : Ω → γ) (μ : Measure Ω) [IsFiniteMeasure μ] : Prop :=
  Kernel.IndepFun f g (condExpKernel μ m') (μ.trim hm')

The local definition was reasonable pre-bridge but is now duplicating mathlib's kernel-based API.

Potential deletion surface

Following the dependency chain from CondIndep:

• Probability/CondIndep/Basic.lean (definition + symmetry + basic lemmas)
• Probability/CondIndep/Indicator.lean, Probability/CondIndep/Bounded.lean, Probability/CondIndep/Bounded/Approximation.lean, Probability/CondIndep/Bounded/Projection.lean (the surviving extension/projection infrastructure)
• Possibly portions of Probability/CondExp.lean that re-export CondIndep helpers

Eleven files currently reference CondIndep (local API surface):
Probability/CondIndep.lean, Probability/CondIndep/{Basic, Indicator, Bounded, Bounded/Approximation, Bounded/Projection}.lean, Probability/CondExp.lean, DeFinetti/ViaMartingale.lean, DeFinetti/ViaMartingale/{LocalInfrastructure, Factorization, PairLawEquality}.lean.

Architectural tradeoff

The local CondIndep is stated elementarily — indicator products + conditional expectation, no kernel machinery in the type signature. The mathlib CondIndepFun adds:

1. [IsFiniteMeasure μ] in the type signature (vs. local definition which requires [IsProbabilityMeasure μ] only at use sites).
2. [StandardBorelSpace Ω] transitively, because condExpKernel requires it.
3. m' : MeasurableSpace Ω as an explicit argument representing what to condition on — different binder shape than the local (W : Ω → γ) plus implicit comap.

So a migration would need to: (a) add [StandardBorelSpace Ω] to every CondIndep-using lemma that doesn't already have it; (b) rewrite call sites to pass the σ-algebra explicitly rather than via a measurable map W; (c) re-prove the indicator-factorization characterization as a lemma about CondIndepFun (since that's what downstream proofs actually consume).

Three options

1. Migrate to mathlib's CondIndepFun. Delete the local CondIndep definition + custom indicator/extension/projection infrastructure. Significant downstream churn from [StandardBorelSpace Ω] and binder-shape changes.

2. Preserve the local definition. Status quo. Reasoning: the elementary statement is easier to read and the project's other API uses (Y, Z, W)-triples consistently. Mathlib's version is equivalent in our setting but its kernel-based statement is heavier at use sites.

3. Middle path. Keep the local CondIndep as a thin abbreviation / iff-statement over mathlib's CondIndepFun, prove the indicator-factorization characterization once as a bridge lemma, and let downstream code stay on the local API. This preserves the lighter statements at use sites without duplicating the underlying definition.

Recommendation in this repo

Preserve the local definition (option 2) for now. The [StandardBorelSpace Ω] propagation would touch ~11 files and risks regressions in the still-active ViaMartingale proof code, while the LoC savings would be modest (the local definition itself is only 13 lines; the value is in the extension/projection lemmas, which would still need to exist post-migration unless mathlib has direct equivalents).

Option 3 (bridge lemma) is the cleanest middle path if/when we want to align with mathlib without forcing the binder/typeclass changes on every call site.

Filed for future reference, not as a planned PR. Companion to #51.