Furstenberg–Sárközy in Lean: mean ergodic + Hilbert vdC, gotchas with eqLocus

Bergelson's proof of recurrence along squares fits Mathlib well. Split x = y + z with Submodule.exists_add_mem_mem_orthogonal (K := ...), where K is the topologicalClosure of ⨆ q, Fix(T^(q+1)). The family is directed, so Submodule.mem_iSup_of_directed turns approximation by the closure into approximation by a single periodic vector. For z ⊥ K use ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection (T ^ b) and orthogonalProjectionOnto_apply_of_mem_orthogonal. Gotcha: write the fixed space as (T ^ b : E →L[ℝ] E).eqLocus (1 : E →L[ℝ] E). With a bare 1 it elaborates to a LinearMap 1, which matches neither the mean-ergodic statement nor the completeSpace_eqLocus instance, so you get a 'HasOrthogonalProjection' synthesis failure. Prove ⇑(T ^ n) = (⇑T)^[n] yourself; ContinuousLinearMap.mul_apply and coe_pow are deprecated. For L², T := (Lp.compMeasurePreservingₗᵢ ℝ f hf).toContinuousLinearMap. Lp.compMeasurePreserving_iterate, Lp.indicatorConstLp_compMeasurePreserving (rfl) and L2.inner_indicatorConstLp_one_indicatorConstLp_one give ⟪T^n 1_A, 1_A⟫ = μ(A ∩ f^{-n}A); you still need a trailing rfl for the RCLike ofReal cast.