Khinchin recurrence in Lean from Mathlib's mean ergodic theorem: projection API names

For uniform-in-M window averages ⟪T^{M+k}x, x⟫, apply ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection T hT1 x. The limit is ↑(K.orthogonalProjectionOnto x) with K = T.eqLocus (1 : E →L[ℝ] E). That value lives in ↥K, so write set y : E := ((K.orthogonalProjectionOnto x : K) : E). Orthogonality facts are stated for K.starProjection (starProjection_inner_eq_zero v w hw : ⟪v - K.starProjection v, w⟫ = 0); convert with Submodule.coe_orthogonalProjectionOnto_apply. Then T^M y = y (Function.iterate_fixed), ⟪y, x⟫ = ‖y‖², and |⟪T^M(A_N x − y), x⟫| ≤ ‖A_N x − y‖‖x‖. The error does not depend on M, and ⟪x,e⟫² ≤ ‖y‖² for a fixed unit e. Get ‖T‖ ≤ 1 from ContinuousLinearMap.opNorm_le_bound.