The full-path joint disintegration

ConditionallyIIDWith μ X ν constrains the joint law of (ν, block) along each finite selection of coordinates. This file upgrades that to the whole path at once: the joint law of the directing measure together with the entire process is the disintegration ∫ δ_{ν ω} ⊗ (ν ω)^{⊗ℕ} dμ(ω).

Main results

• TauCeti.Probability.ConditionallyIIDWith.jointPathLaw_eq_iidMixtureLaw
• TauCeti.Probability.ConditionallyIIDWith.jointPathLaw_eq_of_pathLaw_eq — the joint law depends on the process only through its path law.

Implementation

The right-hand side is not a new construction: iidMixtureLaw (μ.map ν) id is the canonical two-stage law of ConditionallyIID.Construct — draw a probability measure from the mixing law μ.map ν, then sample i.i.d. from it, keeping the drawn measure as a coordinate. So the theorem says the abstract conditional predicate is exactly realised by that generative construction, which is a stronger statement than naming a bespoke disintegration measure would be.

Both measures live on ProbabilityMeasure α × (ℕ → α), and the proof identifies them prefix by prefix. For the joint law that prefix marginal is the defining identity of ConditionallyIIDWith at the selection Fin n → ℕ, which is map_prefixProjPair_jointPathLaw_eq_disintegration. For the mixture law it is map_prefixProjPair_iidMixtureLaw — a general fact about iidMixtureLaw, and so kept with the construction in ConditionallyIID/Construct.lean — proved fibrewise: over each point t of the mixing law the fibre δ_t ⊗ (P t)^{⊗ℕ} projects to δ_t ⊗ (P t)^{⊗ Fin n}, which is map_infinitePi_pair_block at the prefix selection — the tag t and the sampled law P t differ there, which is why that lemma carries an arbitrary tag. Instantiating at the identity kernel and pushing the bind back along ν makes the two prefix marginals agree, and measure_eq_of_prefixProjPair_map_eq promotes the agreement to equality of the full measures.

That last step is where the paired prefix maps prefixProjPair earn their keep. Mathlib's IsProjectiveLimit is stated for pure dependent products ∀ i, α i, so it does not apply to a product with a fixed first factor; measure_eq_of_prefixProjPair_map_eq instead replicates the first factor at every coordinate to reduce to the honest path case.

References

• Roadmap: TauCetiRoadmap/Exchangeability/README.md, Layer 6 (directing measures) — the path-level form of the conditional disintegration the directing-measure layer is stated against.
• O. Kallenberg, Probabilistic Symmetries and Invariance Principles (Springer, 2005), §1.1, where the conditional predicate is stated blockwise.

The path-level form is what downstream work consumes — empirical measures as objects, the affine/barycenter representation, and ergodic decomposition all read the joint law of (ν, X) in one piece rather than block by block.

theorem TauCeti.Probability.ConditionallyIIDWith.map_prefixProjPair_jointPathLaw_eq_disintegration {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : ConditionallyIIDWith μ X ν) (n : ℕ) : MeasureTheory.Measure.map (prefixProjPair (MeasureTheory.ProbabilityMeasure α) α n) (jointPathLaw μ X ν) = μ.bind fun (ω : Ω) => (MeasureTheory.Measure.dirac (ν ω)).prod ↑(MeasureTheory.ProbabilityMeasure.pi fun (x : Fin n) => ν ω)

The prefix pushforward of the joint path law is the block-level disintegration, by the defining identity at the first n coordinates.

The full-path disintegration

theorem TauCeti.Probability.ConditionallyIIDWith.jointPathLaw_eq_iidMixtureLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} [MeasureTheory.IsFiniteMeasure μ] (h : ConditionallyIIDWith μ X ν) : jointPathLaw μ X ν = iidMixtureLaw (MeasureTheory.Measure.map ν μ) id

The full-path joint disintegration. For a conditionally i.i.d. process the joint law of the directing measure together with the whole path is the disintegration ∫ δ_{ν ω} ⊗ (ν ω)^{⊗ℕ} dμ(ω).

The definition of ConditionallyIIDWith gives this along each finite selection of coordinates; this upgrades it to the entire path at once.

theorem TauCeti.Probability.ConditionallyIIDWith.jointPathLaw_eq_of_pathLaw_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} {Ω' : Type u_3} [MeasurableSpace Ω'] [MeasureTheory.IsFiniteMeasure μ] {μ' : MeasureTheory.Measure Ω'} [MeasureTheory.IsFiniteMeasure μ'] {Y : ℕ → Ω' → α} {ν' : Ω' → MeasureTheory.ProbabilityMeasure α} (h : ConditionallyIIDWith μ X ν) (h' : ConditionallyIIDWith μ' Y ν') (hpath : pathLaw μ X = pathLaw μ' Y) : jointPathLaw μ X ν = jointPathLaw μ' Y ν'

The joint law of a directing measure and a path is a function of the path law. Two conditionally i.i.d. processes with the same path law — on possibly different sample spaces — have directing measures jointly distributed with the path in the same way.

This is the conditional-side companion of mixedIID_mixingLaw_eq_of_pathLaw_eq, and is strictly stronger than it: the mixing law is the first marginal of the joint law. It fails for a mere mixing representative, whose coupling with the path is not determined — an independent copy of a directing measure witnesses MixedIIDWith with a different joint law.

The proof is the full-path disintegration read twice: each joint law is the canonical two-stage law iidMixtureLaw of its mixing law, and equal path laws give equal mixing laws.