Orthogonal Projection Lemmas for de Finetti's Theorem

This file establishes key properties of orthogonal projections in Hilbert spaces that are used in the Koopman operator approach to de Finetti's theorem.

Mathematical background

In the ergodic approach to de Finetti, we use the Mean Ergodic Theorem to show that Birkhoff averages converge to a projection onto the fixed-point subspace of the Koopman operator. The key technical challenge is identifying this projection and showing uniqueness.

Orthogonal projection: For a closed subspace S of a Hilbert space E, the orthogonal projection P : E → S is the unique operator satisfying:

1. Range: P(E) = S
2. Idempotence: P² = P (projecting twice = projecting once)
3. Symmetry: P is self-adjoint: ⟨Px, y⟩ = ⟨x, Py⟩
4. Minimality: Px is the closest point in S to x

Main results

• orthogonalProjections_same_range_eq: Uniqueness - Two symmetric idempotent operators with the same range must be equal. This identifies projections from the Mean Ergodic Theorem.
• subtypeL_comp_orthogonalProjection_isSymmetric: The composition of subtype inclusion and orthogonal projection is symmetric.
• projection_eq_orthogonalProjection_of_properties: A symmetric idempotent operator with range S equals the orthogonal projection onto S.

Application to de Finetti

In the ergodic proof of de Finetti:

1. The Koopman operator U acts on L²(μ) by composition: (Uf)(ω) = f(shift ω)
2. The Mean Ergodic Theorem gives convergence to the fixed-point subspace: n⁻¹ ∑ᵢ Uⁱf → Pf where P projects onto {f : Uf = f}
3. These lemmas show P is the conditional expectation onto the tail σ-algebra
4. De Finetti's representation follows from this identification

References

• Kallenberg, "Probabilistic Symmetries and Invariance Principles" (2005), Chapter 1
• Krengel, "Ergodic Theorems" (1985), Chapter 1 (Mean Ergodic Theorem)

theorem orthogonalProjections_same_range_eq {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (P Q : E →L[𝕜] E) (S : Submodule 𝕜 E) [S.HasOrthogonalProjection] (hP_range : Set.range ⇑P = ↑S) (hQ_range : Set.range ⇑Q = ↑S) (_hP_fixes : ∀ g ∈ S, P g = g) (_hQ_fixes : ∀ g ∈ S, Q g = g) (hP_idem : P.comp P = P) (hQ_idem : Q.comp Q = Q) (hP_sym : (↑P).IsSymmetric) (hQ_sym : (↑Q).IsSymmetric) : P = Q

theorem subtypeL_comp_orthogonalProjection_isSymmetric {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (S : Submodule 𝕜 E) [S.HasOrthogonalProjection] : (↑(S.subtypeL.comp S.orthogonalProjection)).IsSymmetric

The composition of subtype inclusion and orthogonal projection is symmetric.

Statement: If S is a closed subspace with orthogonal projection, then the operator subtypeL ∘ orthogonalProjection : E → E (project onto S, then include back into E) is self-adjoint.

Intuition: This says that "project onto S and include back" is a symmetric operator on the ambient space. This is not obvious from the definition but follows from the orthogonality of the projection.

Why this matters: When we identify projections from the Mean Ergodic Theorem, we need to verify they are symmetric. This lemma provides that verification for projections constructed via orthogonal projection onto a subspace.