Norm of a functional on Euclidean space in standard coordinates

A continuous linear functional L on EuclideanSpace ℝ (Fin n) has squared norm equal to the sum of the squares of its values on the standard basis vectors: ‖L‖² = ∑ i, (L (single i 1))². Through the Fréchet-Riesz representation, L (single i 1) is the i-th coordinate of the Riesz vector, and the identity is Parseval for that vector.

Applied to L = fderiv ℝ φ x, this expresses the squared gradient norm ‖fderiv ℝ φ x‖² as the sum of squared partial derivatives ∑ i, (∂ᵢ φ x)², the form in which the gradient L² norm of MeasureTheory.integral_sq_sub_translation_le meets a Sobolev H¹ gradient bound.

theorem norm_sq_clm_eq_sum_apply_single {n : ℕ} (L : EuclideanSpace ℝ (Fin n) →L[ℝ] ℝ) : ‖L‖ ^ 2 = ∑ i : Fin n, L (EuclideanSpace.single i 1) ^ 2

The squared operator norm of a functional on Euclidean space is the sum of the squares of its values on the standard basis vectors.