p : ℝ≥0∞
𝕜 : Type ?u.283751
𝕜' : Type ?u.283754
ι : Type u_2
α : ι → Type ?u.283762
β✝ : ι → Type ?u.283767
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ‖x‖ = Real.sqrt (∑ x_1 : ι, ‖x x_1‖ ^ 2)
p : ℝ≥0∞
𝕜 : Type ?u.283751
𝕜' : Type ?u.283754
ι : Type u_2
α : ι → Type ?u.283762
β✝ : ι → Type ?u.283767
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ↑‖x‖₊ = ↑(↑NNReal.sqrt (∑ i : ι, ‖x i‖₊ ^ 2))
push_cast
no goals
p : ℝ≥0∞
𝕜 : Type ?u.283751
𝕜' : Type ?u.283754
ι : Type u_2
α : ι → Type ?u.283762
β✝ : ι → Type ?u.283767
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ‖x‖ = Real.sqrt (∑ x_1 : ι, ‖x x_1‖ ^ 2)
exact norm_eq_of_L2 x