Coordinatewise maps of mixed i.i.d. families

This file completes the Layer 0 closure API for the exchangeability symmetry classes: applying a measurable map f : α → β to every coordinate of a mixed i.i.d. family gives another mixed i.i.d. family, whose mixing representative is the coordinatewise pushforward ω ↦ (ν ω).map f of the original mixing representative ν.

TauCeti.Probability.Exchangeability.Map already records this closure for ExchangeableAt, Exchangeable, FullyExchangeable, and Contractable. MixedIID is the remaining symmetry class from the roadmap item asking for closure of each class under the coordinatewise pushforward X ↦ (f ∘ Xᵢ) (TauCetiRoadmap/Exchangeability/README.md, Layer 0). The transformation of the mixing representative is the expected one: the mixture identity for the mapped family is the original identity with each product factor pushed forward by f.

map_values holds at an arbitrary index type; mixedIID_of_mixedIID_pathLaw below is genuinely sequence-level, since it transfers along the ℕ-indexed path law.

The proof runs at the level of the finite-block mixture identity. It reuses map_blockLaw (the coordinatewise pushforward of a block law), the random-product measurability of TauCeti.MeasureTheory.Measure.ProductKernel, the naturality of bind (TauCeti.MeasureTheory.map_bind), and Mathlib's product pushforward Measure.pi_map_pi. It needs no material from cameronfreer/exchangeability beyond the existing MixedIIDWith API this repository already carries.

theorem TauCeti.Probability.MixedIIDWith.map_values {Ω : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : MixedIIDWith μ X ν) {f : α → β} (hf : Measurable f) : MixedIIDWith μ (fun (i : ι) (ω : Ω) => f (X i ω)) fun (ω : Ω) => (ν ω).map f

Mixed i.i.d.-ness with a named mixing representative is preserved by a coordinatewise measurable map of the value space: if X is mixed i.i.d. with mixing representative ν, then fun i ω => f (X i ω) is mixed i.i.d. with mixing representative the coordinatewise pushforward fun ω => (ν ω).map f.

theorem TauCeti.Probability.MixedIID.map_values {Ω : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_4} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} (h : MixedIID μ X) {f : α → β} (hf : Measurable f) : MixedIID μ fun (i : ι) (ω : Ω) => f (X i ω)

Mixed i.i.d.-ness is preserved by a coordinatewise measurable map of the value space.

theorem TauCeti.Probability.mixedIID_of_mixedIID_pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX_meas : ∀ (n : ℕ), Measurable (X n)) (h : MixedIID (pathLaw μ X) fun (n : ℕ) (p : ℕ → α) => p n) : MixedIID μ X

Transfer of mixed i.i.d.-ness along the path law. If the coordinate process on path space is mixed i.i.d. under pathLaw μ X, then X is mixed i.i.d. under μ.