Coordinatewise maps of exchangeable processes

This file records that the Layer 0 symmetry notions for sequence laws are preserved by applying a measurable map to every coordinate of the process. It supplies the process-level closure API promised by the Exchangeability roadmap from the law-level lemmas map_blockLaw, map_prefixLaw, and map_pathLaw in Basic.lean.

These statements follow TauCetiRoadmap/Exchangeability/README.md, Layer 0, the item asking for closure of the symmetry classes under coordinatewise pushforward. The proofs use only Tau Ceti's existing finite-dimensional law API and Mathlib's Measure.map composition lemmas.

theorem TauCeti.Probability.ExchangeableAt.map_values {Ω : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {n : ℕ} (h : ExchangeableAt μ X n) {f : α → β} (hf : Measurable f) (hX : ∀ (i : Fin n), AEMeasurable (X ↑i) μ) : ExchangeableAt μ (fun (n : ℕ) (ω : Ω) => f (X n ω)) n

Finite exchangeability at a fixed length is preserved by a coordinatewise measurable map of the value space.

theorem TauCeti.Probability.Exchangeable.map_values {Ω : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : Exchangeable μ X) {f : α → β} (hf : Measurable f) (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) : Exchangeable μ fun (n : ℕ) (ω : Ω) => f (X n ω)

Finite exchangeability is preserved by a coordinatewise measurable map of the value space.

theorem TauCeti.Probability.FullyExchangeable.map_values {Ω : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : FullyExchangeable μ X) {f : α → β} (hf : Measurable f) (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) : FullyExchangeable μ fun (n : ℕ) (ω : Ω) => f (X n ω)

Full exchangeability is preserved by a coordinatewise measurable map of the value space.

theorem TauCeti.Probability.Contractable.map_values {Ω : Type u_1} {α : Type u_2} {β : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : Contractable μ X) {f : α → β} (hf : Measurable f) (hX : ∀ (i : ℕ), AEMeasurable (X i) μ) : Contractable μ fun (n : ℕ) (ω : Ω) => f (X n ω)

Contractability is preserved by a coordinatewise measurable map of the value space.