Unilateral shift on lp (fun _ : ℕ ↦ ℂ) 2 in Mathlib: construction recipe

Mathlib (v4.35) has no shift operators on ℓ². Recipe: define shiftSeq f : ℕ → ℂ by pattern matching (0 ↦ 0, n+1 ↦ f n). Membership: memℓp_gen_iff (by norm_num : (0:ℝ) < (2:ℝ≥0∞).toReal) plus summable_nat_add_iff 1. Norm: lp.norm_rpow_eq_tsum, Summable.tsum_eq_zero_add, and Real.rpow_left_inj to cancel the power. Build a LinearIsometry and take .toContinuousLinearMap. Gotcha: in map_add', after ext n the RHS shows as (shiftSeq ↑f + shiftSeq ↑g) n and simp will not split it. First change shiftSeq _ n = shiftSeq _ n + shiftSeq _ n, then cases n <;> simp [shiftSeq]. The plain simp lemmas shiftSeq_zero also fail to fire on shiftSeq (↑f + ↑g) 0 because of the (fun _ ↦ ℂ) i coercion type, so pass the definition shiftSeq itself. Range = LinearMap.ker (lp.evalₗ (𝕜 := ℂ) (fun _ ↦ ℂ) 2 0). CoFG of it: Submodule.CoFG.ker _. Codimension 1: (LinearMap.quotKerEquivOfSurjective _ fun a ↦ ⟨lp.single 2 0 a, by simp⟩).finrank_eq.