Block-product factorisation and the de Finetti summit #
The block-product factorisation of the conditional expectation, and — built directly on it — the de Finetti summit for the reverse-martingale route.
Given that the selected coordinates of a contractable process are conditionally independent over the tail σ-algebra, the conditional expectation of a block-indicator product factors as a product of the directing measure on the coordinate sets:
μ[blockIndicatorProd X k C | tailProcess X] =ᵐ fun ω => ∏ i, (directingMeasure μ X ω).real (C i).
This chains Mathlib's iCondIndepFun_iff_condExp_inter_preimage_eq_mul (conditional independence ⟺
product of indicator conditional expectations) with
Contractable.directingMeasure_ae_eq_condExp_coord (each coordinate's conditional law is the
directing measure). The tail factorization
condExp_blockIndicatorProd_tailProcess_ae_eq_prod (from TailFactorization) then discharges the
finite-block rectangle identity for directingProbabilityMeasure μ X, exactly what
mixedIIDWith_of_forall_rectangles consumes — so the whole chain assembles here.
Main results #
condExp_blockIndicatorProd_prefix_ae_eq_prod_directingMeasure— the prefix block factorization (theL²route proves a stronger, arbitrary-selection form independently, ascondExp_blockIndicatorProd_strictMono_tailProcess_ae_eq_prod_directingMeasureinDeFinetti/ViaL2/BlockFactorization.lean; the overlap is the intended two-route structure and neither file imports the other) at the directing measure, the base case rectangle identities over a contractable process reduce to.mixedIIDWith_of_contractable— a contractable process on a standard Borel sample space is mixed i.i.d., withdirectingProbabilityMeasure μ X(the tail conditional law) as the witness. That witness is the canonical directing measure, not merely a mixing representative; what this file proves about that witness is the mixture identity. The sharp existential theorem on an arbitrary sample space isconditionallyIID_of_contractable; on path space,conditionallyIIDWith_of_contractable_pathSpaceexposes its canonical tail-law witness explicitly.mixedIID_of_contractable— the existential form, for a contractable process on an arbitrary measurable sample space (state space still standard Borel).mixedIID_of_exchangeable— the exchangeable form (viaExchangeable.contractable).
The ..._of_iCondIndepFun_tailProcess theorems expose the intermediate reduction (de Finetti given
tail conditional independence of the coordinates). All of the rectangle-mixture staging lemmas and
the standard-Borel-Ω existential are private (proof staging); the integrability and real/ℝ≥0∞
conversion facts this file runs on are DirectingMeasure/Integral.lean.
The reverse-martingale ("third") proof follows Kallenberg, Probabilistic Symmetries and Invariance
Principles, Theorem 1.1 (pp. 26–28). Adapted from cameronfreer/exchangeability
(DeFinetti/ViaMartingale/CommonEnding.lean and DeFinetti/TheoremViaMartingale.lean, pin
e0532e59ceff23edab44dda9ab0655debbc9cc22); here the factorisation is obtained by reuse of
Mathlib's iCondIndepFun characterisation rather than a hand-rolled π-system.
Block-product factorisation of the conditional expectation (given tail conditional
independence). If the selected coordinates fun i => X (k i) are conditionally independent given
the tail, then the conditional expectation of the block-indicator product factors as
∏ i, (directingMeasure μ X ·).real (C i).
Block law of a rectangle as a directing-measure mixture (given tail conditional
independence). The block law of the rectangle ∏ᵢ C i is the μ-average of the directing-measure
product ∏ i, directingMeasure μ X ω (C i).
de Finetti reduces to conditional independence over the tail (directing-measure form). If
every finite injective selection of coordinates of a contractable process is conditionally
independent given the tail σ-algebra, then the process is mixed i.i.d. with directing
measure the tail conditional law directingProbabilityMeasure μ X.
de Finetti reduces to conditional independence over the tail. The existential form of
mixedIIDWith_of_iCondIndepFun_tailProcess: under the same tail conditional-independence
hypothesis, a contractable process is MixedIID.
Prefix block factorization at the directing measure. For a contractable process, the
conditional expectation of the length-r prefix indicator product given the tail σ-algebra
tailProcess X is a.e. the product of directing-measure evaluations
∏ i, (directingMeasure μ X ω).real (C i) on the coordinate sets.
This is the base case for rectangle identities over a contractable process: a finite block of coordinates is replaced by the directing measure under the tail σ-algebra, and identities for arbitrary selections reduce to it.
de Finetti's theorem, directed form. A contractable process on a
standard Borel space is mixed i.i.d. with witness the tail conditional law
directingProbabilityMeasure μ X.
de Finetti's theorem, mixture form: contractable ⇒ mixed i.i.d. A contractable process
valued in a standard Borel space, on an arbitrary measurable sample space, is mixed i.i.d. This is
the roadmap's mixedIID_of_contractable; the sharp summit conditionallyIID_of_contractable,
which concludes the joint-law disintegration rather than only the mixture identity, is in
TauCeti.Probability.DeFinetti.Theorem.
de Finetti's theorem, mixture form: exchangeable ⇒ mixed i.i.d. An exchangeable process valued in a standard Borel space, on an arbitrary measurable sample space, is mixed i.i.d.