theorem standard_unit_vector_apply {I : Type u} [DecidableEq I] (i j : I) : ↑(lp.single 2 i 1) j = if j = i then 1 else 0

The standard unit vector is 1 at its defining index and 0 at every other coordinate.

theorem l2_inner_eq_tsum_mul {I : Type u} (ξ η : ↥(lp (fun (x : I) => ℝ) 2)) : inner ℝ ξ η = ∑' (j : I), ↑ξ j * ↑η j

In real ℓ²(I), the inner product is the sum of the pointwise products of the coordinates.