The conditional rectangle common ending for de Finetti

This file supplies the joint-law companion of the mixture rectangle common ending. To prove that a measurable random probability measure ν : Ω → ProbabilityMeasure α directs a coordinatewise μ-a.e. measurable family, it is enough to verify the expected disintegration on sets of the form

S ×ˢ Set.univ.pi B

where S is measurable in ProbabilityMeasure α and B is a measurable finite rectangle in the block coordinates. These sets form a π-system generating the joint product σ-algebra, so equality there extends to the full joint-law identity in ConditionallyIIDWith.

Main results

• conditionallyIID_of_jointRectangles — the Layer 1 common ending, at a named directing measure;
• conditionallyIIDWith_of_measure_inter_blockCylinder_eq_setLIntegral — a set-integral factorization of the mass of a directing-measure event met with a block cylinder, converted here into the joint-rectangle identity above. A reusable seam assuming no standard-Borel structure on either space: all three de Finetti routes consume it;
• ConditionallyIIDWith.jointLaw_prod_univ_pi — the converse rectangle identity;
• conditionallyIIDWith_iff_forall_jointRectangles and conditionallyIID_iff_exists_forall_jointRectangles — characteristic forms for the named and existential predicates.

This advances TauCetiRoadmap/Exchangeability/README.md, Layer 1, the conditional common ending conditionallyIID_of_jointRectangles. The joint-law formulation is Kallenberg's conditional i.i.d. identity (Probabilistic Symmetries and Invariance Principles, 2005, §1.1, equation (2)). The rectangle-extension argument is the joint-space analogue of the common-ending strategy in cameronfreer/exchangeability (DeFinetti/CommonEnding.lean, pin e0532e59ceff23edab44dda9ab0655debbc9cc22), adapted to Tau Ceti's stronger ConditionallyIIDWith predicate and Mathlib's generateFrom_eq_prod, generateFrom_pi, and π-system API.

theorem TauCeti.Probability.conditionallyIID_of_jointRectangles {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {ι : Type u_3} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (hX : ∀ (i : ι), AEMeasurable (X i) μ) (hν : Measurable ν) (h_rect : ∀ (m : ℕ) (k : Fin m → ι), Function.Injective k → ∀ (S : Set (MeasureTheory.ProbabilityMeasure α)), MeasurableSet S → ∀ (B : Fin m → Set α), (∀ (i : Fin m), MeasurableSet (B i)) → (MeasureTheory.Measure.map (fun (ω : Ω) => (ν ω, fun (i : Fin m) => X (k i) ω)) μ) (S ×ˢ Set.univ.pi B) = (μ.bind fun (ω : Ω) => (MeasureTheory.Measure.dirac (ν ω)).prod ↑(MeasureTheory.ProbabilityMeasure.pi fun (x : Fin m) => ν ω)) (S ×ˢ Set.univ.pi B)) : ConditionallyIIDWith μ X ν

Conditional common de Finetti ending. If the joint law of a measurable random probability measure ν and every injective finite block agrees with ∫ δ_{ν(ω)} ⊗ (ν(ω))^{⊗m} ∂μ(ω) on all measurable products of a set in the ν coordinate and a rectangle in the block coordinates, then ν directs the family.

theorem TauCeti.Probability.conditionallyIIDWith_of_measure_inter_blockCylinder_eq_setLIntegral {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hX_meas : ∀ (n : ℕ), AEMeasurable (X n) μ) {ν : Ω → MeasureTheory.ProbabilityMeasure α} (hν : Measurable ν) (hcore : ∀ (r : ℕ) (k : Fin r → ℕ), StrictMono k → ∀ (S : Set (MeasureTheory.ProbabilityMeasure α)), MeasurableSet S → ∀ (B : Fin r → Set α), (∀ (i : Fin r), MeasurableSet (B i)) → μ (ν ⁻¹' S ∩ blockCylinder X k B) = ∫⁻ (ω : Ω) in ν ⁻¹' S, ∏ i : Fin r, ↑(ν ω) (B i) ∂μ) : ConditionallyIIDWith μ X ν

Set-integral common de Finetti ending. If for every strictly monotone block the mass of a directing-measure event met with a block cylinder is the set-integral of the product of the witness's evaluations, then the witness directs the process.

ConditionallyIIDWith quantifies over arbitrary injective selections, but a caller need only supply the monotone case: the reduction by sorting happens here. That matches what the proof routes naturally produce, since a block argument reads disjoint windows in increasing order.

This theorem is, alone among the rectangle endings, stated for a sequence. The obstruction is inherited rather than intrinsic: the statement is phrased with blockCylinder, which Process/Cylinder.lean defines only for X : ℕ → Ω → α, and the sorting reduction needs a linear order on the index — hence ℕ. The others quantify over an arbitrary index type.

This is a reusable seam: nothing here mentions how ν was built, so a route supplies only its own factorization identity. The martingale route reaches it from tail conditional laws and consumes it in conditionallyIIDWith_of_contractable_pathSpace; the L² route reaches it from its own block factorization; and the Koopman route conditions on the shift-invariant σ-algebra instead and consumes it in ContractableLaw.conditionallyIIDWith_invariantConditionalProbabilityMeasure.

In particular there is no standard-Borel or non-empty hypothesis on either space: those are needed to construct a directing measure, not to recognise one.

theorem TauCeti.Probability.ConditionallyIIDWith.jointLaw_prod_univ_pi {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {ι : Type u_3} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : ConditionallyIIDWith μ X ν) {m : ℕ} (k : Fin m → ι) (hk : Function.Injective k) (S : Set (MeasureTheory.ProbabilityMeasure α)) (B : Fin m → Set α) : (MeasureTheory.Measure.map (fun (ω : Ω) => (ν ω, fun (i : Fin m) => X (k i) ω)) μ) (S ×ˢ Set.univ.pi B) = (μ.bind fun (ω : Ω) => (MeasureTheory.Measure.dirac (ν ω)).prod ↑(MeasureTheory.ProbabilityMeasure.pi fun (x : Fin m) => ν ω)) (S ×ˢ Set.univ.pi B)

A ConditionallyIIDWith witness gives the joint disintegration on a product of an arbitrary set in the directing-measure coordinate and an arbitrary finite block rectangle.

theorem TauCeti.Probability.conditionallyIIDWith_iff_forall_jointRectangles {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {ι : Type u_3} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} : ConditionallyIIDWith μ X ν ↔ (∀ (i : ι), AEMeasurable (X i) μ) ∧ Measurable ν ∧ ∀ (m : ℕ) (k : Fin m → ι), Function.Injective k → ∀ (S : Set (MeasureTheory.ProbabilityMeasure α)), MeasurableSet S → ∀ (B : Fin m → Set α), (∀ (i : Fin m), MeasurableSet (B i)) → (MeasureTheory.Measure.map (fun (ω : Ω) => (ν ω, fun (i : Fin m) => X (k i) ω)) μ) (S ×ˢ Set.univ.pi B) = (μ.bind fun (ω : Ω) => (MeasureTheory.Measure.dirac (ν ω)).prod ↑(MeasureTheory.ProbabilityMeasure.pi fun (x : Fin m) => ν ω)) (S ×ˢ Set.univ.pi B)

Joint-rectangle factorization characterizes ConditionallyIIDWith for a finite base measure.

theorem TauCeti.Probability.conditionallyIID_iff_exists_forall_jointRectangles {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {ι : Type u_3} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → α} : ConditionallyIID μ X ↔ ∃ (ν : Ω → MeasureTheory.ProbabilityMeasure α), (∀ (i : ι), AEMeasurable (X i) μ) ∧ Measurable ν ∧ ∀ (m : ℕ) (k : Fin m → ι), Function.Injective k → ∀ (S : Set (MeasureTheory.ProbabilityMeasure α)), MeasurableSet S → ∀ (B : Fin m → Set α), (∀ (i : Fin m), MeasurableSet (B i)) → (MeasureTheory.Measure.map (fun (ω : Ω) => (ν ω, fun (i : Fin m) => X (k i) ω)) μ) (S ×ˢ Set.univ.pi B) = (μ.bind fun (ω : Ω) => (MeasureTheory.Measure.dirac (ν ω)).prod ↑(MeasureTheory.ProbabilityMeasure.pi fun (x : Fin m) => ν ω)) (S ×ˢ Set.univ.pi B)

Joint-rectangle factorization characterizes the existential predicate ConditionallyIID for a finite base measure.