norm_le_convexBodySumFun — Mathlib

English

The norm of x is bounded above by convexBodySumFun x: ||x|| ≤ convexBodySumFun x.

Русский

Норма x не превосходит convexBodySumFun x: \\|x\\| ≤ convexBodySumFun x.

LaTeX

$$\$ \\|x\\| \\le convexBodySumFun(x) \$$$

Lean4

theorem norm_le_convexBodySumFun (x : mixedSpace K) : ‖x‖ ≤ convexBodySumFun x :=
  by
  rw [norm_eq_sup'_normAtPlace]
  refine (Finset.sup'_le_iff _ _).mpr fun w _ ↦ ?_
  rw [convexBodySumFun_apply, ← Finset.univ.add_sum_erase _ (Finset.mem_univ w)]
  refine le_add_of_le_of_nonneg ?_ ?_
  · exact le_mul_of_one_le_left (normAtPlace_nonneg w x) one_le_mult
  · exact Finset.sum_nonneg (fun _ _ => mul_nonneg (Nat.cast_pos.mpr mult_pos).le (normAtPlace_nonneg _ _))

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