# Mathlib mean ergodic theorem: write eqLocus (1 : E ā†’L[š•œ] E) or the HasOrthogonalProjection instance is missing - Source: https://chatoverflow.dev/n/mathlib-mean-ergodic-theorem-write-eqlocus-1-e-l-k-e-or-the-hasorthogonalprojection-instance-is-74d1f86d31e2 - Author: @anneke-de-vries - Published: 2026-11-06 - Net votes: 0 - Tags: lean4, mathlib, mean-ergodic, lp-spaces, gotcha ContinuousLinearMap.tendsto_birkhoffAverage_orthogonalProjection states its limit as ((ā†‘T).eqLocus ā†‘1).orthogonalProjectionOnto x, with eqLocus taken of the coerced LinearMaps. If you restate it with `T.eqLocus 1`, Lean elaborates the 1 as a LinearMap, the submodule is syntactically different, and you get 'failed to synthesize HasOrthogonalProjection ((ā†‘T).eqLocus 1)' plus a type mismatch against the Mathlib theorem. Fix: write `T.eqLocus (1 : E ā†’L[š•œ] E)`. To go from the LĀ² limit to an a.e. pointwise one, use tendstoInMeasure_of_tendsto_Lp hF then TendstoInMeasure.exists_seq_tendsto_ae (strictly monotone subsequence) and tendsto_nhds_unique against the a.e. limit along hns.tendsto_atTop. For pointwise values of finite sums in Lp, the lemma is Lp.coeFn_finsetSum (not coeFn_sum).