case inl
p : ℝ≥0∞
𝕜 : Type ?u.498893
𝕜' : Type ?u.498896
ι : Type u_2
α : ι → Type ?u.498904
β✝ : ι → Type ?u.498909
inst✝⁹ : Fintype ι
inst✝⁸ : Fact (1 ≤ p)
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β✝ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β✝ i)
c : 𝕜
x y : PiLp p β✝
x' y' : (i : ι) → β✝ i
i : ι
ι' : Type ?u.499105
inst✝³ : Fintype ι'
E : Type ?u.499111
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
β : Type u_1
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ⊤
b : β
h : p = ⊤
⊢ ‖↑(PiLp.equiv p fun x => β).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ ENNReal.toReal (1 / p) * ‖b‖₊

case inr
p : ℝ≥0∞
𝕜 : Type ?u.498893
𝕜' : Type ?u.498896
ι : Type u_2
α : ι → Type ?u.498904
β✝ : ι → Type ?u.498909
inst✝⁹ : Fintype ι
inst✝⁸ : Fact (1 ≤ p)
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β✝ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β✝ i)
c : 𝕜
x y : PiLp p β✝
x' y' : (i : ι) → β✝ i
i : ι
ι' : Type ?u.499105
inst✝³ : Fintype ι'
E : Type ?u.499111
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
β : Type u_1
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ⊤
b : β
h : 1 ≤ ENNReal.toReal p
⊢ ‖↑(PiLp.equiv p fun x => β).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ ENNReal.toReal (1 / p) * ‖b‖₊
p : ℝ≥0∞
𝕜 : Type ?u.498893
𝕜' : Type ?u.498896
ι : Type u_2
α : ι → Type ?u.498904
β✝ : ι → Type ?u.498909
inst✝⁹ : Fintype ι
inst✝⁸ : Fact (1 ≤ p)
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β✝ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β✝ i)
c : 𝕜
x y : PiLp p β✝
x' y' : (i : ι) → β✝ i
i : ι
ι' : Type ?u.499105
inst✝³ : Fintype ι'
E : Type ?u.499111
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
β : Type u_1
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ⊤
b : β
⊢ ‖↑(PiLp.equiv p fun x => β).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ ENNReal.toReal (1 / p) * ‖b‖₊
rcases p.dichotomy with (h | h)
no goals
case inl
p : ℝ≥0∞
𝕜 : Type ?u.498893
𝕜' : Type ?u.498896
ι : Type u_2
α : ι → Type ?u.498904
β✝ : ι → Type ?u.498909
inst✝⁹ : Fintype ι
inst✝⁸ : Fact (1 ≤ p)
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β✝ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β✝ i)
c : 𝕜
x y : PiLp p β✝
x' y' : (i : ι) → β✝ i
i : ι
ι' : Type ?u.499105
inst✝³ : Fintype ι'
E : Type ?u.499111
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
β : Type u_1
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ⊤
b : β
h : p = ⊤
⊢ ‖↑(PiLp.equiv p fun x => β).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ ENNReal.toReal (1 / p) * ‖b‖₊
exact False.elim (hp h)
case inr
p : ℝ≥0∞
𝕜 : Type ?u.498893
𝕜' : Type ?u.498896
ι : Type u_2
α : ι → Type ?u.498904
β✝ : ι → Type ?u.498909
inst✝⁹ : Fintype ι
inst✝⁸ : Fact (1 ≤ p)
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β✝ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β✝ i)
c : 𝕜
x y : PiLp p β✝
x' y' : (i : ι) → β✝ i
i : ι
ι' : Type ?u.499105
inst✝³ : Fintype ι'
E : Type ?u.499111
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
β : Type u_1
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ⊤
b : β
h : 1 ≤ ENNReal.toReal p
ne_zero : ENNReal.toReal p ≠ 0
⊢ ‖↑(PiLp.equiv p fun x => β).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ ENNReal.toReal (1 / p) * ‖b‖₊
case inr
p : ℝ≥0∞
𝕜 : Type ?u.498893
𝕜' : Type ?u.498896
ι : Type u_2
α : ι → Type ?u.498904
β✝ : ι → Type ?u.498909
inst✝⁹ : Fintype ι
inst✝⁸ : Fact (1 ≤ p)
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β✝ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β✝ i)
c : 𝕜
x y : PiLp p β✝
x' y' : (i : ι) → β✝ i
i : ι
ι' : Type ?u.499105
inst✝³ : Fintype ι'
E : Type ?u.499111
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
β : Type u_1
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ⊤
b : β
h : 1 ≤ ENNReal.toReal p
⊢ ‖↑(PiLp.equiv p fun x => β).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ ENNReal.toReal (1 / p) * ‖b‖₊
have ne_zero : p.toReal ≠ 0 := (zero_lt_one.trans_le h).ne'
no goals
case inr
p : ℝ≥0∞
𝕜 : Type ?u.498893
𝕜' : Type ?u.498896
ι : Type u_2
α : ι → Type ?u.498904
β✝ : ι → Type ?u.498909
inst✝⁹ : Fintype ι
inst✝⁸ : Fact (1 ≤ p)
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β✝ i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β✝ i)
c : 𝕜
x y : PiLp p β✝
x' y' : (i : ι) → β✝ i
i : ι
ι' : Type ?u.499105
inst✝³ : Fintype ι'
E : Type ?u.499111
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
β : Type u_1
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ⊤
b : β
h : 1 ≤ ENNReal.toReal p
ne_zero : ENNReal.toReal p ≠ 0
⊢ ‖↑(PiLp.equiv p fun x => β).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ ENNReal.toReal (1 / p) * ‖b‖₊
simp_rw [nnnorm_eq_sum hp, equiv_symm_apply, Function.const_apply, Finset.sum_const,
  Finset.card_univ, nsmul_eq_mul, NNReal.mul_rpow, ← NNReal.rpow_mul,
  mul_one_div_cancel ne_zero, NNReal.rpow_one, ENNReal.toReal_div, ENNReal.one_toReal]