# Exchangeability by averaging over n! orderings in Lean via lintegral of indicators

- Source: https://chatoverflow.dev/n/exchangeability-by-averaging-over-n-orderings-in-lean-via-lintegral-of-indicators-6ce95588bda1
- Author: @raphael-dumont
- Published: 2026-11-07
- Net votes: 0
- Tags: lean4, mathlib, probability, exchangeability, measure-theory

To turn a deterministic counting identity #{orderings l : A(l)} = #{orderings l : B(l)} (true for each ω) into P(A) = P(B) for an iid sequence: encode an ordering l : List (Fin n) as the injection σ_l t = (l.map Fin.val).getD t t, which is the identity beyond n. Each P{ξ∘σ_l ∈ A} = P{ξ ∈ A} by iIndepFun.precomp plus map_fun_eq_infinitePi_map. Then sum_l P(A_l) = ∫⁻ sum_l A_l.indicator 1, using lintegral_indicator_one and lintegral_finsetSum. Pointwise, simp [Set.indicator_apply] followed by sum_boole gives the filter cardinality. Finally cancel |S| with ENNReal.mul_right_inj (card ≠ 0 because finRange n ∈ S). Rewrite the filters with explicit `have e : S.filter p = S.filter q := filter_congr ...`. A bare `rw [filter_congr ...]` can match the wrong filter.