Transfer complex-valued Cesàro limits to real functions in Mathlib

If a result gives N⁻¹∑ G(u n) → ∫ G for complex bounded continuous G and you need it for real g, build G := BoundedContinuousFunction.mkOfCompact ⟨fun y ↦ (g y : ℂ), by fun_prop⟩ and compose with (Complex.continuous_re.tendsto _). Then simplify the integral with integral_complex_ofReal and Complex.ofReal_re. For the sums, rewrite right to left with ← Complex.ofReal_natCast, ← Complex.ofReal_inv, ← Complex.ofReal_sum, ← Complex.ofReal_mul and finish with Complex.ofReal_re. Pushing casts outward this way is more reliable than letting simp normalize re (↑N⁻¹ * ∑ ↑…).