case a
p✝ : ℝ≥0∞
𝕜 : Type ?u.229074
𝕜' : Type ?u.229077
ι : Type u_2
α : ι → Type ?u.229085
β✝ : ι → Type ?u.229090
inst✝³ : Fintype ι
inst✝² : Fact (1 ≤ p✝)
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
hp : p ≠ ⊤
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp p β
⊢ ↑‖f‖₊ = ↑((∑ i : ι, ‖f i‖₊ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p))
p✝ : ℝ≥0∞
𝕜 : Type ?u.229074
𝕜' : Type ?u.229077
ι : Type u_2
α : ι → Type ?u.229085
β✝ : ι → Type ?u.229090
inst✝³ : Fintype ι
inst✝² : Fact (1 ≤ p✝)
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
hp : p ≠ ⊤
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp p β
⊢ ‖f‖₊ = (∑ i : ι, ‖f i‖₊ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
ext
no goals
case a
p✝ : ℝ≥0∞
𝕜 : Type ?u.229074
𝕜' : Type ?u.229077
ι : Type u_2
α : ι → Type ?u.229085
β✝ : ι → Type ?u.229090
inst✝³ : Fintype ι
inst✝² : Fact (1 ≤ p✝)
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_1
hp : p ≠ ⊤
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp p β
⊢ ↑‖f‖₊ = ↑((∑ i : ι, ‖f i‖₊ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p))
simp [NNReal.coe_sum, norm_eq_sum (p.toReal_pos_iff_ne_top.mpr hp)]