case inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Fintype α
f : { x // x ∈ lp E 0 }
⊢ ‖↑Equiv.lpPiLp f‖ = ‖f‖

case inr.inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Fintype α
f : { x // x ∈ lp E ⊤ }
⊢ ‖↑Equiv.lpPiLp f‖ = ‖f‖

case inr.inr
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Fintype α
f : { x // x ∈ lp E p }
h : 0 < ENNReal.toReal p
⊢ ‖↑Equiv.lpPiLp f‖ = ‖f‖
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Fintype α
f : { x // x ∈ lp E p }
⊢ ‖↑Equiv.lpPiLp f‖ = ‖f‖
rcases p.trichotomy with (rfl | rfl | h)
no goals
case inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Fintype α
f : { x // x ∈ lp E 0 }
⊢ ‖↑Equiv.lpPiLp f‖ = ‖f‖
rw [PiLp.norm_eq_card, lp.norm_eq_card_dsupport]
case inr.inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Fintype α
f : { x // x ∈ lp E ⊤ }
⊢ (⨆ (i : α), ‖↑Equiv.lpPiLp f i‖) = ⨆ (i : α), ‖↑f i‖
case inr.inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Fintype α
f : { x // x ∈ lp E ⊤ }
⊢ ‖↑Equiv.lpPiLp f‖ = ‖f‖
rw [PiLp.norm_eq_ciSup, lp.norm_eq_ciSup]
no goals
case inr.inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Fintype α
f : { x // x ∈ lp E ⊤ }
⊢ (⨆ (i : α), ‖↑Equiv.lpPiLp f i‖) = ⨆ (i : α), ‖↑f i‖
rfl
case inr.inr
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Fintype α
f : { x // x ∈ lp E p }
h : 0 < ENNReal.toReal p
⊢ (Finset.sum Finset.univ fun i => ‖↑Equiv.lpPiLp f i‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p) =
    (Finset.sum Finset.univ fun b => ‖↑f b‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
case inr.inr
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Fintype α
f : { x // x ∈ lp E p }
h : 0 < ENNReal.toReal p
⊢ ‖↑Equiv.lpPiLp f‖ = ‖f‖
rw [PiLp.norm_eq_sum h, lp.norm_eq_tsum_rpow h, tsum_fintype]
no goals
case inr.inr
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Fintype α
f : { x // x ∈ lp E p }
h : 0 < ENNReal.toReal p
⊢ (Finset.sum Finset.univ fun i => ‖↑Equiv.lpPiLp f i‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p) =
    (Finset.sum Finset.univ fun b => ‖↑f b‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
rfl