abs of vector component ≤ norm of vector

Stream: Is there code for X?

[David Renshaw]

Is there an existing lemma that I can appeal to here?

import Mathlib

lemma fst_abs_le_norm (v : EuclideanSpace ℝ (Fin 2)) : |v 0| ≤ ‖v‖ := by
  rw [EuclideanSpace.norm_eq, Fin.sum_univ_two]
  have h : ‖v 0‖ ^ 2 ≤ ‖v 0‖ ^ 2 + ‖v 1‖ ^ 2 := by nlinarith
  have h1 : √(‖v 0‖ ^ 2) ≤ √(‖v 0‖ ^ 2 + ‖v 1‖ ^ 2) := Real.sqrt_le_sqrt h
  have h2 : 0 ≤ ‖v 0‖ := norm_nonneg (v 0)
  rw [Real.sqrt_sq h2] at h1
  rw [←Real.norm_eq_abs]
  exact h1

[David Renshaw]

like Complex.abs_re_le_norm, but for vectors in Euclidean space?

[Eric Wieser]

import Mathlib

lemma nnnorm_apply_le_nnnorm {m} [Fintype m] (v : EuclideanSpace ℝ m) (i : m) : ‖v i‖₊ ≤ ‖v‖₊ := by
  rw [EuclideanSpace.nnnorm_eq, NNReal.le_sqrt_iff_sq_le]
  exact Finset.single_le_sum (f := fun i => ‖v i‖₊ ^ 2) (fun _ _ => zero_le _) (Finset.mem_univ i)

[Eric Wieser]

This should generalize to WithLp

[Eric Wieser]

docs#PiLp.lipschitzWith_equiv is probably hiding the statement you want internally

[Yury G. Kudryashov]

It definitely implies that statement, and probably uses it in the proof.

[Eric Wieser]

#24402 extracts it

[David Renshaw]

added #24415

[Yury G. Kudryashov]

Sent to bors, but some day we should stop abusing defeq for WithLp.

[Eric Wieser]

Paul is working on a refactor that first renames the constructors