Monotonicity of finite exchangeability

This file records the implication-lattice API for ExchangeableAt: if the first n coordinates have permutation-invariant law, then so do the first m coordinates for every m ≤ n. The proof is the finite-dimensional marginal argument: extend a permutation of Fin m to one of Fin n, use exchangeability at n, and project the n-prefix law back to the first m coordinates.

The permutation-extension step reuses Mathlib's Equiv.Perm.exists_extending_pair; the measure-level projection step reuses Tau Ceti's map_blockLaw_reindex and map_prefixLaw_castLE.

This projection argument is adapted from Tau Ceti's credited Exchangeable.blockLaw_eq_prefixLaw_of_injective proof in Contractability.lean, following the cameronfreer/exchangeability sources.

theorem TauCeti.Probability.ExchangeableAt.blockLaw_eq_prefixLaw_of_injective {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {m n : ℕ} (h : ExchangeableAt μ X n) (k : Fin m → Fin n) (hk : Function.Injective k) (hX : ∀ (i : Fin n), AEMeasurable (X ↑i) μ) : (blockLaw μ X fun (i : Fin m) => ↑(k i)) = prefixLaw μ X m

An exchangeable n-prefix has the prefix law on every injective m-subselection inside that prefix.

theorem TauCeti.Probability.ExchangeableAt.of_le {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {m n : ℕ} (h : ExchangeableAt μ X n) (hmn : m ≤ n) (hX : ∀ (i : Fin n), AEMeasurable (X ↑i) μ) : ExchangeableAt μ X m

Finite exchangeability at length n descends to every shorter prefix length m ≤ n.

theorem TauCeti.Probability.ExchangeableAt.pred {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} {n : ℕ} (h : ExchangeableAt μ X (n + 1)) (hX : ∀ (i : Fin (n + 1)), AEMeasurable (X ↑i) μ) : ExchangeableAt μ X n

Exchangeability at n + 1 descends to exchangeability at n.