Worked examples: the de Finetti public API #
This file demonstrates the public de Finetti API available from the single facade import
TauCeti.Probability.DeFinetti. The initial bare references give a compact index of the principal
process predicates, implications, representation theorems, uniqueness results, and empirical
convergence statements.
The worked examples then use two complementary descriptions of an exchangeable law. The canonical mixing-law example shows that an i.i.d. path law has a Dirac de Finetti measure. The two affine examples show that a convex combination of two Dirac mixing laws corresponds exactly to the same convex combination of the associated i.i.d. path laws, in both directions. Together they illustrate how the representation theorem and its affine equivalence are used in concrete calculations.
Further worked examples live with the objects they concern: the conditionally i.i.d. coin-flip
construction in Exchangeability/ConditionallyIID/CoinFlips.lean, the constant-witness
characterisation of i.i.d. in ConditionallyIID/Const.lean, and the stationary but
non-exchangeable 3-cycle in Exchangeability/ThreeCycle.lean.
The canonical mixing-law example rests on the uniqueness statement
eq_deFinettiMeasure_of_pathLaw_eq_bind_infinitePi together with the barycentre computation
deFinettiBarycenter_dirac; the affine examples rest on deFinettiEquiv and its values on Dirac
mixing laws and on convex combinations, in both directions. A reader adapting these calculations to
another exchangeable law should start from those results.