α : Type ?u.30416
β : Type ?u.30419
n d k N : ℕ
x✝ x : Fin n → ℕ
hx : x ∈ sphere n d k
⊢ Real.sqrt (∑ i : Fin n, ‖↑(PiLp.equiv 2 fun a => ℝ).symm (Nat.cast ∘ x) i‖ ^ 2) = Real.sqrt ↑k
α : Type ?u.30416
β : Type ?u.30419
n d k N : ℕ
x✝ x : Fin n → ℕ
hx : x ∈ sphere n d k
⊢ ‖↑(PiLp.equiv 2 fun a => ℝ).symm (Nat.cast ∘ x)‖ = Real.sqrt ↑k
rw [EuclideanSpace.norm_eq]
α : Type ?u.30416
β : Type ?u.30419
n d k N : ℕ
x✝ x : Fin n → ℕ
hx : x ∈ sphere n d k
⊢ Real.sqrt (∑ i : Fin n, abs ↑(x i) ^ 2) = Real.sqrt ↑k
α : Type ?u.30416
β : Type ?u.30419
n d k N : ℕ
x✝ x : Fin n → ℕ
hx : x ∈ sphere n d k
⊢ Real.sqrt (∑ i : Fin n, ‖↑(PiLp.equiv 2 fun a => ℝ).symm (Nat.cast ∘ x) i‖ ^ 2) = Real.sqrt ↑k
dsimp
no goals
α : Type ?u.30416
β : Type ?u.30419
n d k N : ℕ
x✝ x : Fin n → ℕ
hx : x ∈ sphere n d k
⊢ Real.sqrt (∑ i : Fin n, abs ↑(x i) ^ 2) = Real.sqrt ↑k
simp_rw [abs_cast, ← cast_pow, ← cast_sum, (mem_filter.1 hx).2]