p : ℝ≥0∞
𝕜 : Type ?u.49389
𝕜' : Type ?u.49392
ι : Type u_1
α : ι → Type ?u.49400
β : ι → Type u_2
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
⊢ edist (↑(PiLp.equiv p β) x) (↑(PiLp.equiv p β) y) ≤ ↑1 * edist x y
p : ℝ≥0∞
𝕜 : Type ?u.49389
𝕜' : Type ?u.49392
ι : Type u_1
α : ι → Type ?u.49400
β : ι → Type u_2
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
⊢ LipschitzWith 1 ↑(PiLp.equiv p β)
intro x y
case inl
𝕜 : Type ?u.49389
𝕜' : Type ?u.49392
ι : Type u_1
α : ι → Type ?u.49400
β : ι → Type u_2
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ⊤)
x y : PiLp ⊤ β
⊢ edist (↑(PiLp.equiv ⊤ β) x) (↑(PiLp.equiv ⊤ β) y) ≤ ↑1 * edist x y

case inr
p : ℝ≥0∞
𝕜 : Type ?u.49389
𝕜' : Type ?u.49392
ι : Type u_1
α : ι → Type ?u.49400
β : ι → Type u_2
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
⊢ edist (↑(PiLp.equiv p β) x) (↑(PiLp.equiv p β) y) ≤ ↑1 * edist x y
p : ℝ≥0∞
𝕜 : Type ?u.49389
𝕜' : Type ?u.49392
ι : Type u_1
α : ι → Type ?u.49400
β : ι → Type u_2
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
⊢ edist (↑(PiLp.equiv p β) x) (↑(PiLp.equiv p β) y) ≤ ↑1 * edist x y
rcases p.dichotomy with (rfl | h)
no goals
case inl
𝕜 : Type ?u.49389
𝕜' : Type ?u.49392
ι : Type u_1
α : ι → Type ?u.49400
β : ι → Type u_2
inst✝³ : (i : ι) → PseudoMetricSpace (α i)
inst✝² : (i : ι) → PseudoEMetricSpace (β i)
inst✝¹ : Fintype ι
inst✝ : Fact (1 ≤ ⊤)
x y : PiLp ⊤ β
⊢ edist (↑(PiLp.equiv ⊤ β) x) (↑(PiLp.equiv ⊤ β) y) ≤ ↑1 * edist x y
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)
case inr
p : ℝ≥0∞
𝕜 : Type ?u.49389
𝕜' : Type ?u.49392
ι : Type u_1
α : ι → Type ?u.49400
β : ι → Type u_2
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 (↑(PiLp.equiv p β) x) (↑(PiLp.equiv p β) y) ≤ ↑1 * edist x y
case inr
p : ℝ≥0∞
𝕜 : Type ?u.49389
𝕜' : Type ?u.49392
ι : Type u_1
α : ι → Type ?u.49400
β : ι → Type u_2
inst✝³ : Fact (1 ≤ p)
inst✝² : (i : ι) → PseudoMetricSpace (α i)
inst✝¹ : (i : ι) → PseudoEMetricSpace (β i)
inst✝ : Fintype ι
x y : PiLp p β
h : 1 ≤ ENNReal.toReal p
⊢ edist (↑(PiLp.equiv p β) x) (↑(PiLp.equiv p β) y) ≤ ↑1 * edist x y
have cancel : p.toReal * (1 / p.toReal) = 1 := mul_div_cancel' 1 (zero_lt_one.trans_le h).ne'
case inr
p : ℝ≥0∞
𝕜 : Type ?u.49389
𝕜' : Type ?u.49392
ι : Type u_1
α : ι → Type ?u.49400
β : ι → Type u_2
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 (↑(PiLp.equiv p β) x) (↑(PiLp.equiv p β) y) ≤
    ↑1 * (∑ i : ι, edist (x i) (y i) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
case inr
p : ℝ≥0∞
𝕜 : Type ?u.49389
𝕜' : Type ?u.49392
ι : Type u_1
α : ι → Type ?u.49400
β : ι → Type u_2
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 (↑(PiLp.equiv p β) x) (↑(PiLp.equiv p β) y) ≤ ↑1 * edist x y
rw [edist_eq_sum (zero_lt_one.trans_le h)]
case inr
p : ℝ≥0∞
𝕜 : Type ?u.49389
𝕜' : Type ?u.49392
ι : Type u_1
α : ι → Type ?u.49400
β : ι → Type u_2
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 (↑(PiLp.equiv p β) x b) (↑(PiLp.equiv p β) y b) ≤
      (∑ x_1 : ι, edist (x x_1) (y x_1) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
case inr
p : ℝ≥0∞
𝕜 : Type ?u.49389
𝕜' : Type ?u.49392
ι : Type u_1
α : ι → Type ?u.49400
β : ι → Type u_2
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 (↑(PiLp.equiv p β) x) (↑(PiLp.equiv p β) y) ≤
    ↑1 * (∑ i : ι, edist (x i) (y i) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
simp only [edist, forall_prop_of_true, one_mul, Finset.mem_univ, Finset.sup_le_iff,
  ENNReal.coe_one]
case inr
p : ℝ≥0∞
𝕜 : Type ?u.49389
𝕜' : Type ?u.49392
ι : Type u_1
α : ι → Type ?u.49400
β : ι → Type u_2
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 (↑(PiLp.equiv p β) x i) (↑(PiLp.equiv p β) y i) ≤
    (∑ x_1 : ι, edist (x x_1) (y x_1) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
case inr
p : ℝ≥0∞
𝕜 : Type ?u.49389
𝕜' : Type ?u.49392
ι : Type u_1
α : ι → Type ?u.49400
β : ι → Type u_2
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 (↑(PiLp.equiv p β) x b) (↑(PiLp.equiv p β) y b) ≤
      (∑ x_1 : ι, edist (x x_1) (y x_1) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
intro i
no goals
case inr
p : ℝ≥0∞
𝕜 : Type ?u.49389
𝕜' : Type ?u.49392
ι : Type u_1
α : ι → Type ?u.49400
β : ι → Type u_2
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 (↑(PiLp.equiv p β) x i) (↑(PiLp.equiv p β) y i) ≤
    (∑ x_1 : ι, edist (x x_1) (y x_1) ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
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)
no goals
p : ℝ≥0∞
𝕜 : Type ?u.49389
𝕜' : Type ?u.49392
ι : Type u_1
α : ι → Type ?u.49400
β : ι → Type u_2
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)
simp [← ENNReal.rpow_mul, cancel, -one_div]
p : ℝ≥0∞
𝕜 : Type ?u.49389
𝕜' : Type ?u.49392
ι : Type u_1
α : ι → Type ?u.49400
β : ι → Type u_2
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
p : ℝ≥0∞
𝕜 : Type ?u.49389
𝕜' : Type ?u.49392
ι : Type u_1
α : ι → Type ?u.49400
β : ι → Type u_2
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)
apply ENNReal.rpow_le_rpow _ (one_div_nonneg.2 <| zero_le_one.trans h)
no goals
p : ℝ≥0∞
𝕜 : Type ?u.49389
𝕜' : Type ?u.49392
ι : Type u_1
α : ι → Type ?u.49400
β : ι → Type u_2
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
exact Finset.single_le_sum (fun i _ => (bot_le : (0 : ℝ≥0∞) ≤ _)) (Finset.mem_univ i)