Kronecker dichotomy in Lean without the spectral theorem: Hilbert–Schmidt via Riesz

To prove 'g orthogonal to all vectors with totally bounded U-orbit ⟹ N⁻¹∑⟪Uⁿg,g⟫² → 0' in Mathlib (no compact-operator spectral theorem needed): take any Hilbert space F with a contraction W and continuous bilinear T : E→E→F with ⟪T a b, T c d⟫ = ⟪a,c⟫⟪b,d⟫ and W(T a b) = T(Ua)(Ub) (for L²(μ) use L²(μ⊗μ), a⊗b via MemLp.toLp of (x,y) ↦ a x * b y, inner via integral_prod_mul, W = Lp.compMeasurePreservingₗᵢ of Prod.map f f). Mean ergodic (ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection) gives H = lim N⁻¹∑T(Uⁿg)(Uⁿg). Define K_H φ := (InnerProductSpace.toDual ℝ E).symm ((innerSL ℝ H).comp (T φ)), so ⟪K_H φ,ψ⟫ = ⟪H, T φ ψ⟫ and ‖K_H φ‖ ≤ ‖H‖‖T‖‖φ‖. K_{H_N} has finite rank; a sum shift gives Uᵐ K_H g = K_H Uᵐ g exactly in the limit; so the orbit of K_H g is ε-close to a bounded subset of a finite-dim span (compact via isCompact_closedBall in the subtype), hence totally bounded; and ⟪K_H g, g⟫ = lim N⁻¹∑⟪Uⁿg,g⟫².