The covariance structure of a contractable L² sequence

This file opens the Layer 3 (L²) lane of the Exchangeability roadmap (TauCetiRoadmap/Exchangeability/README.md, "Layer 3: L² averaging library and the standard-Borel de Finetti route"), whose first analytic input is the uniform covariance structure of a contractable L² sequence (contractable_covariance_structure). It also supplies the two Layer 3 preliminaries listed before it — "equality of means and integrals from equal one-dimensional laws" and "equality of pair covariances from equal two-dimensional laws".

For a real-valued contractable sequence, the one- and two-coordinate IdentDistrib facts in TauCeti.Probability.Exchangeability.Contractability give the uniform first- and second-moment structure:

• Contractable.integral_coord_eq: all coordinate means agree;
• Contractable.variance_coord_eq: all coordinate variances agree;
• Contractable.covariance_eq_of_ne: any two off-diagonal covariances agree, cov[X i, X j; μ] = cov[X k, X l; μ] for i ≠ j and k ≠ l.

The IdentDistrib and moment machinery is Mathlib's (ProbabilityTheory.IdentDistrib, ProbabilityTheory.covariance, ProbabilityTheory.variance); the contractability input is the Layer 0 API in TauCeti.Probability.Exchangeability.Contractability. No material from cameronfreer/exchangeability is used: the source's L² lane carries the real-valued statement through block averages, whereas this file records only the elementary moment-uniformity that seeds it.

theorem TauCeti.Probability.Contractable.integral_coord_eq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {γ : Type u_2} [MeasurableSpace γ] [NormedAddCommGroup γ] [NormedSpace ℝ γ] [BorelSpace γ] {Z : ℕ → Ω → γ} (hZ : Contractable μ Z) {i j : ℕ} (hi_meas : AEMeasurable (Z i) μ) (hj_meas : AEMeasurable (Z j) μ) : ∫ (x : Ω), Z i x ∂μ = ∫ (x : Ω), Z j x ∂μ

Equal means from contractability. For a contractable process with values in a normed real vector space, all coordinate expectations agree.

theorem TauCeti.Probability.Contractable.variance_coord_eq {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → ℝ} (hX : Contractable μ X) {i j : ℕ} (hi_meas : AEMeasurable (X i) μ) (hj_meas : AEMeasurable (X j) μ) : ProbabilityTheory.variance (X i) μ = ProbabilityTheory.variance (X j) μ

Equal variances from contractability. For a contractable real-valued process, all coordinate variances agree.

theorem TauCeti.Probability.Contractable.covariance_eq_of_lt {Ω : Type u_1} [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.covariance (X i) (X j) μ = ProbabilityTheory.covariance (X k) (X l) μ

Uniform covariances from contractability. For a contractable real-valued process with a.e. measurable coordinates, any two off-diagonal covariances agree: cov[X i, X j; μ] = cov[X k, X l; μ] whenever i < j and k < l.

theorem TauCeti.Probability.Contractable.covariance_eq_of_ne {Ω : Type u_1} [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.covariance (X i) (X j) μ = ProbabilityTheory.covariance (X k) (X l) μ

Uniform off-diagonal covariances from contractability. For a contractable real-valued process with a.e. measurable coordinates, any two off-diagonal covariances agree: cov[X i, X j; μ] = cov[X k, X l; μ] whenever i ≠ j and k ≠ l.

theorem TauCeti.Probability.contractable_covariance_structure {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : ℕ → Ω → ℝ} (hX : Contractable μ X) (hX_L2 : ∀ (n : ℕ), MeasureTheory.MemLp (X n) 2 μ) : (∀ (i j : ℕ), ∫ (x : Ω), X i x ∂μ = ∫ (x : Ω), X j x ∂μ) ∧ (∀ (i j : ℕ), ProbabilityTheory.variance (X i) μ = ProbabilityTheory.variance (X j) μ) ∧ ∀ (i j k l : ℕ), i ≠ j → k ≠ l → ProbabilityTheory.covariance (X i) (X j) μ = ProbabilityTheory.covariance (X k) (X l) μ

The uniform covariance structure of a contractable L² sequence. A contractable real-valued process with L² coordinates has constant coordinate means and variances, and a single common off-diagonal covariance: any two unequal-index pairs have equal covariance. This is the seed of the Layer 3 L² route to de Finetti.