2-norm of vectors

Stream: mathlib4

[Yi.Yuan]

How can we write the 2-norm of u : Fin n → ℝ, i.e. ‖u‖₂ = √(∑ i, u i ^ 2)? Sometimes it’s unavoidable to use Fin n → ℝ instead of EuclideanSpace ℝ (Fin n) to represent vectors. For example, in the following problem:

/-
P5.2.12 Show that if $A \in \mathbb{R}^{n \times n}$ and $a_i=A(:, i)$, then
$$
|\operatorname{det}(A)| \leq\left\|a_1\right\|_2 \cdots\left\|a_n\right\|_2 .
$$
-/

theorem abs_det_le_product_norm_columns {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) :
    |A.det| ≤ ∏ i : Fin n, ‖(A.transpose) i‖₂ := by
  sorry

I’ve found an ugly way to write ‖(WithLp.toLp (p := 2) (Aᵀ i) : EuclideanSpace ℝ (Fin n))‖, and I’m not satisfied with it.

[Etienne Marion]

You can do this:

import Mathlib

open WithLp

theorem abs_det_le_product_norm_columns {n : ℕ} (A : Matrix (Fin n) (Fin n) ℝ) :
    |A.det| ≤ ∏ i : Fin n, ‖toLp 2 ((A.transpose) i)‖ := by
  sorry

[Yi.Yuan]

Cool, thanks a lot, it really works well.

[Bhavik Mehta]

I have a proof of this result (in transposed form) which I was actually planning to PR today, in case that's useful to you

[Eric Wieser]

A.col i I think is a slightly better working than using transpose