[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝¹ : Fintype ι
inst✝ : (i : ι) → EDist (β i)
f g : PiLp ⊤ β
⊢ edist f g = ⨆ (i : ι), edist (f i) (g i)
[PROOFSTEP]
dsimp [edist]
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝¹ : Fintype ι
inst✝ : (i : ι) → EDist (β i)
f g : PiLp ⊤ β
⊢ (if ⊤ = 0 then ↑(Finset.card (Finite.toFinset (_ : Set.Finite {i | f i ≠ g i})))
    else if ⊤ = ⊤ then ⨆ (i : ι), edist (f i) (g i) else (∑ i : ι, edist (f i) (g i) ^ 0) ^ (1 / 0)) =
    ⨆ (i : ι), edist (f i) (g i)
[PROOFSTEP]
exact if_neg ENNReal.top_ne_zero
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp p β
⊢ edist f f = 0
[PROOFSTEP]
rcases p.trichotomy with (rfl | rfl | h)
[GOAL]
case inl
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp 0 β
⊢ edist f f = 0
[PROOFSTEP]
simp [edist_eq_card]
[GOAL]
case inr.inl
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp ⊤ β
⊢ edist f f = 0
[PROOFSTEP]
simp [edist_eq_iSup]
[GOAL]
case inr.inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f : PiLp p β
h : 0 < ENNReal.toReal p
⊢ edist f f = 0
[PROOFSTEP]
simp [edist_eq_sum h, ENNReal.zero_rpow_of_pos h, ENNReal.zero_rpow_of_pos (inv_pos.2 <| h)]
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp p β
⊢ edist f g = edist g f
[PROOFSTEP]
rcases p.trichotomy with (rfl | rfl | h)
[GOAL]
case inl
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp 0 β
⊢ edist f g = edist g f
[PROOFSTEP]
simp only [edist_eq_card, eq_comm, Ne.def]
[GOAL]
case inr.inl
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp ⊤ β
⊢ edist f g = edist g f
[PROOFSTEP]
simp only [edist_eq_iSup, edist_comm]
[GOAL]
case inr.inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝¹ : Fintype ι
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
f g : PiLp p β
h : 0 < ENNReal.toReal p
⊢ edist f g = edist g f
[PROOFSTEP]
simp only [edist_eq_sum h, edist_comm]
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝¹ : Fintype ι
inst✝ : (i : ι) → Dist (α i)
f g : PiLp ⊤ α
⊢ dist f g = ⨆ (i : ι), dist (f i) (g i)
[PROOFSTEP]
dsimp [dist]
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝¹ : Fintype ι
inst✝ : (i : ι) → Dist (α i)
f g : PiLp ⊤ α
⊢ (if ⊤ = 0 then ↑(Finset.card (Finite.toFinset (_ : Set.Finite {i | f i ≠ g i})))
    else if ⊤ = ⊤ then ⨆ (i : ι), dist (f i) (g i) else (∑ i : ι, dist (f i) (g i) ^ 0) ^ (1 / 0)) =
    ⨆ (i : ι), dist (f i) (g i)
[PROOFSTEP]
exact if_neg ENNReal.top_ne_zero
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : (i : ι) → Norm (β i)
inst✝ : (i : ι) → Zero (β i)
f : PiLp ⊤ β
⊢ ‖f‖ = ⨆ (i : ι), ‖f i‖
[PROOFSTEP]
dsimp [Norm.norm]
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : (i : ι) → Norm (β i)
inst✝ : (i : ι) → Zero (β i)
f : PiLp ⊤ β
⊢ (if ⊤ = 0 then ↑(Finset.card (Finite.toFinset (_ : Set.Finite {i | f i ≠ 0})))
    else if ⊤ = ⊤ then ⨆ (i : ι), ‖f i‖ else (∑ i : ι, ‖f i‖ ^ 0) ^ (1 / 0)) =
    ⨆ (i : ι), ‖f i‖
[PROOFSTEP]
exact if_neg ENNReal.top_ne_zero
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
f g h : PiLp p β
⊢ edist f h ≤ edist f g + edist g h
[PROOFSTEP]
rcases p.dichotomy with (rfl | hp)
[GOAL]
case inl
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ⊤)
f g h : PiLp ⊤ β
⊢ edist f h ≤ edist f g + edist g h
[PROOFSTEP]
simp only [edist_eq_iSup]
[GOAL]
case inl
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ⊤)
f g h : PiLp ⊤ β
⊢ ⨆ (i : ι), edist (f i) (h i) ≤ (⨆ (i : ι), edist (f i) (g i)) + ⨆ (i : ι), edist (g i) (h i)
[PROOFSTEP]
cases isEmpty_or_nonempty ι
[GOAL]
case inl.inl
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ⊤)
f g h : PiLp ⊤ β
h✝ : IsEmpty ι
⊢ ⨆ (i : ι), edist (f i) (h i) ≤ (⨆ (i : ι), edist (f i) (g i)) + ⨆ (i : ι), edist (g i) (h i)
[PROOFSTEP]
simp only [ciSup_of_empty, ENNReal.bot_eq_zero, add_zero, nonpos_iff_eq_zero]
  -- Porting note: `le_iSup` needed some help
[GOAL]
case inl.inr
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ⊤)
f g h : PiLp ⊤ β
h✝ : Nonempty ι
⊢ ⨆ (i : ι), edist (f i) (h i) ≤ (⨆ (i : ι), edist (f i) (g i)) + ⨆ (i : ι), edist (g i) (h i)
[PROOFSTEP]
refine
  iSup_le fun i =>
    (edist_triangle _ (g i) _).trans <|
      add_le_add (le_iSup (fun k => edist (f k) (g k)) i) (le_iSup (fun k => edist (g k) (h k)) i)
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
f g h : PiLp p β
hp : 1 ≤ ENNReal.toReal p
⊢ edist f h ≤ edist f g + edist g h
[PROOFSTEP]
simp only [edist_eq_sum (zero_lt_one.trans_le hp)]
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
f g h : PiLp p β
hp : 1 ≤ ENNReal.toReal p
⊢ (∑ i : ι, edist (f i) (h i) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p) ≤
    (∑ i : ι, edist (f i) (g i) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p) +
      (∑ i : ι, edist (g i) (h i) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
[PROOFSTEP]
calc
  (∑ i, edist (f i) (h i) ^ p.toReal) ^ (1 / p.toReal) ≤
      (∑ i, (edist (f i) (g i) + edist (g i) (h i)) ^ p.toReal) ^ (1 / p.toReal) :=
    by
    apply ENNReal.rpow_le_rpow _ (one_div_nonneg.2 <| zero_le_one.trans hp)
    refine' Finset.sum_le_sum fun i _ => _
    exact ENNReal.rpow_le_rpow (edist_triangle _ _ _) (zero_le_one.trans hp)
  _ ≤ (∑ i, edist (f i) (g i) ^ p.toReal) ^ (1 / p.toReal) + (∑ i, edist (g i) (h i) ^ p.toReal) ^ (1 / p.toReal) :=
    ENNReal.Lp_add_le _ _ _ hp
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
f g h : PiLp p β
hp : 1 ≤ ENNReal.toReal p
⊢ (∑ i : ι, edist (f i) (h i) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p) ≤
    (∑ i : ι, (edist (f i) (g i) + edist (g i) (h i)) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
[PROOFSTEP]
apply ENNReal.rpow_le_rpow _ (one_div_nonneg.2 <| zero_le_one.trans hp)
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
f g h : PiLp p β
hp : 1 ≤ ENNReal.toReal p
⊢ ∑ i : ι, edist (f i) (h i) ^ ENNReal.toReal p ≤ ∑ i : ι, (edist (f i) (g i) + edist (g i) (h i)) ^ ENNReal.toReal p
[PROOFSTEP]
refine' Finset.sum_le_sum fun i _ => _
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
f g h : PiLp p β
hp : 1 ≤ ENNReal.toReal p
i : ι
x✝ : i ∈ Finset.univ
⊢ edist (f i) (h i) ^ ENNReal.toReal p ≤ (edist (f i) (g i) + edist (g i) (h i)) ^ ENNReal.toReal p
[PROOFSTEP]
exact ENNReal.rpow_le_rpow (edist_triangle _ _ _) (zero_le_one.trans hp)
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι✝ : Type u_3
α✝ : ι✝ → Type u_4
β : ι✝ → Type u_5
inst✝⁵ : Fact (1 ≤ p)
inst✝⁴ : (i : ι✝) → PseudoMetricSpace (α✝ i)
inst✝³ : (i : ι✝) → PseudoEMetricSpace (β i)
inst✝² : Fintype ι✝
ι : Type u_6
inst✝¹ : Finite ι
α : ι → Type u_7
inst✝ : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ⊤ α
⊢ ⨆ (i : ι), edist (f i) (g i) ≠ ⊤
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι✝ : Type u_3
α✝ : ι✝ → Type u_4
β : ι✝ → Type u_5
inst✝⁵ : Fact (1 ≤ p)
inst✝⁴ : (i : ι✝) → PseudoMetricSpace (α✝ i)
inst✝³ : (i : ι✝) → PseudoEMetricSpace (β i)
inst✝² : Fintype ι✝
ι : Type u_6
inst✝¹ : Finite ι
α : ι → Type u_7
inst✝ : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ⊤ α
val✝ : Fintype ι
⊢ ⨆ (i : ι), edist (f i) (g i) ≠ ⊤
[PROOFSTEP]
obtain ⟨M, hM⟩ := Fintype.exists_le fun i => (⟨dist (f i) (g i), dist_nonneg⟩ : ℝ≥0)
[GOAL]
case intro.intro
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι✝ : Type u_3
α✝ : ι✝ → Type u_4
β : ι✝ → Type u_5
inst✝⁵ : Fact (1 ≤ p)
inst✝⁴ : (i : ι✝) → PseudoMetricSpace (α✝ i)
inst✝³ : (i : ι✝) → PseudoEMetricSpace (β i)
inst✝² : Fintype ι✝
ι : Type u_6
inst✝¹ : Finite ι
α : ι → Type u_7
inst✝ : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ⊤ α
val✝ : Fintype ι
M : { r // 0 ≤ r }
hM : ∀ (i : ι), { val := dist (f i) (g i), property := (_ : 0 ≤ dist (f i) (g i)) } ≤ M
⊢ ⨆ (i : ι), edist (f i) (g i) ≠ ⊤
[PROOFSTEP]
refine' ne_of_lt ((iSup_le fun i => _).trans_lt (@ENNReal.coe_lt_top M))
[GOAL]
case intro.intro
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι✝ : Type u_3
α✝ : ι✝ → Type u_4
β : ι✝ → Type u_5
inst✝⁵ : Fact (1 ≤ p)
inst✝⁴ : (i : ι✝) → PseudoMetricSpace (α✝ i)
inst✝³ : (i : ι✝) → PseudoEMetricSpace (β i)
inst✝² : Fintype ι✝
ι : Type u_6
inst✝¹ : Finite ι
α : ι → Type u_7
inst✝ : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ⊤ α
val✝ : Fintype ι
M : { r // 0 ≤ r }
hM : ∀ (i : ι), { val := dist (f i) (g i), property := (_ : 0 ≤ dist (f i) (g i)) } ≤ M
i : ι
⊢ edist (f i) (g i) ≤ ↑M
[PROOFSTEP]
simp only [edist, PseudoMetricSpace.edist_dist, ENNReal.ofReal_eq_coe_nnreal dist_nonneg]
[GOAL]
case intro.intro
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι✝ : Type u_3
α✝ : ι✝ → Type u_4
β : ι✝ → Type u_5
inst✝⁵ : Fact (1 ≤ p)
inst✝⁴ : (i : ι✝) → PseudoMetricSpace (α✝ i)
inst✝³ : (i : ι✝) → PseudoEMetricSpace (β i)
inst✝² : Fintype ι✝
ι : Type u_6
inst✝¹ : Finite ι
α : ι → Type u_7
inst✝ : (i : ι) → PseudoMetricSpace (α i)
f g : PiLp ⊤ α
val✝ : Fintype ι
M : { r // 0 ≤ r }
hM : ∀ (i : ι), { val := dist (f i) (g i), property := (_ : 0 ≤ dist (f i) (g i)) } ≤ M
i : ι
⊢ ↑{ val := dist (f i) (g i), property := (_ : 0 ≤ dist (f i) (g i)) } ≤ ↑M
[PROOFSTEP]
exact_mod_cast hM i
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
f g : PiLp p α
⊢ edist f g ≠ ⊤
[PROOFSTEP]
rcases p.dichotomy with (rfl | h)
[GOAL]
case inl
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ⊤)
f g : PiLp ⊤ α
⊢ edist f g ≠ ⊤
[PROOFSTEP]
exact iSup_edist_ne_top_aux f g
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
f g : PiLp p α
h : 1 ≤ ENNReal.toReal p
⊢ edist f g ≠ ⊤
[PROOFSTEP]
rw [edist_eq_sum (zero_lt_one.trans_le h)]
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
f g : PiLp p α
h : 1 ≤ ENNReal.toReal p
⊢ (∑ i : ι, edist (f i) (g i) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p) ≠ ⊤
[PROOFSTEP]
exact
  ENNReal.rpow_ne_top_of_nonneg (one_div_nonneg.2 (zero_le_one.trans h))
    (ne_of_lt <| ENNReal.sum_lt_top fun i hi => ENNReal.rpow_ne_top_of_nonneg (zero_le_one.trans h) (edist_ne_top _ _))
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
f g : PiLp p α
⊢ dist f g = ENNReal.toReal (edist f g)
[PROOFSTEP]
rcases p.dichotomy with (rfl | h)
[GOAL]
case inl
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ⊤)
f g : PiLp ⊤ α
⊢ dist f g = ENNReal.toReal (edist f g)
[PROOFSTEP]
rw [edist_eq_iSup, dist_eq_iSup]
[GOAL]
case inl
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ⊤)
f g : PiLp ⊤ α
⊢ ⨆ (i : ι), dist (f i) (g i) = ENNReal.toReal (⨆ (i : ι), edist (f i) (g i))
[PROOFSTEP]
cases isEmpty_or_nonempty ι
[GOAL]
case inl.inl
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ⊤)
f g : PiLp ⊤ α
h✝ : IsEmpty ι
⊢ ⨆ (i : ι), dist (f i) (g i) = ENNReal.toReal (⨆ (i : ι), edist (f i) (g i))
[PROOFSTEP]
simp only [Real.ciSup_empty, ciSup_of_empty, ENNReal.bot_eq_zero, ENNReal.zero_toReal]
[GOAL]
case inl.inr
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ⊤)
f g : PiLp ⊤ α
h✝ : Nonempty ι
⊢ ⨆ (i : ι), dist (f i) (g i) = ENNReal.toReal (⨆ (i : ι), edist (f i) (g i))
[PROOFSTEP]
refine' le_antisymm (ciSup_le fun i => _) _
[GOAL]
case inl.inr.refine'_1
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ⊤)
f g : PiLp ⊤ α
h✝ : Nonempty ι
i : ι
⊢ dist (f i) (g i) ≤ ENNReal.toReal (⨆ (i : ι), edist (f i) (g i))
[PROOFSTEP]
rw [← ENNReal.ofReal_le_iff_le_toReal (iSup_edist_ne_top_aux f g), ← PseudoMetricSpace.edist_dist]
  -- Porting note: `le_iSup` needed some help
[GOAL]
case inl.inr.refine'_1
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ⊤)
f g : PiLp ⊤ α
h✝ : Nonempty ι
i : ι
⊢ PseudoMetricSpace.edist (f i) (g i) ≤ ⨆ (i : ι), edist (f i) (g i)
[PROOFSTEP]
exact le_iSup (fun k => edist (f k) (g k)) i
[GOAL]
case inl.inr.refine'_2
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ⊤)
f g : PiLp ⊤ α
h✝ : Nonempty ι
⊢ ENNReal.toReal (⨆ (i : ι), edist (f i) (g i)) ≤ ⨆ (i : ι), dist (f i) (g i)
[PROOFSTEP]
refine' ENNReal.toReal_le_of_le_ofReal (Real.sSup_nonneg _ _) (iSup_le fun i => _)
[GOAL]
case inl.inr.refine'_2.refine'_1
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ⊤)
f g : PiLp ⊤ α
h✝ : Nonempty ι
⊢ ∀ (x : ℝ), (x ∈ range fun i => dist (f i) (g i)) → 0 ≤ x
[PROOFSTEP]
rintro - ⟨i, rfl⟩
[GOAL]
case inl.inr.refine'_2.refine'_1.intro
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ⊤)
f g : PiLp ⊤ α
h✝ : Nonempty ι
i : ι
⊢ 0 ≤ (fun i => dist (f i) (g i)) i
[PROOFSTEP]
exact dist_nonneg
[GOAL]
case inl.inr.refine'_2.refine'_2
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ⊤)
f g : PiLp ⊤ α
h✝ : Nonempty ι
i : ι
⊢ edist (f i) (g i) ≤ ENNReal.ofReal (⨆ (i : ι), dist (f i) (g i))
[PROOFSTEP]
change PseudoMetricSpace.edist _ _ ≤ _
[GOAL]
case inl.inr.refine'_2.refine'_2
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ⊤)
f g : PiLp ⊤ α
h✝ : Nonempty ι
i : ι
⊢ PseudoMetricSpace.edist (f i) (g i) ≤ ENNReal.ofReal (⨆ (i : ι), dist (f i) (g i))
[PROOFSTEP]
rw [PseudoMetricSpace.edist_dist]
  -- Porting note: `le_ciSup` needed some help
[GOAL]
case inl.inr.refine'_2.refine'_2
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ⊤)
f g : PiLp ⊤ α
h✝ : Nonempty ι
i : ι
⊢ ENNReal.ofReal (dist (f i) (g i)) ≤ ENNReal.ofReal (⨆ (i : ι), dist (f i) (g i))
[PROOFSTEP]
exact ENNReal.ofReal_le_ofReal (le_ciSup (Fintype.bddAbove_range (fun k => dist (f k) (g k))) i)
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
f g : PiLp p α
h : 1 ≤ ENNReal.toReal p
⊢ dist f g = ENNReal.toReal (edist f g)
[PROOFSTEP]
have A : ∀ i, edist (f i) (g i) ^ p.toReal ≠ ⊤ := fun i =>
  ENNReal.rpow_ne_top_of_nonneg (zero_le_one.trans h) (edist_ne_top _ _)
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
f g : PiLp p α
h : 1 ≤ ENNReal.toReal p
A : ∀ (i : ι), edist (f i) (g i) ^ ENNReal.toReal p ≠ ⊤
⊢ dist f g = ENNReal.toReal (edist f g)
[PROOFSTEP]
simp only [edist_eq_sum (zero_lt_one.trans_le h), dist_edist, ENNReal.toReal_rpow, dist_eq_sum (zero_lt_one.trans_le h),
  ← ENNReal.toReal_sum fun i _ => A i]
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
⊢ LipschitzWith 1 ↑(equiv p β)
[PROOFSTEP]
intro x y
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
⊢ edist (↑(equiv p β) x) (↑(equiv p β) y) ≤ ↑1 * edist x y
[PROOFSTEP]
rcases p.dichotomy with (rfl | h)
[GOAL]
case inl
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ⊤)
x y : PiLp ⊤ β
⊢ edist (↑(equiv ⊤ β) x) (↑(equiv ⊤ β) y) ≤ ↑1 * edist x y
[PROOFSTEP]
simpa only [ENNReal.coe_one, one_mul, edist_eq_iSup, edist, Finset.sup_le_iff, Finset.mem_univ, forall_true_left] using
  le_iSup fun i => edist (x i) (y i)
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
⊢ edist (↑(equiv p β) x) (↑(equiv p β) y) ≤ ↑1 * edist x y
[PROOFSTEP]
have cancel : p.toReal * (1 / p.toReal) = 1 := mul_div_cancel' 1 (zero_lt_one.trans_le h).ne'
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
cancel : ENNReal.toReal p * (1 / ENNReal.toReal p) = 1
⊢ edist (↑(equiv p β) x) (↑(equiv p β) y) ≤ ↑1 * edist x y
[PROOFSTEP]
rw [edist_eq_sum (zero_lt_one.trans_le h)]
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
cancel : ENNReal.toReal p * (1 / ENNReal.toReal p) = 1
⊢ edist (↑(equiv p β) x) (↑(equiv p β) y) ≤
    ↑1 * (∑ i : ι, edist (x i) (y i) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
[PROOFSTEP]
simp only [edist, forall_prop_of_true, one_mul, Finset.mem_univ, Finset.sup_le_iff, ENNReal.coe_one]
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
cancel : ENNReal.toReal p * (1 / ENNReal.toReal p) = 1
⊢ ∀ (b : ι),
    edist (↑(equiv p β) x b) (↑(equiv p β) y b) ≤
      (∑ x_1 : ι, edist (x x_1) (y x_1) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
[PROOFSTEP]
intro i
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
cancel : ENNReal.toReal p * (1 / ENNReal.toReal p) = 1
i : ι
⊢ edist (↑(equiv p β) x i) (↑(equiv p β) y i) ≤
    (∑ x_1 : ι, edist (x x_1) (y x_1) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
[PROOFSTEP]
calc
  edist (x i) (y i) = (edist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal) := by simp [← ENNReal.rpow_mul, cancel, -one_div]
  _ ≤ (∑ i, edist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal) :=
    by
    apply ENNReal.rpow_le_rpow _ (one_div_nonneg.2 <| zero_le_one.trans h)
    exact Finset.single_le_sum (fun i _ => (bot_le : (0 : ℝ≥0∞) ≤ _)) (Finset.mem_univ i)
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
cancel : ENNReal.toReal p * (1 / ENNReal.toReal p) = 1
i : ι
⊢ edist (x i) (y i) = (edist (x i) (y i) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
[PROOFSTEP]
simp [← ENNReal.rpow_mul, cancel, -one_div]
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
cancel : ENNReal.toReal p * (1 / ENNReal.toReal p) = 1
i : ι
⊢ (edist (x i) (y i) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p) ≤
    (∑ i : ι, edist (x i) (y i) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
[PROOFSTEP]
apply ENNReal.rpow_le_rpow _ (one_div_nonneg.2 <| zero_le_one.trans h)
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
cancel : ENNReal.toReal p * (1 / ENNReal.toReal p) = 1
i : ι
⊢ edist (x i) (y i) ^ ENNReal.toReal p ≤ ∑ i : ι, edist (x i) (y i) ^ ENNReal.toReal p
[PROOFSTEP]
exact Finset.single_le_sum (fun i _ => (bot_le : (0 : ℝ≥0∞) ≤ _)) (Finset.mem_univ i)
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
⊢ AntilipschitzWith (↑(Fintype.card ι) ^ ENNReal.toReal (1 / p)) ↑(equiv p β)
[PROOFSTEP]
intro x y
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
⊢ edist x y ≤ ↑(↑(Fintype.card ι) ^ ENNReal.toReal (1 / p)) * edist (↑(equiv p β) x) (↑(equiv p β) y)
[PROOFSTEP]
rcases p.dichotomy with (rfl | h)
[GOAL]
case inl
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ⊤)
x y : PiLp ⊤ β
⊢ edist x y ≤ ↑(↑(Fintype.card ι) ^ ENNReal.toReal (1 / ⊤)) * edist (↑(equiv ⊤ β) x) (↑(equiv ⊤ β) y)
[PROOFSTEP]
simp only [edist_eq_iSup, ENNReal.div_top, ENNReal.zero_toReal, NNReal.rpow_zero, ENNReal.coe_one, one_mul, iSup_le_iff]
  -- Porting note: `Finset.le_sup` needed some help
[GOAL]
case inl
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ⊤)
x y : PiLp ⊤ β
⊢ ∀ (i : ι), edist (x i) (y i) ≤ edist (↑(equiv ⊤ β) x) (↑(equiv ⊤ β) y)
[PROOFSTEP]
exact fun i => Finset.le_sup (f := fun i => edist (x i) (y i)) (Finset.mem_univ i)
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
⊢ edist x y ≤ ↑(↑(Fintype.card ι) ^ ENNReal.toReal (1 / p)) * edist (↑(equiv p β) x) (↑(equiv p β) y)
[PROOFSTEP]
have pos : 0 < p.toReal := zero_lt_one.trans_le h
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
pos : 0 < ENNReal.toReal p
⊢ edist x y ≤ ↑(↑(Fintype.card ι) ^ ENNReal.toReal (1 / p)) * edist (↑(equiv p β) x) (↑(equiv p β) y)
[PROOFSTEP]
have nonneg : 0 ≤ 1 / p.toReal := one_div_nonneg.2 (le_of_lt pos)
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
pos : 0 < ENNReal.toReal p
nonneg : 0 ≤ 1 / ENNReal.toReal p
⊢ edist x y ≤ ↑(↑(Fintype.card ι) ^ ENNReal.toReal (1 / p)) * edist (↑(equiv p β) x) (↑(equiv p β) y)
[PROOFSTEP]
have cancel : p.toReal * (1 / p.toReal) = 1 := mul_div_cancel' 1 (ne_of_gt pos)
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
pos : 0 < ENNReal.toReal p
nonneg : 0 ≤ 1 / ENNReal.toReal p
cancel : ENNReal.toReal p * (1 / ENNReal.toReal p) = 1
⊢ edist x y ≤ ↑(↑(Fintype.card ι) ^ ENNReal.toReal (1 / p)) * edist (↑(equiv p β) x) (↑(equiv p β) y)
[PROOFSTEP]
rw [edist_eq_sum pos, ENNReal.toReal_div 1 p]
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
pos : 0 < ENNReal.toReal p
nonneg : 0 ≤ 1 / ENNReal.toReal p
cancel : ENNReal.toReal p * (1 / ENNReal.toReal p) = 1
⊢ (∑ i : ι, edist (x i) (y i) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p) ≤
    ↑(↑(Fintype.card ι) ^ (ENNReal.toReal 1 / ENNReal.toReal p)) * edist (↑(equiv p β) x) (↑(equiv p β) y)
[PROOFSTEP]
simp only [edist, ← one_div, ENNReal.one_toReal]
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
pos : 0 < ENNReal.toReal p
nonneg : 0 ≤ 1 / ENNReal.toReal p
cancel : ENNReal.toReal p * (1 / ENNReal.toReal p) = 1
⊢ (∑ x_1 : ι, edist (x x_1) (y x_1) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p) ≤
    ↑(↑(Fintype.card ι) ^ (1 / ENNReal.toReal p)) *
      Finset.sup Finset.univ fun b => edist (↑(equiv p β) x b) (↑(equiv p β) y b)
[PROOFSTEP]
calc
  (∑ i, edist (x i) (y i) ^ p.toReal) ^ (1 / p.toReal) ≤
      (∑ _i, edist (PiLp.equiv p β x) (PiLp.equiv p β y) ^ p.toReal) ^ (1 / p.toReal) :=
    by
    refine ENNReal.rpow_le_rpow ?_ nonneg
    swap
    refine Finset.sum_le_sum fun i _ => ?_
    apply ENNReal.rpow_le_rpow _ (le_of_lt pos)
    exact Finset.le_sup (f := fun i => edist (x i) (y i)) (Finset.mem_univ i)
  _ = ((Fintype.card ι : ℝ≥0) ^ (1 / p.toReal) : ℝ≥0) * edist (PiLp.equiv p β x) (PiLp.equiv p β y) :=
    by
    simp only [nsmul_eq_mul, Finset.card_univ, ENNReal.rpow_one, Finset.sum_const,
      ENNReal.mul_rpow_of_nonneg _ _ nonneg, ← ENNReal.rpow_mul, cancel]
    have : (Fintype.card ι : ℝ≥0∞) = (Fintype.card ι : ℝ≥0) := (ENNReal.coe_nat (Fintype.card ι)).symm
    rw [this, ENNReal.coe_rpow_of_nonneg _ nonneg]
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
pos : 0 < ENNReal.toReal p
nonneg : 0 ≤ 1 / ENNReal.toReal p
cancel : ENNReal.toReal p * (1 / ENNReal.toReal p) = 1
⊢ (∑ i : ι, edist (x i) (y i) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p) ≤
    (∑ _i : ?m.67030, edist (↑(equiv p β) x) (↑(equiv p β) y) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
[PROOFSTEP]
refine ENNReal.rpow_le_rpow ?_ nonneg
[GOAL]
case refine_1
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
pos : 0 < ENNReal.toReal p
nonneg : 0 ≤ 1 / ENNReal.toReal p
cancel : ENNReal.toReal p * (1 / ENNReal.toReal p) = 1
⊢ Fintype ?m.67030
case refine_2
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
pos : 0 < ENNReal.toReal p
nonneg : 0 ≤ 1 / ENNReal.toReal p
cancel : ENNReal.toReal p * (1 / ENNReal.toReal p) = 1
⊢ ∑ i : ι, edist (x i) (y i) ^ ENNReal.toReal p ≤
    ∑ _i : ?m.67030, edist (↑(equiv p β) x) (↑(equiv p β) y) ^ ENNReal.toReal p
[PROOFSTEP]
swap
[GOAL]
case refine_2
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
pos : 0 < ENNReal.toReal p
nonneg : 0 ≤ 1 / ENNReal.toReal p
cancel : ENNReal.toReal p * (1 / ENNReal.toReal p) = 1
⊢ ∑ i : ι, edist (x i) (y i) ^ ENNReal.toReal p ≤
    ∑ _i : ?m.67030, edist (↑(equiv p β) x) (↑(equiv p β) y) ^ ENNReal.toReal p
case refine_1
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
pos : 0 < ENNReal.toReal p
nonneg : 0 ≤ 1 / ENNReal.toReal p
cancel : ENNReal.toReal p * (1 / ENNReal.toReal p) = 1
⊢ Fintype ?m.67030
[PROOFSTEP]
refine Finset.sum_le_sum fun i _ => ?_
[GOAL]
case refine_2
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
pos : 0 < ENNReal.toReal p
nonneg : 0 ≤ 1 / ENNReal.toReal p
cancel : ENNReal.toReal p * (1 / ENNReal.toReal p) = 1
i : ι
x✝ : i ∈ Finset.univ
⊢ edist (x i) (y i) ^ ENNReal.toReal p ≤ edist (↑(equiv p β) x) (↑(equiv p β) y) ^ ENNReal.toReal p
[PROOFSTEP]
apply ENNReal.rpow_le_rpow _ (le_of_lt pos)
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
pos : 0 < ENNReal.toReal p
nonneg : 0 ≤ 1 / ENNReal.toReal p
cancel : ENNReal.toReal p * (1 / ENNReal.toReal p) = 1
i : ι
x✝ : i ∈ Finset.univ
⊢ edist (x i) (y i) ≤ edist (↑(equiv p β) x) (↑(equiv p β) y)
[PROOFSTEP]
exact Finset.le_sup (f := fun i => edist (x i) (y i)) (Finset.mem_univ i)
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
pos : 0 < ENNReal.toReal p
nonneg : 0 ≤ 1 / ENNReal.toReal p
cancel : ENNReal.toReal p * (1 / ENNReal.toReal p) = 1
⊢ (∑ _i : ι, edist (↑(equiv p β) x) (↑(equiv p β) y) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p) =
    ↑(↑(Fintype.card ι) ^ (1 / ENNReal.toReal p)) * edist (↑(equiv p β) x) (↑(equiv p β) y)
[PROOFSTEP]
simp only [nsmul_eq_mul, Finset.card_univ, ENNReal.rpow_one, Finset.sum_const, ENNReal.mul_rpow_of_nonneg _ _ nonneg, ←
  ENNReal.rpow_mul, cancel]
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
pos : 0 < ENNReal.toReal p
nonneg : 0 ≤ 1 / ENNReal.toReal p
cancel : ENNReal.toReal p * (1 / ENNReal.toReal p) = 1
⊢ ↑(Fintype.card ι) ^ (1 / ENNReal.toReal p) * edist (↑(equiv p β) x) (↑(equiv p β) y) =
    ↑(↑(Fintype.card ι) ^ (1 / ENNReal.toReal p)) * edist (↑(equiv p β) x) (↑(equiv p β) y)
[PROOFSTEP]
have : (Fintype.card ι : ℝ≥0∞) = (Fintype.card ι : ℝ≥0) := (ENNReal.coe_nat (Fintype.card ι)).symm
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
pos : 0 < ENNReal.toReal p
nonneg : 0 ≤ 1 / ENNReal.toReal p
cancel : ENNReal.toReal p * (1 / ENNReal.toReal p) = 1
this : ↑(Fintype.card ι) = ↑↑(Fintype.card ι)
⊢ ↑(Fintype.card ι) ^ (1 / ENNReal.toReal p) * edist (↑(equiv p β) x) (↑(equiv p β) y) =
    ↑(↑(Fintype.card ι) ^ (1 / ENNReal.toReal p)) * edist (↑(equiv p β) x) (↑(equiv p β) y)
[PROOFSTEP]
rw [this, ENNReal.coe_rpow_of_nonneg _ nonneg]
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
⊢ 𝓤 (PiLp p β) = 𝓤 ((i : ι) → β i)
[PROOFSTEP]
have A : UniformInducing (PiLp.equiv p β) :=
  (antilipschitzWith_equiv_aux p β).uniformInducing (lipschitzWith_equiv_aux p β).uniformContinuous
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
A : UniformInducing ↑(equiv p β)
⊢ 𝓤 (PiLp p β) = 𝓤 ((i : ι) → β i)
[PROOFSTEP]
have : (fun x : PiLp p β × PiLp p β => ((PiLp.equiv p β) x.fst, (PiLp.equiv p β) x.snd)) = id := by ext i <;> rfl
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
A : UniformInducing ↑(equiv p β)
⊢ (fun x => (↑(equiv p β) x.fst, ↑(equiv p β) x.snd)) = id
[PROOFSTEP]
ext i
[GOAL]
case h.h₁.h
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
A : UniformInducing ↑(equiv p β)
i : PiLp p β × PiLp p β
x✝ : ι
⊢ Prod.fst (↑(equiv p β) i.fst, ↑(equiv p β) i.snd) x✝ = Prod.fst (id i) x✝
[PROOFSTEP]
rfl
[GOAL]
case h.h₂.h
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
A : UniformInducing ↑(equiv p β)
i : PiLp p β × PiLp p β
x✝ : ι
⊢ Prod.snd (↑(equiv p β) i.fst, ↑(equiv p β) i.snd) x✝ = Prod.snd (id i) x✝
[PROOFSTEP]
rfl
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
A : UniformInducing ↑(equiv p β)
this : (fun x => (↑(equiv p β) x.fst, ↑(equiv p β) x.snd)) = id
⊢ 𝓤 (PiLp p β) = 𝓤 ((i : ι) → β i)
[PROOFSTEP]
rw [← A.comap_uniformity, this, comap_id]
[GOAL]
p✝ : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝³ : Fintype ι
inst✝² : Fact (1 ≤ p✝)
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_6
inst✝ : (i : ι) → PseudoMetricSpace (β i)
hp : p ≠ ⊤
x y : PiLp p β
⊢ ↑(nndist x y) = ↑((∑ i : ι, nndist (x i) (y i) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p))
[PROOFSTEP]
push_cast
[GOAL]
p✝ : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝³ : Fintype ι
inst✝² : Fact (1 ≤ p✝)
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_6
inst✝ : (i : ι) → PseudoMetricSpace (β i)
hp : p ≠ ⊤
x y : PiLp p β
⊢ dist x y = (∑ x_1 : ι, dist (x x_1) (y x_1) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
[PROOFSTEP]
exact dist_eq_sum (p.toReal_pos_iff_ne_top.mpr hp) _ _
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_6
inst✝ : (i : ι) → PseudoMetricSpace (β i)
x y : PiLp ⊤ β
⊢ ↑(nndist x y) = ↑(⨆ (i : ι), nndist (x i) (y i))
[PROOFSTEP]
push_cast
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_6
inst✝ : (i : ι) → PseudoMetricSpace (β i)
x y : PiLp ⊤ β
⊢ dist x y = ⨆ (i : ι), dist (x i) (y i)
[PROOFSTEP]
exact dist_eq_iSup _ _
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
x y : PiLp ⊤ β
⊢ edist (↑(equiv ⊤ β) x) (↑(equiv ⊤ β) y) ≤ edist x y
[PROOFSTEP]
simpa only [ENNReal.coe_one, one_mul] using lipschitzWith_equiv ∞ β x y
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
inst✝ : (i : ι) → PseudoEMetricSpace (β i)
x y : PiLp ⊤ β
⊢ edist x y ≤ edist (↑(equiv ⊤ β) x) (↑(equiv ⊤ β) y)
[PROOFSTEP]
simpa only [ENNReal.div_top, ENNReal.zero_toReal, NNReal.rpow_zero, ENNReal.coe_one, one_mul] using
  antilipschitzWith_equiv ∞ β x y
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
src✝ : AddCommGroup ((i : ι) → β i) := Pi.addCommGroup
x y : PiLp p β
⊢ dist x y = ‖x - y‖
[PROOFSTEP]
rcases p.dichotomy with (rfl | h)
[GOAL]
case inl
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
src✝ : AddCommGroup ((i : ι) → β i) := Pi.addCommGroup
inst✝ : Fact (1 ≤ ⊤)
x y : PiLp ⊤ β
⊢ dist x y = ‖x - y‖
[PROOFSTEP]
simp only [dist_eq_iSup, norm_eq_ciSup, dist_eq_norm]
  -- Porting note: added
[GOAL]
case inl
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
src✝ : AddCommGroup ((i : ι) → β i) := Pi.addCommGroup
inst✝ : Fact (1 ≤ ⊤)
x y : PiLp ⊤ β
⊢ ⨆ (i : ι), ‖x i - y i‖ = ⨆ (i : ι), ‖(x - y) i‖
[PROOFSTEP]
congr
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
src✝ : AddCommGroup ((i : ι) → β i) := Pi.addCommGroup
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
⊢ dist x y = ‖x - y‖
[PROOFSTEP]
have : p ≠ ∞ := by
  intro hp
  rw [hp, ENNReal.top_toReal] at h 
  linarith
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
src✝ : AddCommGroup ((i : ι) → β i) := Pi.addCommGroup
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
⊢ p ≠ ⊤
[PROOFSTEP]
intro hp
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
src✝ : AddCommGroup ((i : ι) → β i) := Pi.addCommGroup
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
hp : p = ⊤
⊢ False
[PROOFSTEP]
rw [hp, ENNReal.top_toReal] at h 
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
src✝ : AddCommGroup ((i : ι) → β i) := Pi.addCommGroup
x y : PiLp p β
h : 1 ≤ 0
hp : p = ⊤
⊢ False
[PROOFSTEP]
linarith
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
src✝ : AddCommGroup ((i : ι) → β i) := Pi.addCommGroup
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
this : p ≠ ⊤
⊢ dist x y = ‖x - y‖
[PROOFSTEP]
simp only [dist_eq_sum (zero_lt_one.trans_le h), norm_eq_sum (zero_lt_one.trans_le h), dist_eq_norm]
  -- Porting note: added
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
src✝ : AddCommGroup ((i : ι) → β i) := Pi.addCommGroup
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
this : p ≠ ⊤
⊢ (∑ x_1 : ι, ‖x x_1 - y x_1‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p) =
    (∑ i : ι, ‖(x - y) i‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
[PROOFSTEP]
congr
[GOAL]
p✝ : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝³ : Fintype ι
inst✝² : Fact (1 ≤ p✝)
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_6
hp : p ≠ ⊤
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp p β
⊢ ‖f‖₊ = (∑ i : ι, ‖f i‖₊ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
[PROOFSTEP]
ext
[GOAL]
case a
p✝ : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝³ : Fintype ι
inst✝² : Fact (1 ≤ p✝)
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_6
hp : p ≠ ⊤
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp p β
⊢ ↑‖f‖₊ = ↑((∑ i : ι, ‖f i‖₊ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p))
[PROOFSTEP]
simp [NNReal.coe_sum, norm_eq_sum (p.toReal_pos_iff_ne_top.mpr hp)]
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_6
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp ⊤ β
⊢ ‖f‖₊ = ⨆ (i : ι), ‖f i‖₊
[PROOFSTEP]
ext
[GOAL]
case a
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_6
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
f : PiLp ⊤ β
⊢ ↑‖f‖₊ = ↑(⨆ (i : ι), ‖f i‖₊)
[PROOFSTEP]
simp [NNReal.coe_iSup, norm_eq_ciSup]
[GOAL]
p✝ : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝³ : Fintype ι
inst✝² : Fact (1 ≤ p✝)
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_6
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
n : ℕ
h : p = ↑n
f : PiLp p β
⊢ ‖f‖ = (∑ i : ι, ‖f i‖ ^ n) ^ (1 / ↑n)
[PROOFSTEP]
have := p.toReal_pos_iff_ne_top.mpr (ne_of_eq_of_ne h <| ENNReal.nat_ne_top n)
[GOAL]
p✝ : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝³ : Fintype ι
inst✝² : Fact (1 ≤ p✝)
p : ℝ≥0∞
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_6
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
n : ℕ
h : p = ↑n
f : PiLp p β
this : 0 < ENNReal.toReal p
⊢ ‖f‖ = (∑ i : ι, ‖f i‖ ^ n) ^ (1 / ↑n)
[PROOFSTEP]
simp only [one_div, h, Real.rpow_nat_cast, ENNReal.toReal_nat, eq_self_iff_true, Finset.sum_congr, norm_eq_sum this]
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_6
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ‖x‖ = Real.sqrt (∑ i : ι, ‖x i‖ ^ 2)
[PROOFSTEP]
rw [norm_eq_of_nat 2 (by norm_cast) _]
  -- Porting note: was `convert`
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_6
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ 2 = ↑2
[PROOFSTEP]
norm_cast
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_6
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ (∑ i : ι, ‖x i‖ ^ 2) ^ (1 / ↑2) = Real.sqrt (∑ i : ι, ‖x i‖ ^ 2)
[PROOFSTEP]
rw [Real.sqrt_eq_rpow]
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_6
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ (∑ i : ι, ‖x i‖ ^ 2) ^ (1 / ↑2) = (∑ i : ι, ‖x i‖ ^ 2) ^ (1 / 2)
[PROOFSTEP]
norm_cast
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_6
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ↑‖x‖₊ = ↑(↑NNReal.sqrt (∑ i : ι, ‖x i‖₊ ^ 2))
[PROOFSTEP]
push_cast
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_6
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ‖x‖ = Real.sqrt (∑ x_1 : ι, ‖x x_1‖ ^ 2)
[PROOFSTEP]
exact norm_eq_of_L2 x
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_6
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ‖x‖ ^ 2 = ∑ i : ι, ‖x i‖ ^ 2
[PROOFSTEP]
suffices ‖x‖₊ ^ 2 = ∑ i : ι, ‖x i‖₊ ^ 2 by simpa only [NNReal.coe_sum] using congr_arg ((↑) : ℝ≥0 → ℝ) this
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_6
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
this : ‖x‖₊ ^ 2 = ∑ i : ι, ‖x i‖₊ ^ 2
⊢ ‖x‖ ^ 2 = ∑ i : ι, ‖x i‖ ^ 2
[PROOFSTEP]
simpa only [NNReal.coe_sum] using congr_arg ((↑) : ℝ≥0 → ℝ) this
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_6
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x : PiLp 2 β
⊢ ‖x‖₊ ^ 2 = ∑ i : ι, ‖x i‖₊ ^ 2
[PROOFSTEP]
rw [nnnorm_eq_of_L2, NNReal.sq_sqrt]
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_6
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
⊢ dist x y = Real.sqrt (∑ i : ι, dist (x i) (y i) ^ 2)
[PROOFSTEP]
simp_rw [dist_eq_norm, norm_eq_of_L2]
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_6
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
⊢ Real.sqrt (∑ i : ι, ‖(x - y) i‖ ^ 2) = Real.sqrt (∑ x_1 : ι, ‖x x_1 - y x_1‖ ^ 2)
[PROOFSTEP]
rfl
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_6
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
⊢ ↑(nndist x y) = ↑(↑NNReal.sqrt (∑ i : ι, nndist (x i) (y i) ^ 2))
[PROOFSTEP]
push_cast
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_6
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
⊢ dist x y = Real.sqrt (∑ x_1 : ι, dist (x x_1) (y x_1) ^ 2)
[PROOFSTEP]
exact dist_eq_of_L2 _ _
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝² : Fintype ι
inst✝¹ : Fact (1 ≤ p)
β : ι → Type u_6
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 2 β
⊢ edist x y = (∑ i : ι, edist (x i) (y i) ^ 2) ^ (1 / 2)
[PROOFSTEP]
simp [PiLp.edist_eq_sum]
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁵ : Fintype ι
inst✝⁴ : Fact (1 ≤ p)
inst✝³ : NormedField 𝕜
inst✝² : NormedField 𝕜'
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
f : PiLp p β
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
[PROOFSTEP]
rcases p.dichotomy with (rfl | hp)
[GOAL]
case inl
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁵ : Fintype ι
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
inst✝ : Fact (1 ≤ ⊤)
f : PiLp ⊤ β
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
[PROOFSTEP]
letI : Module 𝕜 (PiLp ∞ β) := Pi.module ι β 𝕜
[GOAL]
case inl
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁵ : Fintype ι
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
inst✝ : Fact (1 ≤ ⊤)
f : PiLp ⊤ β
this : Module 𝕜 (PiLp ⊤ β) := Pi.module ι β 𝕜
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
[PROOFSTEP]
suffices ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊ by exact_mod_cast NNReal.coe_mono this.le
[GOAL]
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁵ : Fintype ι
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
inst✝ : Fact (1 ≤ ⊤)
f : PiLp ⊤ β
this✝ : Module 𝕜 (PiLp ⊤ β) := Pi.module ι β 𝕜
this : ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
[PROOFSTEP]
exact_mod_cast NNReal.coe_mono this.le
[GOAL]
case inl
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁵ : Fintype ι
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
inst✝ : Fact (1 ≤ ⊤)
f : PiLp ⊤ β
this : Module 𝕜 (PiLp ⊤ β) := Pi.module ι β 𝕜
⊢ ‖c • f‖₊ = ‖c‖₊ * ‖f‖₊
[PROOFSTEP]
simp only [nnnorm_eq_ciSup, NNReal.mul_iSup, ← nnnorm_smul]
  -- Porting note: added
[GOAL]
case inl
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁵ : Fintype ι
inst✝⁴ : NormedField 𝕜
inst✝³ : NormedField 𝕜'
inst✝² : (i : ι) → SeminormedAddCommGroup (β i)
inst✝¹ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
inst✝ : Fact (1 ≤ ⊤)
f : PiLp ⊤ β
this : Module 𝕜 (PiLp ⊤ β) := Pi.module ι β 𝕜
⊢ ⨆ (i : ι), ‖(c • f) i‖₊ = ⨆ (i : ι), ‖c • f i‖₊
[PROOFSTEP]
congr
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁵ : Fintype ι
inst✝⁴ : Fact (1 ≤ p)
inst✝³ : NormedField 𝕜
inst✝² : NormedField 𝕜'
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ ENNReal.toReal p
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
[PROOFSTEP]
have : p.toReal * (1 / p.toReal) = 1 := mul_div_cancel' 1 (zero_lt_one.trans_le hp).ne'
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁵ : Fintype ι
inst✝⁴ : Fact (1 ≤ p)
inst✝³ : NormedField 𝕜
inst✝² : NormedField 𝕜'
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ ENNReal.toReal p
this : ENNReal.toReal p * (1 / ENNReal.toReal p) = 1
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
[PROOFSTEP]
have smul_apply : ∀ i : ι, (c • f) i = c • (f i) := fun i => rfl
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁵ : Fintype ι
inst✝⁴ : Fact (1 ≤ p)
inst✝³ : NormedField 𝕜
inst✝² : NormedField 𝕜'
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ ENNReal.toReal p
this : ENNReal.toReal p * (1 / ENNReal.toReal p) = 1
smul_apply : ∀ (i : ι), (c • f) i = c • f i
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
[PROOFSTEP]
simp only [norm_eq_sum (zero_lt_one.trans_le hp), norm_smul, Real.mul_rpow, norm_nonneg, ← Finset.mul_sum, smul_apply]
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁵ : Fintype ι
inst✝⁴ : Fact (1 ≤ p)
inst✝³ : NormedField 𝕜
inst✝² : NormedField 𝕜'
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ ENNReal.toReal p
this : ENNReal.toReal p * (1 / ENNReal.toReal p) = 1
smul_apply : ∀ (i : ι), (c • f) i = c • f i
⊢ (‖c‖ ^ ENNReal.toReal p * ∑ x : ι, ‖f x‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p) ≤
    ‖c‖ * (∑ x : ι, ‖f x‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
[PROOFSTEP]
rw [mul_rpow (rpow_nonneg_of_nonneg (norm_nonneg _) _), ← rpow_mul (norm_nonneg _), this, Real.rpow_one]
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁵ : Fintype ι
inst✝⁴ : Fact (1 ≤ p)
inst✝³ : NormedField 𝕜
inst✝² : NormedField 𝕜'
inst✝¹ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
f : PiLp p β
hp : 1 ≤ ENNReal.toReal p
this : ENNReal.toReal p * (1 / ENNReal.toReal p) = 1
smul_apply : ∀ (i : ι), (c • f) i = c • f i
⊢ 0 ≤ ∑ x : ι, ‖f x‖ ^ ENNReal.toReal p
[PROOFSTEP]
exact Finset.sum_nonneg fun i _ => rpow_nonneg_of_nonneg (norm_nonneg _) _
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
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 : ι
src✝ : PiLp ⊤ β ≃ ((i : ι) → β i) := equiv ⊤ β
f : PiLp ⊤ β
⊢ ‖↑{
            toLinearMap :=
              {
                toAddHom :=
                  { toFun := src✝.toFun,
                    map_add' := (_ : ∀ (f g : PiLp ⊤ β), Equiv.toFun src✝ (f + g) = Equiv.toFun src✝ (f + g)) },
                map_smul' :=
                  (_ :
                    ∀ (c : 𝕜) (f : PiLp ⊤ β),
                      AddHom.toFun
                          { toFun := src✝.toFun,
                            map_add' := (_ : ∀ (f g : PiLp ⊤ β), Equiv.toFun src✝ (f + g) = Equiv.toFun src✝ (f + g)) }
                          (c • f) =
                        AddHom.toFun
                          { toFun := src✝.toFun,
                            map_add' := (_ : ∀ (f g : PiLp ⊤ β), Equiv.toFun src✝ (f + g) = Equiv.toFun src✝ (f + g)) }
                          (c • f)) },
            invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        f‖ =
    ‖f‖
[PROOFSTEP]
suffices (Finset.univ.sup fun i => ‖f i‖₊) = ⨆ i, ‖f i‖₊ by
  simpa only [NNReal.coe_iSup] using congr_arg ((↑) : ℝ≥0 → ℝ) this
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
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 : ι
src✝ : PiLp ⊤ β ≃ ((i : ι) → β i) := equiv ⊤ β
f : PiLp ⊤ β
this : (Finset.sup Finset.univ fun i => ‖f i‖₊) = ⨆ (i : ι), ‖f i‖₊
⊢ ‖↑{
            toLinearMap :=
              {
                toAddHom :=
                  { toFun := src✝.toFun,
                    map_add' := (_ : ∀ (f g : PiLp ⊤ β), Equiv.toFun src✝ (f + g) = Equiv.toFun src✝ (f + g)) },
                map_smul' :=
                  (_ :
                    ∀ (c : 𝕜) (f : PiLp ⊤ β),
                      AddHom.toFun
                          { toFun := src✝.toFun,
                            map_add' := (_ : ∀ (f g : PiLp ⊤ β), Equiv.toFun src✝ (f + g) = Equiv.toFun src✝ (f + g)) }
                          (c • f) =
                        AddHom.toFun
                          { toFun := src✝.toFun,
                            map_add' := (_ : ∀ (f g : PiLp ⊤ β), Equiv.toFun src✝ (f + g) = Equiv.toFun src✝ (f + g)) }
                          (c • f)) },
            invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        f‖ =
    ‖f‖
[PROOFSTEP]
simpa only [NNReal.coe_iSup] using congr_arg ((↑) : ℝ≥0 → ℝ) this
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
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 : ι
src✝ : PiLp ⊤ β ≃ ((i : ι) → β i) := equiv ⊤ β
f : PiLp ⊤ β
⊢ (Finset.sup Finset.univ fun i => ‖f i‖₊) = ⨆ (i : ι), ‖f i‖₊
[PROOFSTEP]
refine' antisymm (Finset.sup_le fun i _ => le_ciSup (Fintype.bddAbove_range fun i => ‖f i‖₊) _) _
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
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 : ι
src✝ : PiLp ⊤ β ≃ ((i : ι) → β i) := equiv ⊤ β
f : PiLp ⊤ β
⊢ ⨆ (i : ι), ‖f i‖₊ ≤ Finset.sup Finset.univ fun i => ‖f i‖₊
[PROOFSTEP]
cases isEmpty_or_nonempty ι
[GOAL]
case inl
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
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 : ι
src✝ : PiLp ⊤ β ≃ ((i : ι) → β i) := equiv ⊤ β
f : PiLp ⊤ β
h✝ : IsEmpty ι
⊢ ⨆ (i : ι), ‖f i‖₊ ≤ Finset.sup Finset.univ fun i => ‖f i‖₊
[PROOFSTEP]
simp only [ciSup_of_empty, Finset.univ_eq_empty, Finset.sup_empty, le_rfl]
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
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 : ι
src✝ : PiLp ⊤ β ≃ ((i : ι) → β i) := equiv ⊤ β
f : PiLp ⊤ β
h✝ : Nonempty ι
⊢ ⨆ (i : ι), ‖f i‖₊ ≤ Finset.sup Finset.univ fun i => ‖f i‖₊
[PROOFSTEP]
exact ciSup_le fun i => Finset.le_sup (f := fun k => ‖f k‖₊) (Finset.mem_univ i)
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
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_6
inst✝² : Fintype ι'
E : Type u_7
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
e : ι ≃ ι'
x' : PiLp p fun x => E
⊢ ‖↑(LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e) x'‖ = ‖x'‖
[PROOFSTEP]
clear x y
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁸ : Fintype ι
inst✝⁷ : Fact (1 ≤ p)
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedField 𝕜'
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x'✝ y' : (i : ι) → β i
i : ι
ι' : Type u_6
inst✝² : Fintype ι'
E : Type u_7
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
e : ι ≃ ι'
x' : PiLp p fun x => E
⊢ ‖↑(LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e) x'‖ = ‖x'‖
[PROOFSTEP]
rcases p.dichotomy with (rfl | h)
[GOAL]
case inl
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁸ : Fintype ι
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x'✝ y' : (i : ι) → β i
i : ι
ι' : Type u_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
e : ι ≃ ι'
inst✝ : Fact (1 ≤ ⊤)
x' : PiLp ⊤ fun x => E
⊢ ‖↑(LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e) x'‖ = ‖x'‖
[PROOFSTEP]
simp_rw [norm_eq_ciSup]
[GOAL]
case inl
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁸ : Fintype ι
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x'✝ y' : (i : ι) → β i
i : ι
ι' : Type u_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
e : ι ≃ ι'
inst✝ : Fact (1 ≤ ⊤)
x' : PiLp ⊤ fun x => E
⊢ ⨆ (i : ι'), ‖↑(LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e) x' i‖ = ⨆ (i : ι), ‖x' i‖
[PROOFSTEP]
exact e.symm.iSup_congr fun _ => rfl
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁸ : Fintype ι
inst✝⁷ : Fact (1 ≤ p)
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedField 𝕜'
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x'✝ y' : (i : ι) → β i
i : ι
ι' : Type u_6
inst✝² : Fintype ι'
E : Type u_7
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
e : ι ≃ ι'
x' : PiLp p fun x => E
h : 1 ≤ ENNReal.toReal p
⊢ ‖↑(LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e) x'‖ = ‖x'‖
[PROOFSTEP]
simp only [norm_eq_sum (zero_lt_one.trans_le h)]
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁸ : Fintype ι
inst✝⁷ : Fact (1 ≤ p)
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedField 𝕜'
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x'✝ y' : (i : ι) → β i
i : ι
ι' : Type u_6
inst✝² : Fintype ι'
E : Type u_7
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
e : ι ≃ ι'
x' : PiLp p fun x => E
h : 1 ≤ ENNReal.toReal p
⊢ (∑ x : ι', ‖↑(LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e) x' x‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p) =
    (∑ x : ι, ‖x' x‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
[PROOFSTEP]
congr 1
[GOAL]
case inr.e_a
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁸ : Fintype ι
inst✝⁷ : Fact (1 ≤ p)
inst✝⁶ : NormedField 𝕜
inst✝⁵ : NormedField 𝕜'
inst✝⁴ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x'✝ y' : (i : ι) → β i
i : ι
ι' : Type u_6
inst✝² : Fintype ι'
E : Type u_7
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
e : ι ≃ ι'
x' : PiLp p fun x => E
h : 1 ≤ ENNReal.toReal p
⊢ ∑ x : ι', ‖↑(LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e) x' x‖ ^ ENNReal.toReal p = ∑ x : ι, ‖x' x‖ ^ ENNReal.toReal p
[PROOFSTEP]
exact Fintype.sum_equiv e.symm _ _ fun _ => rfl
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
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_6
inst✝² : Fintype ι'
E : Type u_7
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
e : ι ≃ ι'
z : PiLp p fun x => E
⊢ ↑(LinearIsometryEquiv.symm (LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e)) z =
    ↑(LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e.symm) z
[PROOFSTEP]
simp only [LinearIsometryEquiv.piLpCongrLeft, LinearIsometryEquiv.symm, LinearIsometryEquiv.coe_mk]
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
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_6
inst✝² : Fintype ι'
E : Type u_7
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
e : ι ≃ ι'
z : PiLp p fun x => E
⊢ ↑(LinearEquiv.symm (LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e)) z =
    ↑(LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e.symm) z
[PROOFSTEP]
unfold PiLp WithLp
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
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_6
inst✝² : Fintype ι'
E : Type u_7
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
e : ι ≃ ι'
z : PiLp p fun x => E
⊢ ↑(LinearEquiv.symm (LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e)) z =
    ↑(LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e.symm) z
[PROOFSTEP]
ext
[GOAL]
case h
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
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_6
inst✝² : Fintype ι'
E : Type u_7
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
e : ι ≃ ι'
z : PiLp p fun x => E
x✝ : ι
⊢ ↑(LinearEquiv.symm (LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e)) z x✝ =
    ↑(LinearEquiv.piCongrLeft' 𝕜 (fun x => E) e.symm) z x✝
[PROOFSTEP]
simp only [LinearEquiv.piCongrLeft'_symm_apply, eq_rec_constant, LinearEquiv.piCongrLeft'_apply, Equiv.symm_symm_apply]
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
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_6
inst✝⁴ : Fintype ι'
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
e : ι ≃ ι'
i : ι
v : E
⊢ ↑(LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e) (↑(equiv p fun x => E).symm (Pi.single i v)) =
    ↑(equiv p fun x => E).symm (Pi.single (↑e i) v)
[PROOFSTEP]
funext x
[GOAL]
case h
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
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_6
inst✝⁴ : Fintype ι'
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq ι'
e : ι ≃ ι'
i : ι
v : E
x : ι'
⊢ ↑(LinearIsometryEquiv.piLpCongrLeft p 𝕜 E e) (↑(equiv p fun x => E).symm (Pi.single i v)) x =
    ↑(equiv p fun x => E).symm (Pi.single (↑e i) v) x
[PROOFSTEP]
simp [LinearIsometryEquiv.piLpCongrLeft_apply, LinearEquiv.piCongrLeft', Equiv.piCongrLeft', Pi.single, Function.update,
  Equiv.symm_apply_eq]
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
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_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : DecidableEq ι
hp : Fact (1 ≤ p)
i : ι
b : β i
⊢ ‖↑(equiv p β).symm (Pi.single i b)‖₊ = ‖b‖₊
[PROOFSTEP]
clear x y
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁹ : Fintype ι
inst✝⁸ : Fact (1 ≤ p)
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x' y' : (i : ι) → β i
i✝ : ι
ι' : Type u_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : DecidableEq ι
hp : Fact (1 ≤ p)
i : ι
b : β i
⊢ ‖↑(equiv p β).symm (Pi.single i b)‖₊ = ‖b‖₊
[PROOFSTEP]
haveI : Nonempty ι := ⟨i⟩
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁹ : Fintype ι
inst✝⁸ : Fact (1 ≤ p)
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x' y' : (i : ι) → β i
i✝ : ι
ι' : Type u_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : DecidableEq ι
hp : Fact (1 ≤ p)
i : ι
b : β i
this : Nonempty ι
⊢ ‖↑(equiv p β).symm (Pi.single i b)‖₊ = ‖b‖₊
[PROOFSTEP]
induction p using ENNReal.recTopCoe generalizing hp with
| top =>
  simp_rw [nnnorm_eq_ciSup, equiv_symm_apply]
  refine' ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j => _) fun n hn => ⟨i, hn.trans_eq _⟩
  · obtain rfl | hij := Decidable.eq_or_ne i j
    · rw [Pi.single_eq_same]
    · rw [Pi.single_eq_of_ne' hij, nnnorm_zero]
      exact zero_le _
  · rw [Pi.single_eq_same]
|
  coe p =>
  have hp0 : (p : ℝ) ≠ 0 := by exact_mod_cast (zero_lt_one.trans_le <| Fact.out (p := 1 ≤ (p : ℝ≥0∞))).ne'
  rw [nnnorm_eq_sum ENNReal.coe_ne_top, ENNReal.coe_toReal, Fintype.sum_eq_single i, equiv_symm_apply,
    Pi.single_eq_same, ← NNReal.rpow_mul, one_div, mul_inv_cancel hp0, NNReal.rpow_one]
  intro j hij
  rw [equiv_symm_apply, Pi.single_eq_of_ne hij, nnnorm_zero, NNReal.zero_rpow hp0]
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁹ : Fintype ι
inst✝⁸ : Fact (1 ≤ p)
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x' y' : (i : ι) → β i
i✝ : ι
ι' : Type u_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : DecidableEq ι
hp : Fact (1 ≤ p)
i : ι
b : β i
this : Nonempty ι
⊢ ‖↑(equiv p β).symm (Pi.single i b)‖₊ = ‖b‖₊
[PROOFSTEP]
induction p using ENNReal.recTopCoe generalizing hp with
| top =>
  simp_rw [nnnorm_eq_ciSup, equiv_symm_apply]
  refine' ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j => _) fun n hn => ⟨i, hn.trans_eq _⟩
  · obtain rfl | hij := Decidable.eq_or_ne i j
    · rw [Pi.single_eq_same]
    · rw [Pi.single_eq_of_ne' hij, nnnorm_zero]
      exact zero_le _
  · rw [Pi.single_eq_same]
|
  coe p =>
  have hp0 : (p : ℝ) ≠ 0 := by exact_mod_cast (zero_lt_one.trans_le <| Fact.out (p := 1 ≤ (p : ℝ≥0∞))).ne'
  rw [nnnorm_eq_sum ENNReal.coe_ne_top, ENNReal.coe_toReal, Fintype.sum_eq_single i, equiv_symm_apply,
    Pi.single_eq_same, ← NNReal.rpow_mul, one_div, mul_inv_cancel hp0, NNReal.rpow_one]
  intro j hij
  rw [equiv_symm_apply, Pi.single_eq_of_ne hij, nnnorm_zero, NNReal.zero_rpow hp0]
[GOAL]
case top
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁹ : Fintype ι
inst✝⁸ : Fact (1 ≤ p)
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x' y' : (i : ι) → β i
i✝ : ι
ι' : Type u_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (1 ≤ ⊤)
⊢ ‖↑(equiv ⊤ β).symm (Pi.single i b)‖₊ = ‖b‖₊
[PROOFSTEP]

| top =>
  simp_rw [nnnorm_eq_ciSup, equiv_symm_apply]
  refine' ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j => _) fun n hn => ⟨i, hn.trans_eq _⟩
  · obtain rfl | hij := Decidable.eq_or_ne i j
    · rw [Pi.single_eq_same]
    · rw [Pi.single_eq_of_ne' hij, nnnorm_zero]
      exact zero_le _
  · rw [Pi.single_eq_same]
[GOAL]
case top
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁹ : Fintype ι
inst✝⁸ : Fact (1 ≤ p)
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x' y' : (i : ι) → β i
i✝ : ι
ι' : Type u_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (1 ≤ ⊤)
⊢ ‖↑(equiv ⊤ β).symm (Pi.single i b)‖₊ = ‖b‖₊
[PROOFSTEP]
simp_rw [nnnorm_eq_ciSup, equiv_symm_apply]
[GOAL]
case top
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁹ : Fintype ι
inst✝⁸ : Fact (1 ≤ p)
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x' y' : (i : ι) → β i
i✝ : ι
ι' : Type u_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (1 ≤ ⊤)
⊢ ⨆ (i_1 : ι), ‖Pi.single i b i_1‖₊ = ‖b‖₊
[PROOFSTEP]
refine' ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j => _) fun n hn => ⟨i, hn.trans_eq _⟩
[GOAL]
case top.refine'_1
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁹ : Fintype ι
inst✝⁸ : Fact (1 ≤ p)
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x' y' : (i : ι) → β i
i✝ : ι
ι' : Type u_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (1 ≤ ⊤)
j : ι
⊢ ‖Pi.single i b j‖₊ ≤ ‖b‖₊
[PROOFSTEP]
obtain rfl | hij := Decidable.eq_or_ne i j
[GOAL]
case top.refine'_1.inl
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁹ : Fintype ι
inst✝⁸ : Fact (1 ≤ p)
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x' y' : (i : ι) → β i
i✝ : ι
ι' : Type u_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (1 ≤ ⊤)
⊢ ‖Pi.single i b i‖₊ ≤ ‖b‖₊
[PROOFSTEP]
rw [Pi.single_eq_same]
[GOAL]
case top.refine'_1.inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁹ : Fintype ι
inst✝⁸ : Fact (1 ≤ p)
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x' y' : (i : ι) → β i
i✝ : ι
ι' : Type u_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (1 ≤ ⊤)
j : ι
hij : i ≠ j
⊢ ‖Pi.single i b j‖₊ ≤ ‖b‖₊
[PROOFSTEP]
rw [Pi.single_eq_of_ne' hij, nnnorm_zero]
[GOAL]
case top.refine'_1.inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁹ : Fintype ι
inst✝⁸ : Fact (1 ≤ p)
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x' y' : (i : ι) → β i
i✝ : ι
ι' : Type u_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (1 ≤ ⊤)
j : ι
hij : i ≠ j
⊢ 0 ≤ ‖b‖₊
[PROOFSTEP]
exact zero_le _
[GOAL]
case top.refine'_2
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁹ : Fintype ι
inst✝⁸ : Fact (1 ≤ p)
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x' y' : (i : ι) → β i
i✝ : ι
ι' : Type u_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
hp : Fact (1 ≤ ⊤)
n : ℝ≥0
hn : n < ‖b‖₊
⊢ ‖b‖₊ = ‖Pi.single i b i‖₊
[PROOFSTEP]
rw [Pi.single_eq_same]
[GOAL]
case coe
p✝ : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁹ : Fintype ι
inst✝⁸ : Fact (1 ≤ p✝)
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x' y' : (i : ι) → β i
i✝ : ι
ι' : Type u_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
⊢ ‖↑(equiv (↑p) β).symm (Pi.single i b)‖₊ = ‖b‖₊
[PROOFSTEP]

|
  coe p =>
  have hp0 : (p : ℝ) ≠ 0 := by exact_mod_cast (zero_lt_one.trans_le <| Fact.out (p := 1 ≤ (p : ℝ≥0∞))).ne'
  rw [nnnorm_eq_sum ENNReal.coe_ne_top, ENNReal.coe_toReal, Fintype.sum_eq_single i, equiv_symm_apply,
    Pi.single_eq_same, ← NNReal.rpow_mul, one_div, mul_inv_cancel hp0, NNReal.rpow_one]
  intro j hij
  rw [equiv_symm_apply, Pi.single_eq_of_ne hij, nnnorm_zero, NNReal.zero_rpow hp0]
[GOAL]
case coe
p✝ : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁹ : Fintype ι
inst✝⁸ : Fact (1 ≤ p✝)
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x' y' : (i : ι) → β i
i✝ : ι
ι' : Type u_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
⊢ ‖↑(equiv (↑p) β).symm (Pi.single i b)‖₊ = ‖b‖₊
[PROOFSTEP]
have hp0 : (p : ℝ) ≠ 0 := by exact_mod_cast (zero_lt_one.trans_le <| Fact.out (p := 1 ≤ (p : ℝ≥0∞))).ne'
[GOAL]
p✝ : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁹ : Fintype ι
inst✝⁸ : Fact (1 ≤ p✝)
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x' y' : (i : ι) → β i
i✝ : ι
ι' : Type u_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
⊢ ↑p ≠ 0
[PROOFSTEP]
exact_mod_cast (zero_lt_one.trans_le <| Fact.out (p := 1 ≤ (p : ℝ≥0∞))).ne'
[GOAL]
case coe
p✝ : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁹ : Fintype ι
inst✝⁸ : Fact (1 ≤ p✝)
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x' y' : (i : ι) → β i
i✝ : ι
ι' : Type u_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
hp0 : ↑p ≠ 0
⊢ ‖↑(equiv (↑p) β).symm (Pi.single i b)‖₊ = ‖b‖₊
[PROOFSTEP]
rw [nnnorm_eq_sum ENNReal.coe_ne_top, ENNReal.coe_toReal, Fintype.sum_eq_single i, equiv_symm_apply, Pi.single_eq_same,
  ← NNReal.rpow_mul, one_div, mul_inv_cancel hp0, NNReal.rpow_one]
[GOAL]
case coe
p✝ : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁹ : Fintype ι
inst✝⁸ : Fact (1 ≤ p✝)
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x' y' : (i : ι) → β i
i✝ : ι
ι' : Type u_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
hp0 : ↑p ≠ 0
⊢ ∀ (x : ι), x ≠ i → ‖↑(equiv (↑p) β).symm (Pi.single i b) x‖₊ ^ ↑p = 0
[PROOFSTEP]
intro j hij
[GOAL]
case coe
p✝ : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝⁹ : Fintype ι
inst✝⁸ : Fact (1 ≤ p✝)
inst✝⁷ : NormedField 𝕜
inst✝⁶ : NormedField 𝕜'
inst✝⁵ : (i : ι) → SeminormedAddCommGroup (β i)
inst✝⁴ : (i : ι) → NormedSpace 𝕜 (β i)
c : 𝕜
x' y' : (i : ι) → β i
i✝ : ι
ι' : Type u_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : DecidableEq ι
i : ι
b : β i
this : Nonempty ι
p : ℝ≥0
hp : Fact (1 ≤ ↑p)
hp0 : ↑p ≠ 0
j : ι
hij : j ≠ i
⊢ ‖↑(equiv (↑p) β).symm (Pi.single i b) j‖₊ ^ ↑p = 0
[PROOFSTEP]
rw [equiv_symm_apply, Pi.single_eq_of_ne hij, nnnorm_zero, NNReal.zero_rpow hp0]
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
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_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : DecidableEq ι
i : ι
b₁ b₂ : β i
⊢ nndist (↑(equiv p β).symm (Pi.single i b₁)) (↑(equiv p β).symm (Pi.single i b₂)) = nndist b₁ b₂
[PROOFSTEP]
rw [nndist_eq_nnnorm, nndist_eq_nnnorm, ← WithLp.equiv_symm_sub, ← Pi.single_sub, nnnorm_equiv_symm_single]
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
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_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : DecidableEq ι
i : ι
b₁ b₂ : β i
⊢ edist (↑(equiv p β).symm (Pi.single i b₁)) (↑(equiv p β).symm (Pi.single i b₂)) = edist b₁ b₂
[PROOFSTEP]
simp only [edist_nndist, nndist_equiv_symm_single_same p β i b₁ b₂]
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
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_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
β : Type u_8
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ⊤
b : β
⊢ ‖↑(equiv p fun x => β).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ ENNReal.toReal (1 / p) * ‖b‖₊
[PROOFSTEP]
rcases p.dichotomy with (h | h)
[GOAL]
case inl
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
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_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
β : Type u_8
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ⊤
b : β
h : p = ⊤
⊢ ‖↑(equiv p fun x => β).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ ENNReal.toReal (1 / p) * ‖b‖₊
[PROOFSTEP]
exact False.elim (hp h)
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
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_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
β : Type u_8
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ⊤
b : β
h : 1 ≤ ENNReal.toReal p
⊢ ‖↑(equiv p fun x => β).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ ENNReal.toReal (1 / p) * ‖b‖₊
[PROOFSTEP]
have ne_zero : p.toReal ≠ 0 := (zero_lt_one.trans_le h).ne'
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
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_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
β : Type u_8
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ⊤
b : β
h : 1 ≤ ENNReal.toReal p
ne_zero : ENNReal.toReal p ≠ 0
⊢ ‖↑(equiv p fun x => β).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ ENNReal.toReal (1 / p) * ‖b‖₊
[PROOFSTEP]
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]
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
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_6
inst✝⁴ : Fintype ι'
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
β : Type u_8
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Nonempty ι
b : β
⊢ ‖↑(equiv p fun x => β).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ ENNReal.toReal (1 / p) * ‖b‖₊
[PROOFSTEP]
clear x y
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝¹⁰ : Fintype ι
inst✝⁹ : Fact (1 ≤ p)
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedField 𝕜'
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (β✝ i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (β✝ i)
c : 𝕜
x' y' : (i : ι) → β✝ i
i : ι
ι' : Type u_6
inst✝⁴ : Fintype ι'
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
β : Type u_8
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Nonempty ι
b : β
⊢ ‖↑(equiv p fun x => β).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ ENNReal.toReal (1 / p) * ‖b‖₊
[PROOFSTEP]
rcases em <| p = ∞ with (rfl | hp)
[GOAL]
case inl
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝¹⁰ : Fintype ι
inst✝⁹ : NormedField 𝕜
inst✝⁸ : NormedField 𝕜'
inst✝⁷ : (i : ι) → SeminormedAddCommGroup (β✝ i)
inst✝⁶ : (i : ι) → NormedSpace 𝕜 (β✝ i)
c : 𝕜
x' y' : (i : ι) → β✝ i
i : ι
ι' : Type u_6
inst✝⁵ : Fintype ι'
E : Type u_7
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
β : Type u_8
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Nonempty ι
b : β
inst✝ : Fact (1 ≤ ⊤)
⊢ ‖↑(equiv ⊤ fun x => β).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ ENNReal.toReal (1 / ⊤) * ‖b‖₊
[PROOFSTEP]
simp only [equiv_symm_apply, ENNReal.div_top, ENNReal.zero_toReal, NNReal.rpow_zero, one_mul, nnnorm_eq_ciSup,
  Function.const_apply, ciSup_const]
[GOAL]
case inr
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
inst✝¹⁰ : Fintype ι
inst✝⁹ : Fact (1 ≤ p)
inst✝⁸ : NormedField 𝕜
inst✝⁷ : NormedField 𝕜'
inst✝⁶ : (i : ι) → SeminormedAddCommGroup (β✝ i)
inst✝⁵ : (i : ι) → NormedSpace 𝕜 (β✝ i)
c : 𝕜
x' y' : (i : ι) → β✝ i
i : ι
ι' : Type u_6
inst✝⁴ : Fintype ι'
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
β : Type u_8
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Nonempty ι
b : β
hp : ¬p = ⊤
⊢ ‖↑(equiv p fun x => β).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ ENNReal.toReal (1 / p) * ‖b‖₊
[PROOFSTEP]
exact nnnorm_equiv_symm_const hp b
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
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_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
β : Type u_8
inst✝ : SeminormedAddCommGroup β
hp : p ≠ ⊤
b : β
⊢ ↑(↑(Fintype.card ι) ^ ENNReal.toReal (1 / p) * ‖b‖₊) = ↑(↑(Fintype.card ι) ^ ENNReal.toReal (1 / p)) * ‖b‖
[PROOFSTEP]
simp
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β✝ : ι → Type u_5
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_6
inst✝⁴ : Fintype ι'
E : Type u_7
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
β : Type u_8
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Nonempty ι
b : β
⊢ ↑(↑(Fintype.card ι) ^ ENNReal.toReal (1 / p) * ‖b‖₊) = ↑(↑(Fintype.card ι) ^ ENNReal.toReal (1 / p)) * ‖b‖
[PROOFSTEP]
simp
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
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_6
inst✝³ : Fintype ι'
E : Type u_7
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : DecidableEq ι
i : ι
⊢ ↑(basisFun p 𝕜 ι) i = ↑(equiv p fun i => 𝕜).symm (Pi.single i 1)
[PROOFSTEP]
simp_rw [basisFun, Basis.coe_ofEquivFun, WithLp.linearEquiv_symm_apply, Pi.single]
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
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_6
inst✝² : Fintype ι'
E : Type u_7
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
b : Basis ι 𝕜 (PiLp p fun x => 𝕜)
A : Matrix ι ι 𝕜
⊢ Basis.toMatrix b ↑(basisFun p 𝕜 ι) * A = ↑of fun i j => ↑(↑b.repr (↑(equiv p fun i => 𝕜).symm (Aᵀ j))) i
[PROOFSTEP]
have := basis_toMatrix_basisFun_mul (b.map (PiLp.linearEquiv _ 𝕜 _)) A
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
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_6
inst✝² : Fintype ι'
E : Type u_7
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
b : Basis ι 𝕜 (PiLp p fun x => 𝕜)
A : Matrix ι ι 𝕜
this :
  Basis.toMatrix (Basis.map b (linearEquiv p 𝕜 fun x => 𝕜)) ↑(Pi.basisFun 𝕜 ι) * A =
    ↑of fun i j => ↑(↑(Basis.map b (linearEquiv p 𝕜 fun x => 𝕜)).repr (Aᵀ j)) i
⊢ Basis.toMatrix b ↑(basisFun p 𝕜 ι) * A = ↑of fun i j => ↑(↑b.repr (↑(equiv p fun i => 𝕜).symm (Aᵀ j))) i
[PROOFSTEP]
simp_rw [← PiLp.basisFun_map p, Basis.map_repr, LinearEquiv.trans_apply, WithLp.linearEquiv_symm_apply,
  Basis.toMatrix_map, Function.comp, Basis.map_apply, LinearEquiv.symm_apply_apply] at this 
[GOAL]
p : ℝ≥0∞
𝕜 : Type u_1
𝕜' : Type u_2
ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
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_6
inst✝² : Fintype ι'
E : Type u_7
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
b : Basis ι 𝕜 (PiLp p fun x => 𝕜)
A : Matrix ι ι 𝕜
this :
  (Basis.toMatrix b fun x => ↑(basisFun p 𝕜 ι) x) * A =
    ↑of fun i j => ↑(↑b.repr (↑(WithLp.equiv p (ι → 𝕜)).symm (Aᵀ j))) i
⊢ Basis.toMatrix b ↑(basisFun p 𝕜 ι) * A = ↑of fun i j => ↑(↑b.repr (↑(equiv p fun i => 𝕜).symm (Aᵀ j))) i
[PROOFSTEP]
exact this
