p : ℝ≥0∞
𝕜 : Type ?u.246910
𝕜' : Type ?u.246913
ι : Type u_2
α : ι → Type ?u.246921
β✝ : ι → Type ?u.246926
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ (∑ i : ι, ‖x i‖ ^ 2) ^ (1 / ↑2) = Real.sqrt (∑ i : ι, ‖x i‖ ^ 2)
p : ℝ≥0∞
𝕜 : Type ?u.246910
𝕜' : Type ?u.246913
ι : Type u_2
α : ι → Type ?u.246921
β✝ : ι → Type ?u.246926
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ‖x‖ = Real.sqrt (∑ i : ι, ‖x i‖ ^ 2)
rw [norm_eq_of_nat 2 (by norm_cast) _]
p : ℝ≥0∞
𝕜 : Type ?u.246910
𝕜' : Type ?u.246913
ι : Type u_2
α : ι → Type ?u.246921
β✝ : ι → Type ?u.246926
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ (∑ i : ι, ‖x i‖ ^ 2) ^ (1 / ↑2) = (∑ i : ι, ‖x i‖ ^ 2) ^ (1 / 2)
p : ℝ≥0∞
𝕜 : Type ?u.246910
𝕜' : Type ?u.246913
ι : Type u_2
α : ι → Type ?u.246921
β✝ : ι → Type ?u.246926
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ (∑ i : ι, ‖x i‖ ^ 2) ^ (1 / ↑2) = Real.sqrt (∑ i : ι, ‖x i‖ ^ 2)
rw [Real.sqrt_eq_rpow]
no goals
p : ℝ≥0∞
𝕜 : Type ?u.246910
𝕜' : Type ?u.246913
ι : Type u_2
α : ι → Type ?u.246921
β✝ : ι → Type ?u.246926
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ (∑ i : ι, ‖x i‖ ^ 2) ^ (1 / ↑2) = (∑ i : ι, ‖x i‖ ^ 2) ^ (1 / 2)
norm_cast
no goals
p : ℝ≥0∞
𝕜 : Type ?u.246910
𝕜' : Type ?u.246913
ι : Type u_2
α : ι → Type ?u.246921
β✝ : ι → Type ?u.246926
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ 2 = ↑2
norm_cast