norm_of_mem_sphere — Mathlib

English

Let x be a member of Behrend's sphere n d k. Then the Euclidean norm of the image of x under the standard embedding into Real Pi-space equals the square root of k: ‖WithLp.toLp 2 ((↑) ∘ x : Fin n → ℝ)‖ = √k.

Русский

Пусть x принадлежит сфере Behrend с параметрами n, d, k. Тогда евклидова норма образа x в вещественном пространстве равна √k: ‖WithLp.toLp 2 ((↑) ∘ x : Fin n → ℝ)‖ = √k.

LaTeX

$$$ \\|WithLp.toLp_2((↑) \\circ x)\\| = \\sqrt{k} $$$

Lean4

theorem norm_of_mem_sphere {x : Fin n → ℕ} (hx : x ∈ sphere n d k) : ‖WithLp.toLp 2 ((↑) ∘ x : Fin n → ℝ)‖ = √↑k :=
  by
  rw [EuclideanSpace.norm_eq]
  dsimp
  simp_rw [abs_cast, ← cast_pow, ← cast_sum, (mem_filter.1 hx).2]

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