Comparing the sup norm with the Euclidean quantity on Fin m → ℝ

Mathlib equips the product type Fin m → ℝ with the sup norm (‖x‖ = ⨆ i, |x i|, realized as a finite maximum here), not the Euclidean (ℓ²) norm. Whenever a field that is Lipschitz or bounded in this sup norm feeds into an estimate phrased in Euclidean terms, the two norms have to be compared explicitly. This file collects the elementary inequalities that make that comparison, in either direction and with the intermediate ℓ¹ quantity, as used around lem:aniso:comparison.

theorem CIV.sq_norm_le_sum_sq {m : ℕ} (x : Fin m → ℝ) : ‖x‖ ^ 2 ≤ ∑ i : Fin m, x i ^ 2

The squared sup norm is bounded by the sum of squares of the coordinates: ‖x‖² ≤ ∑ᵢ xᵢ².

theorem CIV.sum_sq_le_card_mul_sq_norm {m : ℕ} (x : Fin m → ℝ) : ∑ i : Fin m, x i ^ 2 ≤ ↑m * ‖x‖ ^ 2

The sum of squares of the coordinates is bounded by m times the squared sup norm: ∑ᵢ xᵢ² ≤ m · ‖x‖².

theorem CIV.norm_le_sqrt_sum_sq {m : ℕ} (x : Fin m → ℝ) : ‖x‖ ≤ √(∑ i : Fin m, x i ^ 2)

The sup norm is bounded by the Euclidean norm: ‖x‖ ≤ √(∑ᵢ xᵢ²).

theorem CIV.sqrt_sum_sq_le_sqrt_card_mul_norm {m : ℕ} (x : Fin m → ℝ) : √(∑ i : Fin m, x i ^ 2) ≤ √↑m * ‖x‖

The Euclidean norm is bounded by √m times the sup norm: √(∑ᵢ xᵢ²) ≤ √m · ‖x‖.

theorem CIV.abs_apply_le_norm {m : ℕ} (x : Fin m → ℝ) (i : Fin m) : |x i| ≤ ‖x‖

Each coordinate is bounded by the sup norm: |xᵢ| ≤ ‖x‖.

theorem CIV.abs_sum_mul_le_norm_mul_sqrt {m : ℕ} (x y : Fin m → ℝ) : |∑ i : Fin m, x i * y i| ≤ ‖x‖ * ∑ i : Fin m, |y i|

Hölder's inequality with the sup norm on x and the ℓ¹ norm on y: |∑ᵢ xᵢ yᵢ| ≤ ‖x‖ · ∑ᵢ |yᵢ|.

theorem CIV.sum_abs_le_sqrt_card_mul_sqrt_sum_sq {m : ℕ} (y : Fin m → ℝ) : ∑ i : Fin m, |y i| ≤ √↑m * √(∑ i : Fin m, y i ^ 2)

Discrete Cauchy–Schwarz: the ℓ¹ norm is bounded by √m times the Euclidean norm, ∑ᵢ |yᵢ| ≤ √m · √(∑ᵢ yᵢ²).