sum_sq_le_of_mem_box — Mathlib

English

If x ∈ box(n,d), then ∑ i x(i)^2 ≤ n (d−1)^2.

Русский

Если x ∈ box(n,d), то сумма квадратов координат ∑_i x(i)^2 не превосходит n (d−1)^2.

LaTeX

$$$ x \\in box\\, n\\, d \\Rightarrow \\sum_{i} x(i)^2 \\le n (d-1)^2 $$$

Lean4

theorem sum_sq_le_of_mem_box (hx : x ∈ box n d) : ∑ i : Fin n, x i ^ 2 ≤ n * (d - 1) ^ 2 :=
  by
  rw [mem_box] at hx
  have : ∀ i, x i ^ 2 ≤ (d - 1) ^ 2 := fun i => Nat.pow_le_pow_left (Nat.le_sub_one_of_lt (hx i)) _
  exact (sum_le_card_nsmul univ _ _ fun i _ => this i).trans (by rw [Finset.card_fin, smul_eq_mul])

Похожие утверждения