The canonical conditionally i.i.d. process

Every measurable family of probability measures is realized as a directing measure. Given a probability measure π on a parameter space T and a measurable family P : T → ProbabilityMeasure α, the law

iidMixtureLaw π P = ∫ δ_t ⊗ (P t)^{⊗ℕ} dπ(t)

on T × (ℕ → α) is the two-stage experiment "draw the parameter t from π, then sample the coordinates i.i.d. from P t", with the parameter retained as the first coordinate. Its coordinate process X n ω = ω.2 n is conditionally i.i.d. with directing measure ω ↦ P ω.1, and the law of that directing measure is the prescribed π.map P.

This is the converse direction of the Layer 6 uniqueness statements: mixedIID_mixingLaw_unique and conditionallyIID_ae_unique say a directing measure is pinned down by the process, and the theorems here say every law on ProbabilityMeasure α of the form π.map P does arise. Before this file the only ConditionallyIIDWith witnesses available were the constant one (ConditionallyIIDWith.of_iIndepFun_identDistrib, i.e. plain i.i.d.) and the one the hard de Finetti theorem extracts from contractability; nothing produced a prescribed nondegenerate directing measure.

Note that the conclusion is the sharp conditional predicate, not merely the mixture identity: the generating construction ties the process to ν and not just to its law, which is exactly the difference the roadmap insists on (TauCetiRoadmap/Exchangeability/README.md, "Standing hypotheses").

Main results

• iidMixtureLaw — the canonical two-stage law, with isProbabilityMeasure_iidMixtureLaw and the marginal iidMixtureLaw_map_fst.
• conditionallyIIDWith_iidMixtureLaw — the coordinate process is conditionally i.i.d. with directing measure ω ↦ P ω.1, and the corollaries mixedIIDWith_iidMixtureLaw, exchangeable_iidMixtureLaw, contractable_iidMixtureLaw.
• iidMixtureLaw_map_directing — the directing measure has the prescribed law π.map P, and pathLaw_iidMixtureLaw reads the path law as the π.map P-mixture of infinite powers.
• map_prod_infinitePi_eq_iidMixtureLaw — the canonical law is realized by a parameter and independent i.i.d. noise pushed through a family of maps carrying the noise law to P t.
• exists_map_eq_dirac_of_iIndepFun_iidMixtureLaw — the construction is genuinely richer than i.i.d.: independent coordinates force the mixing law π.map P to be a point mass.

This advances TauCetiRoadmap/Exchangeability/README.md, Layer 6 (directing measures), and supplies the construction the roadmap's coin-flipping worked example instantiates (TauCeti/Probability/Exchangeability/ConditionallyIID/CoinFlips.lean). It needs no material from cameronfreer/exchangeability, whose ConditionallyIID names the weaker mixture identity.

noncomputable def TauCeti.Probability.iidMixtureLaw {T : Type u_1} {α : Type u_2} [MeasurableSpace T] [MeasurableSpace α] (π : MeasureTheory.Measure T) (P : T → MeasureTheory.ProbabilityMeasure α) : MeasureTheory.Measure (T × (ℕ → α))

The canonical conditionally i.i.d. law. Draw a parameter t from π, then sample the coordinates i.i.d. from P t, keeping t as the first coordinate of the sample space T × (ℕ → α).

Retaining the parameter is what makes this a conditional construction rather than only a mixture of i.i.d. laws: the sequence and its directing measure live on the same space, so the joint law of the two can be compared with the disintegration ConditionallyIIDWith demands.

Equations

• TauCeti.Probability.iidMixtureLaw π P = π.bind fun (t : T) => (MeasureTheory.Measure.dirac t).prod (MeasureTheory.Measure.infinitePi fun (x : ℕ) => ↑(P t))

@[simp]

theorem TauCeti.Probability.iidMixtureLaw_def {T : Type u_1} {α : Type u_2} [MeasurableSpace T] [MeasurableSpace α] (π : MeasureTheory.Measure T) (P : T → MeasureTheory.ProbabilityMeasure α) : iidMixtureLaw π P = π.bind fun (t : T) => (MeasureTheory.Measure.dirac t).prod (MeasureTheory.Measure.infinitePi fun (x : ℕ) => ↑(P t))

The canonical law unfolded as the π-mixture of the parameter-tagged countable powers.

theorem TauCeti.Probability.isProbabilityMeasure_iidMixtureLaw {T : Type u_1} {α : Type u_2} [MeasurableSpace T] [MeasurableSpace α] {π : MeasureTheory.Measure T} {P : T → MeasureTheory.ProbabilityMeasure α} [MeasureTheory.IsProbabilityMeasure π] (hP : Measurable P) : MeasureTheory.IsProbabilityMeasure (iidMixtureLaw π P)

The canonical law is a probability measure. Measurability of P is needed, not decorative: Measure.bind against a non-measurable kernel is the zero measure.

theorem TauCeti.Probability.iidMixtureLaw_map_fst {T : Type u_1} {α : Type u_2} [MeasurableSpace T] [MeasurableSpace α] {π : MeasureTheory.Measure T} {P : T → MeasureTheory.ProbabilityMeasure α} (hP : Measurable P) : MeasureTheory.Measure.map Prod.fst (iidMixtureLaw π P) = π

The parameter coordinate of the canonical law is distributed as π.

theorem TauCeti.Probability.iidMixtureLaw_map_directing {T : Type u_1} {α : Type u_2} [MeasurableSpace T] [MeasurableSpace α] {π : MeasureTheory.Measure T} {P : T → MeasureTheory.ProbabilityMeasure α} (hP : Measurable P) : MeasureTheory.Measure.map (fun (ω : T × (ℕ → α)) => P ω.1) (iidMixtureLaw π P) = MeasureTheory.Measure.map P π

The directing measure of the canonical law has the prescribed mixing law π.map P.

theorem TauCeti.Probability.map_prod_infinitePi_eq_iidMixtureLaw {T : Type u_1} {α : Type u_2} [MeasurableSpace T] [MeasurableSpace α] {π : MeasureTheory.Measure T} {P : T → MeasureTheory.ProbabilityMeasure α} {R : Type u_3} [MeasurableSpace R] (ρ : MeasureTheory.Measure R) [MeasureTheory.IsProbabilityMeasure ρ] {h : T → R → α} (hh : Measurable (Function.uncurry h)) (hP : ∀ (t : T), MeasureTheory.Measure.map (h t) ρ = ↑(P t)) : MeasureTheory.Measure.map (fun (q : T × (ℕ → R)) => (q.1, fun (i : ℕ) => h q.1 (q.2 i))) (π.prod (MeasureTheory.Measure.infinitePi fun (x : ℕ) => ρ)) = iidMixtureLaw π P

The canonical law from a parameter and i.i.d. noise. Draw a parameter t from π and an independent i.i.d. sequence r from ρ, and apply a jointly measurable h t to each noise variable. If h t pushes ρ forward to P t, the resulting pair (t, (h t (r i))ᵢ) has the canonical law iidMixtureLaw π P: given the parameter, the coordinates are i.i.d. P t.

theorem TauCeti.Probability.conditionallyIIDWith_iidMixtureLaw {T : Type u_1} {α : Type u_2} [MeasurableSpace T] [MeasurableSpace α] {π : MeasureTheory.Measure T} {P : T → MeasureTheory.ProbabilityMeasure α} (hP : Measurable P) : ConditionallyIIDWith (iidMixtureLaw π P) (fun (n : ℕ) (ω : T × (ℕ → α)) => ω.2 n) fun (ω : T × (ℕ → α)) => P ω.1

The canonical process is conditionally i.i.d. For a measurable family P, the coordinate process of iidMixtureLaw π P is conditionally i.i.d. with directing measure ω ↦ P ω.1: along every finite selection of distinct coordinates, the joint law of the directing measure and the selected block is the disintegration ∫ δ_{P ω.1} ⊗ (P ω.1)^{⊗ Fin m}.

This is the sharp conditional conclusion — the directing measure is pinned to the process, not merely to the block laws — which is what makes iidMixtureLaw a realization of P as a directing measure rather than only as a mixing representative.

theorem TauCeti.Probability.conditionallyIID_iidMixtureLaw {T : Type u_1} {α : Type u_2} [MeasurableSpace T] [MeasurableSpace α] {π : MeasureTheory.Measure T} {P : T → MeasureTheory.ProbabilityMeasure α} (hP : Measurable P) : ConditionallyIID (iidMixtureLaw π P) fun (n : ℕ) (ω : T × (ℕ → α)) => ω.2 n

The canonical process is conditionally i.i.d. (existential form).

theorem TauCeti.Probability.mixedIIDWith_iidMixtureLaw {T : Type u_1} {α : Type u_2} [MeasurableSpace T] [MeasurableSpace α] {π : MeasureTheory.Measure T} {P : T → MeasureTheory.ProbabilityMeasure α} (hP : Measurable P) : MixedIIDWith (iidMixtureLaw π P) (fun (n : ℕ) (ω : T × (ℕ → α)) => ω.2 n) fun (ω : T × (ℕ → α)) => P ω.1

The prescribed family is in particular a mixing representative of the canonical process.

theorem TauCeti.Probability.exchangeable_iidMixtureLaw {T : Type u_1} {α : Type u_2} [MeasurableSpace T] [MeasurableSpace α] {π : MeasureTheory.Measure T} {P : T → MeasureTheory.ProbabilityMeasure α} (hP : Measurable P) : Exchangeable (iidMixtureLaw π P) fun (n : ℕ) (ω : T × (ℕ → α)) => ω.2 n

The canonical process is exchangeable.

theorem TauCeti.Probability.contractable_iidMixtureLaw {T : Type u_1} {α : Type u_2} [MeasurableSpace T] [MeasurableSpace α] {π : MeasureTheory.Measure T} {P : T → MeasureTheory.ProbabilityMeasure α} (hP : Measurable P) : Contractable (iidMixtureLaw π P) fun (n : ℕ) (ω : T × (ℕ → α)) => ω.2 n

The canonical process is contractable.

theorem TauCeti.Probability.pathLaw_iidMixtureLaw {T : Type u_1} {α : Type u_2} [MeasurableSpace T] [MeasurableSpace α] {π : MeasureTheory.Measure T} {P : T → MeasureTheory.ProbabilityMeasure α} [MeasureTheory.IsProbabilityMeasure π] (hP : Measurable P) : (pathLaw (iidMixtureLaw π P) fun (n : ℕ) (ω : T × (ℕ → α)) => ω.2 n) = (MeasureTheory.Measure.map P π).bind fun (Q : MeasureTheory.ProbabilityMeasure α) => MeasureTheory.Measure.infinitePi fun (x : ℕ) => ↑Q

The path law of the canonical process is the π.map P-mixture of infinite product measures — the de Finetti mixture representation, here with the mixing law prescribed in advance.

theorem TauCeti.Probability.exists_map_eq_dirac_of_iIndepFun_iidMixtureLaw {T : Type u_1} {α : Type u_2} [MeasurableSpace T] [MeasurableSpace α] {π : MeasureTheory.Measure T} {P : T → MeasureTheory.ProbabilityMeasure α} [MeasureTheory.IsProbabilityMeasure π] (hP : Measurable P) (h : ProbabilityTheory.iIndepFun (fun (n : ℕ) (ω : T × (ℕ → α)) => ω.2 n) (iidMixtureLaw π P)) : ∃ (Q : MeasureTheory.ProbabilityMeasure α), MeasureTheory.Measure.map P π = MeasureTheory.Measure.dirac Q

The construction is genuinely richer than i.i.d. If the canonical process happens to have independent coordinates, then its mixing law π.map P is a point mass — so a nondegenerate π.map P produces an exchangeable sequence that is not independent, and the directing measure the construction supplies is genuinely random rather than an a.e. constant.

theorem TauCeti.Probability.map_prefixProjPair_iidMixtureLaw {α : Type u_2} [MeasurableSpace α] {T : Type u_3} [MeasurableSpace T] {π : MeasureTheory.Measure T} {P : T → MeasureTheory.ProbabilityMeasure α} (hP : Measurable P) (n : ℕ) : MeasureTheory.Measure.map (prefixProjPair T α n) (iidMixtureLaw π P) = π.bind fun (t : T) => (MeasureTheory.Measure.dirac t).prod ↑(MeasureTheory.ProbabilityMeasure.pi fun (x : Fin n) => P t)

The prefix pushforward of the canonical mixture law. Projecting δ_t ⊗ (P t)^{⊗ℕ} onto the first n path coordinates leaves δ_t ⊗ (P t)^{⊗ Fin n}, fibre by fibre over the mixing law.