p✝ : ℝ≥0∞
𝕜 : Type ?u.242156
𝕜' : Type ?u.242159
ι : Type u_2
α : ι → Type ?u.242167
β✝ : ι → Type ?u.242172
inst✝³ : Fintype ι
inst✝² : Fact (1 ≤ p✝)
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
n : ℕ
h : p = ↑n
f : PiLp p β
this : 0 < ENNReal.toReal p
⊢ ‖f‖ = (∑ i : ι, ‖f i‖ ^ n) ^ (1 / ↑n)
p✝ : ℝ≥0∞
𝕜 : Type ?u.242156
𝕜' : Type ?u.242159
ι : Type u_2
α : ι → Type ?u.242167
β✝ : ι → Type ?u.242172
inst✝³ : Fintype ι
inst✝² : Fact (1 ≤ p✝)
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
n : ℕ
h : p = ↑n
f : PiLp p β
⊢ ‖f‖ = (∑ i : ι, ‖f i‖ ^ n) ^ (1 / ↑n)
have := p.toReal_pos_iff_ne_top.mpr (ne_of_eq_of_ne h <| ENNReal.nat_ne_top n)
no goals
p✝ : ℝ≥0∞
𝕜 : Type ?u.242156
𝕜' : Type ?u.242159
ι : Type u_2
α : ι → Type ?u.242167
β✝ : ι → Type ?u.242172
inst✝³ : Fintype ι
inst✝² : Fact (1 ≤ p✝)
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
n : ℕ
h : p = ↑n
f : PiLp p β
this : 0 < ENNReal.toReal p
⊢ ‖f‖ = (∑ i : ι, ‖f i‖ ^ n) ^ (1 / ↑n)
simp only [one_div, h, Real.rpow_nat_cast, ENNReal.toReal_nat, eq_self_iff_true, Finset.sum_congr,
  norm_eq_sum this]