Basic implications from mixed i.i.d.-ness

This file records the first implication out of the Layer 0 mixed-i.i.d. API: mixed i.i.d. processes are exchangeable. The definition MixedIIDWith μ X ν already states that every injective finite coordinate selection has the same product-mixture law, so the exchangeability proof is just the specialization to the permuted and identity selections of Fin n.

The resulting exchangeability theorem is one of the Layer 0 bridges listed in TauCetiRoadmap/Exchangeability/Suggested.lean; the contractability corollaries use the same injective-block identity, since strictly increasing finite selections are injective.

These declarations follow the cameronfreer/exchangeability Layer 0 implication lattice pinned at e0532e59ceff23edab44dda9ab0655debbc9cc22, but use Tau Ceti's current MixedIIDWith API, where the finite-block mixture identity is already stated for arbitrary injective selections.

theorem TauCeti.Probability.MixedIIDWith.prefixLaw_eq_mixture {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : MixedIIDWith μ X ν) (n : ℕ) : prefixLaw μ X n = μ.bind fun (ω : Ω) => ↑(MeasureTheory.ProbabilityMeasure.pi fun (x : Fin n) => ν ω)

Under a named mixing representative, the prefix law has the common finite-product mixture law.

theorem TauCeti.Probability.MixedIIDWith.blockLaw_eq_prefixLaw_of_injective {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : MixedIIDWith μ X ν) {m : ℕ} {k : Fin m → ℕ} (hk : Function.Injective k) : blockLaw μ X k = prefixLaw μ X m

Under a named mixing representative, every injective finite block has the same law as the corresponding prefix.

theorem TauCeti.Probability.MixedIID.blockLaw_eq_prefixLaw_of_injective {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : MixedIID μ X) {m : ℕ} {k : Fin m → ℕ} (hk : Function.Injective k) : blockLaw μ X k = prefixLaw μ X m

A mixed i.i.d. process has the same law along every injective finite block as along the corresponding prefix.

theorem TauCeti.Probability.MixedIIDWith.exchangeableAt {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : MixedIIDWith μ X ν) (n : ℕ) : ExchangeableAt μ X n

A named mixing representative makes the law of each finite prefix invariant under permutations of that prefix.

theorem TauCeti.Probability.MixedIIDWith.exchangeable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : MixedIIDWith μ X ν) : Exchangeable μ X

A process with a named mixing representative is exchangeable.

theorem TauCeti.Probability.MixedIID.exchangeable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : MixedIID μ X) : Exchangeable μ X

A mixed i.i.d. process is exchangeable. This is the Layer 0 bridge from the mixed-i.i.d. API to finite exchangeability (the roadmap's exchangeable_of_mixedIID).

theorem TauCeti.Probability.MixedIIDWith.contractable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {ν : Ω → MeasureTheory.ProbabilityMeasure α} (h : MixedIIDWith μ X ν) : Contractable μ X

A process with a named mixing representative is contractable: strictly increasing finite selections are injective finite selections.

theorem TauCeti.Probability.MixedIID.contractable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : MixedIID μ X) : Contractable μ X

A mixed i.i.d. process is contractable: strictly increasing finite selections are injective finite selections.