Contractability API

This file records basic lemmas for Contractable processes. The definitions live in TauCeti.Probability.Exchangeability.Basic.

The main result is Exchangeable.contractable: every exchangeable sequence with a.e. measurable coordinates is contractable. The file also provides Exchangeable.blockLaw_eq_prefixLaw_of_injective (the injective-selection analogue) and Contractable.measurePreserving_reindex / Contractable.measurePreserving_shift (a contractable path law is invariant under strictly monotone time-reindexing, in particular the shift), plus the converse characterization contractable_iff_forall_map_reindex_pathLaw.

These declarations are adapted from the cameronfreer/exchangeability Layer 0 sources pinned at e0532e59ceff23edab44dda9ab0655debbc9cc22, with Tau Ceti API names and hypotheses; the combinatorial core, StrictMono.exists_strictMono_nat_extending_fin, now lives in TauCeti.Data.Fin.StrictMono. Contractable.pairLaw_eq is adapted from DeFinetti/ViaMartingale/FutureRectangles.lean (contractable_dist_eq) in the same repo, reproved via the reindexing route below rather than the reference's rectangle π-system.

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

A contractable process has the same finite-dimensional block law as the corresponding prefix law along any strictly increasing finite index map.

theorem TauCeti.Probability.Contractable.map_single {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : Contractable μ X) (k : Fin 1 → ℕ) : blockLaw μ X k = prefixLaw μ X 1

The one-coordinate specialization of contractability.

theorem TauCeti.Probability.Contractable.map_pair {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : Contractable μ X) {i j : ℕ} (hij : i < j) : blockLaw μ X ![i, j] = prefixLaw μ X 2

The two-coordinate specialization of contractability.

theorem TauCeti.Probability.Contractable.identDistrib_block {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : Contractable μ X) {m : ℕ} {k l : Fin m → ℕ} (hk : StrictMono k) (hl : StrictMono l) (hk_meas : ∀ (r : Fin m), AEMeasurable (X (k r)) μ) (hl_meas : ∀ (r : Fin m), AEMeasurable (X (l r)) μ) : ProbabilityTheory.IdentDistrib (fun (ω : Ω) (r : Fin m) => X (k r) ω) (fun (ω : Ω) (r : Fin m) => X (l r) ω) μ μ

Finite blocks of a contractable process are identically distributed. For a contractable process X, any two strictly increasing finite coordinate selections have the same joint law.

theorem TauCeti.Probability.Contractable.identDistrib_coord {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : Contractable μ X) {i j : ℕ} (hi_meas : AEMeasurable (X i) μ) (hj_meas : AEMeasurable (X j) μ) : ProbabilityTheory.IdentDistrib (X i) (X j) μ μ

Coordinates of a contractable process are identically distributed. For a contractable process X, any two a.e. measurable coordinates X i and X j have the same law.

theorem TauCeti.Probability.Contractable.integrable_comp {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {E : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [BorelSpace E] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : Contractable μ X) (hX_ae : ∀ (n : ℕ), AEMeasurable (X n) μ) {f : α → E} (hf : Measurable f) {i : ℕ} (hf_int : MeasureTheory.Integrable (fun (ω : Ω) => f (X i ω)) μ) (j : ℕ) : MeasureTheory.Integrable (fun (ω : Ω) => f (X j ω)) μ

Integrability of an observable is a coordinate-free property. For a contractable process, integrability of f ∘ X i for one coordinate i gives it for every coordinate j.

theorem TauCeti.Probability.Contractable.memLp_comp {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {E : Type u_3} [MeasurableSpace E] [NormedAddCommGroup E] [BorelSpace E] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : Contractable μ X) (hX_ae : ∀ (n : ℕ), AEMeasurable (X n) μ) {f : α → E} (hf : Measurable f) {p : ENNReal} {i : ℕ} (hf_Lp : MeasureTheory.MemLp (fun (ω : Ω) => f (X i ω)) p μ) (j : ℕ) : MeasureTheory.MemLp (fun (ω : Ω) => f (X j ω)) p μ

Membership in L^p is a coordinate-free property of an observable. For a contractable process, MemLp (f ∘ X i) p for one coordinate i gives it for every coordinate j.

theorem TauCeti.Probability.Contractable.identDistrib_pair {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : Contractable μ X) {i j k l : ℕ} (hi_meas : AEMeasurable (X i) μ) (hj_meas : AEMeasurable (X j) μ) (hk_meas : AEMeasurable (X k) μ) (hl_meas : AEMeasurable (X l) μ) (hij : i < j) (hkl : k < l) : ProbabilityTheory.IdentDistrib (fun (ω : Ω) => (X i ω, X j ω)) (fun (ω : Ω) => (X k ω, X l ω)) μ μ

Increasing pairs of a contractable process are identically distributed. For a contractable process X, if the four selected coordinates are a.e. measurable and i < j, k < l, then (X i, X j) has the same joint law as (X k, X l).

theorem TauCeti.Probability.Contractable.comp {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (h : Contractable μ X) {φ : ℕ → ℕ} (hφ : StrictMono φ) : Contractable μ fun (n : ℕ) (ω : Ω) => X (φ n) ω

Contractability is preserved by passing to a strictly increasing subsequence.

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

An exchangeable sequence has the prefix law along any injective finite selection: blockLaw μ X k = prefixLaw μ X n for injective k : Fin n → ℕ.

theorem TauCeti.Probability.Exchangeable.contractable {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} (hX : Exchangeable μ X) (hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) : Contractable μ X

Every exchangeable sequence with a.e. measurable coordinates is contractable: along any strictly increasing finite selection k, blockLaw μ X k = prefixLaw μ X m. One direction of the de Finetti–Ryll-Nardzewski equivalence.

theorem TauCeti.Probability.Contractable.measurePreserving_reindex {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} [MeasureTheory.IsFiniteMeasure μ] (hX : Contractable μ X) (hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) {φ : ℕ → ℕ} (hφ : StrictMono φ) : MeasureTheory.MeasurePreserving (fun (x : ℕ → α) (k : ℕ) => x (φ k)) (pathLaw μ X) (pathLaw μ X)

A contractable process's path law is invariant under strictly monotone time-reindexing: for StrictMono φ, the reindexing x ↦ x ∘ φ preserves pathLaw μ X.

theorem TauCeti.Probability.contractable_iff_forall_map_reindex_pathLaw {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} [MeasureTheory.IsFiniteMeasure μ] (hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) : Contractable μ X ↔ ∀ (φ : ℕ → ℕ), StrictMono φ → MeasureTheory.Measure.map (fun (x : ℕ → α) (k : ℕ) => x (φ k)) (pathLaw μ X) = pathLaw μ X

Contractability is equivalent to invariance of the path law under every strictly increasing time-reindexing ℕ → ℕ. This is the path-law form of spreadability/contractability.

theorem TauCeti.Probability.contractable_iff_forall_measurePreserving_reindex {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} [MeasureTheory.IsFiniteMeasure μ] (hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) : Contractable μ X ↔ ∀ (φ : ℕ → ℕ), StrictMono φ → MeasureTheory.MeasurePreserving (fun (x : ℕ → α) (k : ℕ) => x (φ k)) (pathLaw μ X) (pathLaw μ X)

Contractability is equivalent to preservation of the path law by every strictly increasing time-reindexing ℕ → ℕ.

theorem TauCeti.Probability.Contractable.map_reindex_pathLaw_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} [MeasureTheory.IsFiniteMeasure μ] (hX : Contractable μ X) (hX_ae : ∀ (i : ℕ), AEMeasurable (X i) μ) {φ : ℕ → ℕ} (hφ : StrictMono φ) : MeasureTheory.Measure.map (fun (ω : Ω) (i : ℕ) => X (φ i) ω) μ = pathLaw μ X

A strictly monotone reindexing leaves the path law alone. Reading a contractable process along φ gives the same path law as reading it along the identity.

theorem TauCeti.Probability.Contractable.measurePreserving_shift {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → α} [MeasureTheory.IsFiniteMeasure μ] (hX : Contractable μ X) (hX_meas : ∀ (i : ℕ), AEMeasurable (X i) μ) : MeasureTheory.MeasurePreserving (shift α) (pathLaw μ X) (pathLaw μ X)

A contractable process has a shift-invariant path law: shift preserves pathLaw μ X.

theorem TauCeti.Probability.Contractable.pairLaw_eq {Ω : Type u_1} {α : Type u_2} [MeasurableSpace Ω] [MeasurableSpace α] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α} (hX : Contractable μ X) (hX_ae : ∀ (n : ℕ), AEMeasurable (X n) μ) {g : ℕ → ℕ} (hg : StrictMono g) {j k : ℕ} (hj : j < g 0) (hk : k < g 0) : MeasureTheory.Measure.map (fun (ω : Ω) => (X j ω, fun (n : ℕ) => X (g n) ω)) μ = MeasureTheory.Measure.map (fun (ω : Ω) => (X k ω, fun (n : ℕ) => X (g n) ω)) μ

Pair-law equality from contractability. For a contractable process, a strictly increasing tail selection g, and two head indices j, k below the tail start g 0, the joint law of the head coordinate X j with the tail (X (g 0), X (g 1), …) equals the joint law of X k with the same tail:

μ.map (fun ω ↦ (X j ω, fun n ↦ X (g n) ω)) = μ.map (fun ω ↦ (X k ω, fun n ↦ X (g n) ω)).