[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ LipschitzWith K f ↔ ∀ (x y : α), dist (f x) (f y) ≤ ↑K * dist x y
[PROOFSTEP]
simp only [LipschitzWith, edist_nndist, dist_nndist]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
f : α → β
⊢ (∀ (x y : α), ↑(nndist (f x) (f y)) ≤ ↑K * ↑(nndist x y)) ↔ ∀ (x y : α), ↑(nndist (f x) (f y)) ≤ ↑K * ↑(nndist x y)
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
⊢ LipschitzOnWith K f s ↔ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → dist (f x) (f y) ≤ ↑K * dist x y
[PROOFSTEP]
simp only [LipschitzOnWith, edist_nndist, dist_nndist]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
K : ℝ≥0
s : Set α
f : α → β
⊢ (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → ↑(nndist (f x) (f y)) ≤ ↑K * ↑(nndist x y)) ↔
    ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → ↑(nndist (f x) (f y)) ≤ ↑K * ↑(nndist x y)
[PROOFSTEP]
norm_cast
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
⊢ LipschitzOnWith K f univ ↔ LipschitzWith K f
[PROOFSTEP]
simp [LipschitzOnWith, LipschitzWith]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
K : ℝ≥0
f : α → β
s : Set α
⊢ LipschitzOnWith K f s ↔ LipschitzWith K (restrict s f)
[PROOFSTEP]
simp only [LipschitzOnWith, LipschitzWith, SetCoe.forall', restrict, Subtype.edist_eq]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
x✝ y✝ : α
r : ℝ≥0∞
h : LipschitzWith K f
x y : α
⊢ (↑K)⁻¹ * edist (f x) (f y) ≤ edist x y
[PROOFSTEP]
rw [mul_comm, ← div_eq_mul_inv]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
x✝ y✝ : α
r : ℝ≥0∞
h : LipschitzWith K f
x y : α
⊢ edist (f x) (f y) / ↑K ≤ edist x y
[PROOFSTEP]
exact ENNReal.div_le_of_le_mul' (h x y)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
x✝ y✝ : α
r : ℝ≥0∞
h : ∀ (x y : α), edist (f x) (f y) ≤ edist x y
x y : α
⊢ edist (f x) (f y) ≤ ↑1 * edist x y
[PROOFSTEP]
simp only [ENNReal.coe_one, one_mul, h]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
x y : α
r : ℝ≥0∞
hf : LipschitzWith K f
s : Set α
⊢ diam (f '' s) ≤ ↑K * diam s
[PROOFSTEP]
apply EMetric.diam_le
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
x y : α
r : ℝ≥0∞
hf : LipschitzWith K f
s : Set α
⊢ ∀ (x : β), x ∈ f '' s → ∀ (y : β), y ∈ f '' s → edist x y ≤ ↑K * diam s
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩
[GOAL]
case h.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
x✝ y✝ : α
r : ℝ≥0∞
hf : LipschitzWith K f
s : Set α
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ edist (f x) (f y) ≤ ↑K * diam s
[PROOFSTEP]
exact hf.edist_le_mul_of_le (EMetric.edist_le_diam_of_mem hx hy)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
x✝ y✝ : α
r : ℝ≥0∞
b : β
x y : α
⊢ edist ((fun x => b) x) ((fun x => b) y) ≤ ↑0 * edist x y
[PROOFSTEP]
simp only [edist_self, zero_le]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K✝ : ℝ≥0
f : α → β
x✝ y✝ : α
r : ℝ≥0∞
b : β
K : ℝ≥0
x y : α
⊢ edist ((fun x => b) x) ((fun x => b) y) ≤ ↑K * edist x y
[PROOFSTEP]
simp only [edist_self, zero_le]
[GOAL]
α✝ : Type u
β : Type v
γ : Type w
ι : Type x
inst✝⁴ : PseudoEMetricSpace α✝
inst✝³ : PseudoEMetricSpace β
inst✝² : PseudoEMetricSpace γ
K : ℝ≥0
f✝ : α✝ → β
x y : α✝
r : ℝ≥0∞
α : ι → Type u
inst✝¹ : (i : ι) → PseudoEMetricSpace (α i)
inst✝ : Fintype ι
i : ι
f g : (x : ι) → α x
⊢ edist (eval i f) (eval i g) ≤ edist f g
[PROOFSTEP]
convert edist_le_pi_edist f g i
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f✝ : α → β
x✝ y✝ : α
r : ℝ≥0∞
Kf Kg : ℝ≥0
f : β → γ
g : α → β
hf : LipschitzWith Kf f
hg : LipschitzWith Kg g
x y : α
⊢ ↑Kf * (↑Kg * edist x y) = ↑(Kf * Kg) * edist x y
[PROOFSTEP]
rw [← mul_assoc, ENNReal.coe_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f✝ : α → β
x y : α
r : ℝ≥0∞
f : α → β
Kf : ℝ≥0
hf : LipschitzWith Kf f
g : α → γ
Kg : ℝ≥0
hg : LipschitzWith Kg g
⊢ LipschitzWith (max Kf Kg) fun x => (f x, g x)
[PROOFSTEP]
intro x y
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f✝ : α → β
x✝ y✝ : α
r : ℝ≥0∞
f : α → β
Kf : ℝ≥0
hf : LipschitzWith Kf f
g : α → γ
Kg : ℝ≥0
hg : LipschitzWith Kg g
x y : α
⊢ edist ((fun x => (f x, g x)) x) ((fun x => (f x, g x)) y) ≤ ↑(max Kf Kg) * edist x y
[PROOFSTEP]
rw [ENNReal.coe_mono.map_max, Prod.edist_eq, ENNReal.max_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f✝ : α → β
x✝ y✝ : α
r : ℝ≥0∞
f : α → β
Kf : ℝ≥0
hf : LipschitzWith Kf f
g : α → γ
Kg : ℝ≥0
hg : LipschitzWith Kg g
x y : α
⊢ max (edist ((fun x => (f x, g x)) x).fst ((fun x => (f x, g x)) y).fst)
      (edist ((fun x => (f x, g x)) x).snd ((fun x => (f x, g x)) y).snd) ≤
    max (↑Kf * edist x y) (↑Kg * edist x y)
[PROOFSTEP]
exact max_le_max (hf x y) (hg x y)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
x y : α
r : ℝ≥0∞
a : α
⊢ LipschitzWith 1 (Prod.mk a)
[PROOFSTEP]
simpa only [max_eq_right zero_le_one] using (LipschitzWith.const a).prod LipschitzWith.id
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f : α → β
x y : α
r : ℝ≥0∞
b : β
⊢ LipschitzWith 1 fun a => (a, b)
[PROOFSTEP]
simpa only [max_eq_left zero_le_one] using LipschitzWith.id.prod (LipschitzWith.const b)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f✝ : α → β
x y : α
r : ℝ≥0∞
f : α → β → γ
Kα Kβ : ℝ≥0
hα : ∀ (b : β), LipschitzWith Kα fun a => f a b
hβ : ∀ (a : α), LipschitzWith Kβ (f a)
⊢ LipschitzWith (Kα + Kβ) (uncurry f)
[PROOFSTEP]
rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
[GOAL]
case mk.mk
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f✝ : α → β
x y : α
r : ℝ≥0∞
f : α → β → γ
Kα Kβ : ℝ≥0
hα : ∀ (b : β), LipschitzWith Kα fun a => f a b
hβ : ∀ (a : α), LipschitzWith Kβ (f a)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ edist (uncurry f (a₁, b₁)) (uncurry f (a₂, b₂)) ≤ ↑(Kα + Kβ) * edist (a₁, b₁) (a₂, b₂)
[PROOFSTEP]
simp only [Function.uncurry, ENNReal.coe_add, add_mul]
[GOAL]
case mk.mk
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f✝ : α → β
x y : α
r : ℝ≥0∞
f : α → β → γ
Kα Kβ : ℝ≥0
hα : ∀ (b : β), LipschitzWith Kα fun a => f a b
hβ : ∀ (a : α), LipschitzWith Kβ (f a)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ edist (f a₁ b₁) (f a₂ b₂) ≤ ↑Kα * edist (a₁, b₁) (a₂, b₂) + ↑Kβ * edist (a₁, b₁) (a₂, b₂)
[PROOFSTEP]
apply le_trans (edist_triangle _ (f a₂ b₁) _)
[GOAL]
case mk.mk
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f✝ : α → β
x y : α
r : ℝ≥0∞
f : α → β → γ
Kα Kβ : ℝ≥0
hα : ∀ (b : β), LipschitzWith Kα fun a => f a b
hβ : ∀ (a : α), LipschitzWith Kβ (f a)
a₁ : α
b₁ : β
a₂ : α
b₂ : β
⊢ edist (f a₁ b₁) (f a₂ b₁) + edist (f a₂ b₁) (f a₂ b₂) ≤ ↑Kα * edist (a₁, b₁) (a₂, b₂) + ↑Kβ * edist (a₁, b₁) (a₂, b₂)
[PROOFSTEP]
exact
  add_le_add (le_trans (hα _ _ _) <| ENNReal.mul_left_mono <| le_max_left _ _)
    (le_trans (hβ _ _ _) <| ENNReal.mul_left_mono <| le_max_right _ _)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f✝ : α → β
x y : α
r : ℝ≥0∞
f : α → α
hf : LipschitzWith K f
⊢ LipschitzWith (K ^ 0) f^[0]
[PROOFSTEP]
simpa only [pow_zero] using LipschitzWith.id
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f✝ : α → β
x y : α
r : ℝ≥0∞
f : α → α
hf : LipschitzWith K f
n : ℕ
⊢ LipschitzWith (K ^ (n + 1)) f^[n + 1]
[PROOFSTEP]
rw [pow_succ']
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f✝ : α → β
x y : α
r : ℝ≥0∞
f : α → α
hf : LipschitzWith K f
n : ℕ
⊢ LipschitzWith (K ^ n * K) f^[n + 1]
[PROOFSTEP]
exact (LipschitzWith.iterate hf n).comp hf
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f✝ : α → β
x✝ y : α
r : ℝ≥0∞
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
⊢ edist (f^[n] x) (f^[n + 1] x) ≤ edist x (f x) * ↑K ^ n
[PROOFSTEP]
rw [iterate_succ, mul_comm]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K : ℝ≥0
f✝ : α → β
x✝ y : α
r : ℝ≥0∞
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
⊢ edist (f^[n] x) ((f^[n] ∘ f) x) ≤ ↑K ^ n * edist x (f x)
[PROOFSTEP]
simpa only [ENNReal.coe_pow] using (hf.iterate n) x (f x)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K✝ : ℝ≥0
f✝ : α → β
x y : α
r : ℝ≥0∞
f : ι → Function.End α
K : ι → ℝ≥0
h : ∀ (i : ι), LipschitzWith (K i) (f i)
⊢ LipschitzWith (List.prod (List.map K [])) (List.prod (List.map f []))
[PROOFSTEP]
simpa using LipschitzWith.id
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K✝ : ℝ≥0
f✝ : α → β
x y : α
r : ℝ≥0∞
f : ι → Function.End α
K : ι → ℝ≥0
h : ∀ (i : ι), LipschitzWith (K i) (f i)
i : ι
l : List ι
⊢ LipschitzWith (List.prod (List.map K (i :: l))) (List.prod (List.map f (i :: l)))
[PROOFSTEP]
simp only [List.map_cons, List.prod_cons]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K✝ : ℝ≥0
f✝ : α → β
x y : α
r : ℝ≥0∞
f : ι → Function.End α
K : ι → ℝ≥0
h : ∀ (i : ι), LipschitzWith (K i) (f i)
i : ι
l : List ι
⊢ LipschitzWith (K i * List.prod (List.map K l)) (f i * List.prod (List.map f l))
[PROOFSTEP]
exact (h i).mul (LipschitzWith.list_prod f K h l)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K✝ : ℝ≥0
f✝ : α → β
x y : α
r : ℝ≥0∞
f : Function.End α
K : ℝ≥0
h : LipschitzWith K f
⊢ LipschitzWith (K ^ 0) (f ^ 0)
[PROOFSTEP]
simpa only [pow_zero] using LipschitzWith.id
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K✝ : ℝ≥0
f✝ : α → β
x y : α
r : ℝ≥0∞
f : Function.End α
K : ℝ≥0
h : LipschitzWith K f
n : ℕ
⊢ LipschitzWith (K ^ (n + 1)) (f ^ (n + 1))
[PROOFSTEP]
rw [pow_succ, pow_succ]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : PseudoEMetricSpace β
inst✝ : PseudoEMetricSpace γ
K✝ : ℝ≥0
f✝ : α → β
x y : α
r : ℝ≥0∞
f : Function.End α
K : ℝ≥0
h : LipschitzWith K f
n : ℕ
⊢ LipschitzWith (K * K ^ n) (f * f ^ n)
[PROOFSTEP]
exact h.mul (LipschitzWith.pow h n)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
K✝ : ℝ≥0
f : α → β
x✝ y✝ : α
r K : ℝ
h : ∀ (x y : α), dist (f x) (f y) ≤ K * dist x y
x y : α
⊢ K * dist x y ≤ ↑(Real.toNNReal K) * dist x y
[PROOFSTEP]
gcongr
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
K✝ : ℝ≥0
f : α → β
x✝ y✝ : α
r K : ℝ
h : ∀ (x y : α), dist (f x) (f y) ≤ K * dist x y
x y : α
⊢ K ≤ ↑(Real.toNNReal K)
[PROOFSTEP]
apply Real.le_coe_toNNReal
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
K : ℝ≥0
f : α → β
x y : α
r : ℝ
h : ∀ (x y : α), dist (f x) (f y) ≤ dist x y
⊢ ∀ (x y : α), dist (f x) (f y) ≤ ↑1 * dist x y
[PROOFSTEP]
simpa only [NNReal.coe_one, one_mul] using h
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
K✝ : ℝ≥0
f✝ : α → β
x y : α
r : ℝ
f : α → ℝ
K : ℝ≥0
h : ∀ (x y : α), f x ≤ f y + ↑K * dist x y
⊢ LipschitzWith K f
[PROOFSTEP]
simpa only [Real.toNNReal_coe] using LipschitzWith.of_le_add_mul' K h
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
K : ℝ≥0
f✝ : α → β
x y : α
r : ℝ
f : α → ℝ
h : ∀ (x y : α), f x ≤ f y + dist x y
⊢ ∀ (x y : α), f x ≤ f y + ↑1 * dist x y
[PROOFSTEP]
simpa only [NNReal.coe_one, one_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
K : ℝ≥0
f : α → β
x y : α
r : ℝ
hf : LipschitzWith K f
hr : dist x y ≤ r
⊢ ↑K * dist x y ≤ ↑K * r
[PROOFSTEP]
gcongr
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
K : ℝ≥0
f : α → β
x y : α
r : ℝ
⊢ LipschitzWith 2 (uncurry dist)
[PROOFSTEP]
rw [← one_add_one_eq_two]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
K : ℝ≥0
f : α → β
x y : α
r : ℝ
⊢ LipschitzWith (1 + 1) (uncurry dist)
[PROOFSTEP]
exact LipschitzWith.uncurry LipschitzWith.dist_left LipschitzWith.dist_right
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
K : ℝ≥0
f✝ : α → β
x✝ y : α
r : ℝ
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
⊢ dist (f^[n] x) (f^[n + 1] x) ≤ dist x (f x) * ↑K ^ n
[PROOFSTEP]
rw [iterate_succ, mul_comm]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
K : ℝ≥0
f✝ : α → β
x✝ y : α
r : ℝ
f : α → α
hf : LipschitzWith K f
x : α
n : ℕ
⊢ dist (f^[n] x) ((f^[n] ∘ f) x) ≤ ↑K ^ n * dist x (f x)
[PROOFSTEP]
simpa only [NNReal.coe_pow] using (hf.iterate n).dist_le_mul x (f x)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoEMetricSpace α
f g : α → ℝ
Kf Kg : ℝ≥0
hf : LipschitzWith Kf f
hg : LipschitzWith Kg g
⊢ LipschitzWith (max Kf Kg) fun x => max (f x) (g x)
[PROOFSTEP]
simpa only [(· ∘ ·), one_mul] using lipschitzWith_max.comp (hf.prod hg)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoEMetricSpace α
f g : α → ℝ
Kf Kg : ℝ≥0
hf : LipschitzWith Kf f
hg : LipschitzWith Kg g
⊢ LipschitzWith (max Kf Kg) fun x => min (f x) (g x)
[PROOFSTEP]
simpa only [(· ∘ ·), one_mul] using lipschitzWith_min.comp (hf.prod hg)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoEMetricSpace α
f g : α → ℝ
Kf Kg : ℝ≥0
hf : LipschitzWith Kf f
a : ℝ
⊢ LipschitzWith Kf fun x => max (f x) a
[PROOFSTEP]
simpa only [max_eq_left (zero_le Kf)] using hf.max (LipschitzWith.const a)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoEMetricSpace α
f g : α → ℝ
Kf Kg : ℝ≥0
hf : LipschitzWith Kf f
a : ℝ
⊢ LipschitzWith Kf fun x => max a (f x)
[PROOFSTEP]
simpa only [max_comm] using hf.max_const a
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoEMetricSpace α
f g : α → ℝ
Kf Kg : ℝ≥0
hf : LipschitzWith Kf f
a : ℝ
⊢ LipschitzWith Kf fun x => min (f x) a
[PROOFSTEP]
simpa only [max_eq_left (zero_le Kf)] using hf.min (LipschitzWith.const a)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoEMetricSpace α
f g : α → ℝ
Kf Kg : ℝ≥0
hf : LipschitzWith Kf f
a : ℝ
⊢ LipschitzWith Kf fun x => min a (f x)
[PROOFSTEP]
simpa only [min_comm] using hf.min_const a
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s : Set α
t : Set β
h : Bounded (s ×ˢ t)
ht : Set.Nonempty t
⊢ Bounded s
[PROOFSTEP]
simpa only [fst_image_prod s ht] using (@LipschitzWith.prod_fst α β _ _).bounded_image h
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s : Set α
t : Set β
h : Bounded (s ×ˢ t)
hs : Set.Nonempty s
⊢ Bounded t
[PROOFSTEP]
simpa only [snd_image_prod hs t] using (@LipschitzWith.prod_snd α β _ _).bounded_image h
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
s : Set α
t : Set β
⊢ Bounded (s ×ˢ t) ↔ s = ∅ ∨ t = ∅ ∨ Bounded s ∧ Bounded t
[PROOFSTEP]
simp only [bounded_iff_isBounded, Bornology.isBounded_prod]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
K✝ : ℝ≥0
s : Set α
f : α → β
K : ℝ
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → dist (f x) (f y) ≤ K * dist x y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ K * dist x y ≤ ↑(Real.toNNReal K) * dist x y
[PROOFSTEP]
gcongr
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
K✝ : ℝ≥0
s : Set α
f : α → β
K : ℝ
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → dist (f x) (f y) ≤ K * dist x y
x : α
hx : x ∈ s
y : α
hy : y ∈ s
⊢ K ≤ ↑(Real.toNNReal K)
[PROOFSTEP]
apply Real.le_coe_toNNReal
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
K : ℝ≥0
s : Set α
f : α → β
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → dist (f x) (f y) ≤ dist x y
⊢ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → dist (f x) (f y) ≤ ↑1 * dist x y
[PROOFSTEP]
simpa only [NNReal.coe_one, one_mul] using h
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
K✝ : ℝ≥0
s : Set α
f✝ : α → β
f : α → ℝ
K : ℝ≥0
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x ≤ f y + ↑K * dist x y
⊢ LipschitzOnWith K f s
[PROOFSTEP]
simpa only [Real.toNNReal_coe] using LipschitzOnWith.of_le_add_mul' K h
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoMetricSpace α
inst✝¹ : PseudoMetricSpace β
inst✝ : PseudoMetricSpace γ
K : ℝ≥0
s : Set α
f✝ : α → β
f : α → ℝ
h : ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x ≤ f y + dist x y
⊢ ∀ (x : α), x ∈ s → ∀ (y : α), y ∈ s → f x ≤ f y + ↑1 * dist x y
[PROOFSTEP]
simpa only [NNReal.coe_one, one_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ (a : α), a ∈ s' → ContinuousOn (fun y => f (a, y)) t
hb : ∀ (b : β), b ∈ t → LipschitzOnWith K (fun x => f (x, b)) s
⊢ ContinuousOn f (s ×ˢ t)
[PROOFSTEP]
rintro ⟨x, y⟩ ⟨hx : x ∈ s, hy : y ∈ t⟩
[GOAL]
case mk.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ (a : α), a ∈ s' → ContinuousOn (fun y => f (a, y)) t
hb : ∀ (b : β), b ∈ t → LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
⊢ ContinuousWithinAt f (s ×ˢ t) (x, y)
[PROOFSTEP]
refine' EMetric.nhds_basis_closed_eball.tendsto_right_iff.2 fun ε (ε0 : 0 < ε) => _
[GOAL]
case mk.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ (a : α), a ∈ s' → ContinuousOn (fun y => f (a, y)) t
hb : ∀ (b : β), b ∈ t → LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε
⊢ ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ EMetric.closedBall (f (x, y)) ε
[PROOFSTEP]
replace ε0 : 0 < ε / 2 := ENNReal.half_pos ε0.ne'
[GOAL]
case mk.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ (a : α), a ∈ s' → ContinuousOn (fun y => f (a, y)) t
hb : ∀ (b : β), b ∈ t → LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
⊢ ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ EMetric.closedBall (f (x, y)) ε
[PROOFSTEP]
obtain ⟨δ, δpos, hδ⟩ : ∃ δ : ℝ≥0, 0 < δ ∧ (δ : ℝ≥0∞) * ↑(3 * K) < ε / 2 :=
  ENNReal.exists_nnreal_pos_mul_lt ENNReal.coe_ne_top ε0.ne'
[GOAL]
case mk.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ (a : α), a ∈ s' → ContinuousOn (fun y => f (a, y)) t
hb : ∀ (b : β), b ∈ t → LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < δ
hδ : ↑δ * ↑(3 * K) < ε / 2
⊢ ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ EMetric.closedBall (f (x, y)) ε
[PROOFSTEP]
rw [← ENNReal.coe_pos] at δpos 
[GOAL]
case mk.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ (a : α), a ∈ s' → ContinuousOn (fun y => f (a, y)) t
hb : ∀ (b : β), b ∈ t → LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
⊢ ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ EMetric.closedBall (f (x, y)) ε
[PROOFSTEP]
rcases EMetric.mem_closure_iff.1 (hss' hx) δ δpos with ⟨x', hx', hxx'⟩
[GOAL]
case mk.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ (a : α), a ∈ s' → ContinuousOn (fun y => f (a, y)) t
hb : ∀ (b : β), b ∈ t → LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
⊢ ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ EMetric.closedBall (f (x, y)) ε
[PROOFSTEP]
have A : s ∩ EMetric.ball x δ ∈ 𝓝[s] x := inter_mem_nhdsWithin _ (EMetric.ball_mem_nhds _ δpos)
[GOAL]
case mk.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ (a : α), a ∈ s' → ContinuousOn (fun y => f (a, y)) t
hb : ∀ (b : β), b ∈ t → LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ EMetric.ball x ↑δ ∈ 𝓝[s] x
⊢ ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ EMetric.closedBall (f (x, y)) ε
[PROOFSTEP]
have B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y :=
  inter_mem self_mem_nhdsWithin (ha x' hx' y hy (EMetric.closedBall_mem_nhds (f (x', y)) ε0))
[GOAL]
case mk.intro.intro.intro.intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ (a : α), a ∈ s' → ContinuousOn (fun y => f (a, y)) t
hb : ∀ (b : β), b ∈ t → LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ EMetric.ball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
⊢ ∀ᶠ (x_1 : α × β) in 𝓝[s ×ˢ t] (x, y), f x_1 ∈ EMetric.closedBall (f (x, y)) ε
[PROOFSTEP]
filter_upwards [nhdsWithin_prod A B] with ⟨a, b⟩ ⟨⟨has, hax⟩, ⟨hbt, hby⟩⟩
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ (a : α), a ∈ s' → ContinuousOn (fun y => f (a, y)) t
hb : ∀ (b : β), b ∈ t → LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ EMetric.ball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).fst ∈ s
hax : (a, b).fst ∈ EMetric.ball x ↑δ
hbt : (a, b).snd ∈ t
hby : (a, b).snd ∈ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2}
⊢ f (a, b) ∈ EMetric.closedBall (f (x, y)) ε
[PROOFSTEP]
calc
  edist (f (a, b)) (f (x, y)) ≤
      edist (f (a, b)) (f (x', b)) + edist (f (x', b)) (f (x', y)) + edist (f (x', y)) (f (x, y)) :=
    edist_triangle4 _ _ _ _
  _ ≤ K * (δ + δ) + ε / 2 + K * δ := by
    gcongr
    · refine (hb b hbt).edist_le_mul_of_le has (hs' hx') ?_
      refine (edist_triangle _ _ _).trans (add_le_add (le_of_lt hax) hxx'.le)
    · exact hby
    · exact (hb y hy).edist_le_mul_of_le (hs' hx') hx ((edist_comm _ _).trans_le hxx'.le)
  _ = δ * ↑(3 * K) + ε / 2 := by push_cast ; ring
  _ ≤ ε / 2 + ε / 2 := by gcongr
  _ = ε := ENNReal.add_halves _
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ (a : α), a ∈ s' → ContinuousOn (fun y => f (a, y)) t
hb : ∀ (b : β), b ∈ t → LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ EMetric.ball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).fst ∈ s
hax : (a, b).fst ∈ EMetric.ball x ↑δ
hbt : (a, b).snd ∈ t
hby : (a, b).snd ∈ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2}
⊢ edist (f (a, b)) (f (x', b)) + edist (f (x', b)) (f (x', y)) + edist (f (x', y)) (f (x, y)) ≤
    ↑K * (↑δ + ↑δ) + ε / 2 + ↑K * ↑δ
[PROOFSTEP]
gcongr
[GOAL]
case h₁.h₁
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ (a : α), a ∈ s' → ContinuousOn (fun y => f (a, y)) t
hb : ∀ (b : β), b ∈ t → LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ EMetric.ball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).fst ∈ s
hax : (a, b).fst ∈ EMetric.ball x ↑δ
hbt : (a, b).snd ∈ t
hby : (a, b).snd ∈ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2}
⊢ edist (f (a, b)) (f (x', b)) ≤ ↑K * (↑δ + ↑δ)
[PROOFSTEP]
refine (hb b hbt).edist_le_mul_of_le has (hs' hx') ?_
[GOAL]
case h₁.h₁
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ (a : α), a ∈ s' → ContinuousOn (fun y => f (a, y)) t
hb : ∀ (b : β), b ∈ t → LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ EMetric.ball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).fst ∈ s
hax : (a, b).fst ∈ EMetric.ball x ↑δ
hbt : (a, b).snd ∈ t
hby : (a, b).snd ∈ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2}
⊢ edist a x' ≤ ↑δ + ↑δ
[PROOFSTEP]
refine (edist_triangle _ _ _).trans (add_le_add (le_of_lt hax) hxx'.le)
[GOAL]
case h₁.h₂
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ (a : α), a ∈ s' → ContinuousOn (fun y => f (a, y)) t
hb : ∀ (b : β), b ∈ t → LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ EMetric.ball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).fst ∈ s
hax : (a, b).fst ∈ EMetric.ball x ↑δ
hbt : (a, b).snd ∈ t
hby : (a, b).snd ∈ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2}
⊢ edist (f (x', b)) (f (x', y)) ≤ ε / 2
[PROOFSTEP]
exact hby
[GOAL]
case h₂
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ (a : α), a ∈ s' → ContinuousOn (fun y => f (a, y)) t
hb : ∀ (b : β), b ∈ t → LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ EMetric.ball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).fst ∈ s
hax : (a, b).fst ∈ EMetric.ball x ↑δ
hbt : (a, b).snd ∈ t
hby : (a, b).snd ∈ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2}
⊢ edist (f (x', y)) (f (x, y)) ≤ ↑K * ↑δ
[PROOFSTEP]
exact (hb y hy).edist_le_mul_of_le (hs' hx') hx ((edist_comm _ _).trans_le hxx'.le)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ (a : α), a ∈ s' → ContinuousOn (fun y => f (a, y)) t
hb : ∀ (b : β), b ∈ t → LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ EMetric.ball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).fst ∈ s
hax : (a, b).fst ∈ EMetric.ball x ↑δ
hbt : (a, b).snd ∈ t
hby : (a, b).snd ∈ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2}
⊢ ↑K * (↑δ + ↑δ) + ε / 2 + ↑K * ↑δ = ↑δ * ↑(3 * K) + ε / 2
[PROOFSTEP]
push_cast
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ (a : α), a ∈ s' → ContinuousOn (fun y => f (a, y)) t
hb : ∀ (b : β), b ∈ t → LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ EMetric.ball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).fst ∈ s
hax : (a, b).fst ∈ EMetric.ball x ↑δ
hbt : (a, b).snd ∈ t
hby : (a, b).snd ∈ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2}
⊢ ↑K * (↑δ + ↑δ) + ε / 2 + ↑K * ↑δ = ↑δ * (3 * ↑K) + ε / 2
[PROOFSTEP]
ring
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
s s' : Set α
t : Set β
hs' : s' ⊆ s
hss' : s ⊆ closure s'
K : ℝ≥0
ha : ∀ (a : α), a ∈ s' → ContinuousOn (fun y => f (a, y)) t
hb : ∀ (b : β), b ∈ t → LipschitzOnWith K (fun x => f (x, b)) s
x : α
y : β
hx : x ∈ s
hy : y ∈ t
ε : ℝ≥0∞
ε0 : 0 < ε / 2
δ : ℝ≥0
δpos : 0 < ↑δ
hδ : ↑δ * ↑(3 * K) < ε / 2
x' : α
hx' : x' ∈ s'
hxx' : edist x x' < ↑δ
A : s ∩ EMetric.ball x ↑δ ∈ 𝓝[s] x
B : t ∩ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2} ∈ 𝓝[t] y
a : α
b : β
has : (a, b).fst ∈ s
hax : (a, b).fst ∈ EMetric.ball x ↑δ
hbt : (a, b).snd ∈ t
hby : (a, b).snd ∈ {b | edist (f (x', b)) (f (x', y)) ≤ ε / 2}
⊢ ↑δ * ↑(3 * K) + ε / 2 ≤ ε / 2 + ε / 2
[PROOFSTEP]
gcongr
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
K : ℝ≥0
s : Set α
hs : Dense s
ha : ∀ (a : α), a ∈ s → Continuous fun y => f (a, y)
hb : ∀ (b : β), LipschitzWith K fun x => f (x, b)
⊢ Continuous f
[PROOFSTEP]
simp only [continuous_iff_continuousOn_univ, ← univ_prod_univ, ← lipschitz_on_univ] at *
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝² : PseudoEMetricSpace α
inst✝¹ : TopologicalSpace β
inst✝ : PseudoEMetricSpace γ
f : α × β → γ
K : ℝ≥0
s : Set α
hs : Dense s
ha : ∀ (a : α), a ∈ s → ContinuousOn (fun y => f (a, y)) univ
hb : ∀ (b : β), LipschitzOnWith K (fun x => f (x, b)) univ
⊢ ContinuousOn f (univ ×ˢ univ)
[PROOFSTEP]
exact
  continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith f (subset_univ _) hs.closure_eq.ge K ha fun b _ =>
    hb b
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
x : α
r : ℝ
hr : 0 < r
K : ℝ
h : ∀ (y : α), dist y x < r → dist (f y) (f x) ≤ K * dist y x
⊢ ContinuousAt f x
[PROOFSTEP]
refine
  tendsto_iff_dist_tendsto_zero.2
    (squeeze_zero' (eventually_of_forall fun _ => dist_nonneg) (mem_of_superset (ball_mem_nhds _ hr) h) ?_)
      -- Then show that `K * dist y x` tends to zero as `y → x`
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
x : α
r : ℝ
hr : 0 < r
K : ℝ
h : ∀ (y : α), dist y x < r → dist (f y) (f x) ≤ K * dist y x
⊢ Tendsto (fun a => K * dist a x) (𝓝 x) (𝓝 0)
[PROOFSTEP]
refine (continuous_const.mul (continuous_id.dist continuous_const)).tendsto' _ _ ?_
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
f : α → β
x : α
r : ℝ
hr : 0 < r
K : ℝ
h : ∀ (y : α), dist y x < r → dist (f y) (f x) ≤ K * dist y x
⊢ K * dist (id x) x = 0
[PROOFSTEP]
simp
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
[PROOFSTEP]
rcases eq_empty_or_nonempty s with (rfl | hs)
[GOAL]
case inl
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoMetricSpace α
f : α → ℝ
K : ℝ≥0
hf : LipschitzOnWith K f ∅
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g ∅
[PROOFSTEP]
exact ⟨fun _ => 0, (LipschitzWith.const _).weaken (zero_le _), eqOn_empty _ _⟩
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : Set.Nonempty s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
[PROOFSTEP]
have : Nonempty s := by simp only [hs, nonempty_coe_sort]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : Set.Nonempty s
⊢ Nonempty ↑s
[PROOFSTEP]
simp only [hs, nonempty_coe_sort]
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : Set.Nonempty s
this : Nonempty ↑s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
[PROOFSTEP]
let g := fun y : α => iInf fun x : s => f x + K * dist y x
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : Set.Nonempty s
this : Nonempty ↑s
g : α → ℝ := fun y => ⨅ (x : ↑s), f ↑x + ↑K * dist y ↑x
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
[PROOFSTEP]
have B : ∀ y : α, BddBelow (range fun x : s => f x + K * dist y x) := fun y =>
  by
  rcases hs with ⟨z, hz⟩
  refine' ⟨f z - K * dist y z, _⟩
  rintro w ⟨t, rfl⟩
  dsimp
  rw [sub_le_iff_le_add, add_assoc, ← mul_add, add_comm (dist y t)]
  calc
    f z ≤ f t + K * dist z t := hf.le_add_mul hz t.2
    _ ≤ f t + K * (dist y z + dist y t) := by gcongr; apply dist_triangle_left
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : Set.Nonempty s
this : Nonempty ↑s
g : α → ℝ := fun y => ⨅ (x : ↑s), f ↑x + ↑K * dist y ↑x
y : α
⊢ BddBelow (range fun x => f ↑x + ↑K * dist y ↑x)
[PROOFSTEP]
rcases hs with ⟨z, hz⟩
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty ↑s
g : α → ℝ := fun y => ⨅ (x : ↑s), f ↑x + ↑K * dist y ↑x
y z : α
hz : z ∈ s
⊢ BddBelow (range fun x => f ↑x + ↑K * dist y ↑x)
[PROOFSTEP]
refine' ⟨f z - K * dist y z, _⟩
[GOAL]
case intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty ↑s
g : α → ℝ := fun y => ⨅ (x : ↑s), f ↑x + ↑K * dist y ↑x
y z : α
hz : z ∈ s
⊢ f z - ↑K * dist y z ∈ lowerBounds (range fun x => f ↑x + ↑K * dist y ↑x)
[PROOFSTEP]
rintro w ⟨t, rfl⟩
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty ↑s
g : α → ℝ := fun y => ⨅ (x : ↑s), f ↑x + ↑K * dist y ↑x
y z : α
hz : z ∈ s
t : ↑s
⊢ f z - ↑K * dist y z ≤ (fun x => f ↑x + ↑K * dist y ↑x) t
[PROOFSTEP]
dsimp
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty ↑s
g : α → ℝ := fun y => ⨅ (x : ↑s), f ↑x + ↑K * dist y ↑x
y z : α
hz : z ∈ s
t : ↑s
⊢ f z - ↑K * dist y z ≤ f ↑t + ↑K * dist y ↑t
[PROOFSTEP]
rw [sub_le_iff_le_add, add_assoc, ← mul_add, add_comm (dist y t)]
[GOAL]
case intro.intro
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty ↑s
g : α → ℝ := fun y => ⨅ (x : ↑s), f ↑x + ↑K * dist y ↑x
y z : α
hz : z ∈ s
t : ↑s
⊢ f z ≤ f ↑t + ↑K * (dist y z + dist y ↑t)
[PROOFSTEP]
calc
  f z ≤ f t + K * dist z t := hf.le_add_mul hz t.2
  _ ≤ f t + K * (dist y z + dist y t) := by gcongr; apply dist_triangle_left
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty ↑s
g : α → ℝ := fun y => ⨅ (x : ↑s), f ↑x + ↑K * dist y ↑x
y z : α
hz : z ∈ s
t : ↑s
⊢ f ↑t + ↑K * dist z ↑t ≤ f ↑t + ↑K * (dist y z + dist y ↑t)
[PROOFSTEP]
gcongr
[GOAL]
case bc.h
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : Nonempty ↑s
g : α → ℝ := fun y => ⨅ (x : ↑s), f ↑x + ↑K * dist y ↑x
y z : α
hz : z ∈ s
t : ↑s
⊢ dist z ↑t ≤ dist y z + dist y ↑t
[PROOFSTEP]
apply dist_triangle_left
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : Set.Nonempty s
this : Nonempty ↑s
g : α → ℝ := fun y => ⨅ (x : ↑s), f ↑x + ↑K * dist y ↑x
B : ∀ (y : α), BddBelow (range fun x => f ↑x + ↑K * dist y ↑x)
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
[PROOFSTEP]
have E : EqOn f g s := fun x hx =>
  by
  refine' le_antisymm (le_ciInf fun y => hf.le_add_mul hx y.2) _
  simpa only [add_zero, Subtype.coe_mk, mul_zero, dist_self] using ciInf_le (B x) ⟨x, hx⟩
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : Set.Nonempty s
this : Nonempty ↑s
g : α → ℝ := fun y => ⨅ (x : ↑s), f ↑x + ↑K * dist y ↑x
B : ∀ (y : α), BddBelow (range fun x => f ↑x + ↑K * dist y ↑x)
x : α
hx : x ∈ s
⊢ f x = g x
[PROOFSTEP]
refine' le_antisymm (le_ciInf fun y => hf.le_add_mul hx y.2) _
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : Set.Nonempty s
this : Nonempty ↑s
g : α → ℝ := fun y => ⨅ (x : ↑s), f ↑x + ↑K * dist y ↑x
B : ∀ (y : α), BddBelow (range fun x => f ↑x + ↑K * dist y ↑x)
x : α
hx : x ∈ s
⊢ g x ≤ f x
[PROOFSTEP]
simpa only [add_zero, Subtype.coe_mk, mul_zero, dist_self] using ciInf_le (B x) ⟨x, hx⟩
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : Set.Nonempty s
this : Nonempty ↑s
g : α → ℝ := fun y => ⨅ (x : ↑s), f ↑x + ↑K * dist y ↑x
B : ∀ (y : α), BddBelow (range fun x => f ↑x + ↑K * dist y ↑x)
E : EqOn f g s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
[PROOFSTEP]
refine' ⟨g, LipschitzWith.of_le_add_mul K fun x y => _, E⟩
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : Set.Nonempty s
this : Nonempty ↑s
g : α → ℝ := fun y => ⨅ (x : ↑s), f ↑x + ↑K * dist y ↑x
B : ∀ (y : α), BddBelow (range fun x => f ↑x + ↑K * dist y ↑x)
E : EqOn f g s
x y : α
⊢ g x ≤ g y + ↑K * dist x y
[PROOFSTEP]
rw [← sub_le_iff_le_add]
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : Set.Nonempty s
this : Nonempty ↑s
g : α → ℝ := fun y => ⨅ (x : ↑s), f ↑x + ↑K * dist y ↑x
B : ∀ (y : α), BddBelow (range fun x => f ↑x + ↑K * dist y ↑x)
E : EqOn f g s
x y : α
⊢ g x - ↑K * dist x y ≤ g y
[PROOFSTEP]
refine' le_ciInf fun z => _
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : Set.Nonempty s
this : Nonempty ↑s
g : α → ℝ := fun y => ⨅ (x : ↑s), f ↑x + ↑K * dist y ↑x
B : ∀ (y : α), BddBelow (range fun x => f ↑x + ↑K * dist y ↑x)
E : EqOn f g s
x y : α
z : ↑s
⊢ g x - ↑K * dist x y ≤ f ↑z + ↑K * dist y ↑z
[PROOFSTEP]
rw [sub_le_iff_le_add]
[GOAL]
case inr
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : Set.Nonempty s
this : Nonempty ↑s
g : α → ℝ := fun y => ⨅ (x : ↑s), f ↑x + ↑K * dist y ↑x
B : ∀ (y : α), BddBelow (range fun x => f ↑x + ↑K * dist y ↑x)
E : EqOn f g s
x y : α
z : ↑s
⊢ g x ≤ f ↑z + ↑K * dist y ↑z + ↑K * dist x y
[PROOFSTEP]
calc
  g x ≤ f z + K * dist x z := ciInf_le (B x) _
  _ ≤ f z + K * dist y z + K * dist x y :=
    by
    rw [add_assoc, ← mul_add, add_comm (dist y z)]
    gcongr
    apply dist_triangle
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : Set.Nonempty s
this : Nonempty ↑s
g : α → ℝ := fun y => ⨅ (x : ↑s), f ↑x + ↑K * dist y ↑x
B : ∀ (y : α), BddBelow (range fun x => f ↑x + ↑K * dist y ↑x)
E : EqOn f g s
x y : α
z : ↑s
⊢ f ↑z + ↑K * dist x ↑z ≤ f ↑z + ↑K * dist y ↑z + ↑K * dist x y
[PROOFSTEP]
rw [add_assoc, ← mul_add, add_comm (dist y z)]
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : Set.Nonempty s
this : Nonempty ↑s
g : α → ℝ := fun y => ⨅ (x : ↑s), f ↑x + ↑K * dist y ↑x
B : ∀ (y : α), BddBelow (range fun x => f ↑x + ↑K * dist y ↑x)
E : EqOn f g s
x y : α
z : ↑s
⊢ f ↑z + ↑K * dist x ↑z ≤ f ↑z + ↑K * (dist x y + dist y ↑z)
[PROOFSTEP]
gcongr
[GOAL]
case bc.h
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝ : PseudoMetricSpace α
f : α → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
hs : Set.Nonempty s
this : Nonempty ↑s
g : α → ℝ := fun y => ⨅ (x : ↑s), f ↑x + ↑K * dist y ↑x
B : ∀ (y : α), BddBelow (range fun x => f ↑x + ↑K * dist y ↑x)
E : EqOn f g s
x y : α
z : ↑s
⊢ dist x ↑z ≤ dist x y + dist y ↑z
[PROOFSTEP]
apply dist_triangle
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
[PROOFSTEP]
have : ∀ i, ∃ g : α → ℝ, LipschitzWith K g ∧ EqOn (fun x => f x i) g s := fun i =>
  by
  have : LipschitzOnWith K (fun x : α => f x i) s :=
    LipschitzOnWith.of_dist_le_mul fun x hx y hy => (dist_le_pi_dist _ _ i).trans (hf.dist_le_mul x hx y hy)
  exact this.extend_real
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
i : ι
⊢ ∃ g, LipschitzWith K g ∧ EqOn (fun x => f x i) g s
[PROOFSTEP]
have : LipschitzOnWith K (fun x : α => f x i) s :=
  LipschitzOnWith.of_dist_le_mul fun x hx y hy => (dist_le_pi_dist _ _ i).trans (hf.dist_le_mul x hx y hy)
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
i : ι
this : LipschitzOnWith K (fun x => f x i) s
⊢ ∃ g, LipschitzWith K g ∧ EqOn (fun x => f x i) g s
[PROOFSTEP]
exact this.extend_real
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
this : ∀ (i : ι), ∃ g, LipschitzWith K g ∧ EqOn (fun x => f x i) g s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
[PROOFSTEP]
choose g hg using this
[GOAL]
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x => f x i) (g i) s
⊢ ∃ g, LipschitzWith K g ∧ EqOn f g s
[PROOFSTEP]
refine' ⟨fun x i => g i x, LipschitzWith.of_dist_le_mul fun x y => _, _⟩
[GOAL]
case refine'_1
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x => f x i) (g i) s
x y : α
⊢ (dist (fun i => g i x) fun i => g i y) ≤ ↑K * dist x y
[PROOFSTEP]
exact (dist_pi_le_iff (mul_nonneg K.2 dist_nonneg)).2 fun i => (hg i).1.dist_le_mul x y
[GOAL]
case refine'_2
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x => f x i) (g i) s
⊢ EqOn f (fun x i => g i x) s
[PROOFSTEP]
intro x hx
[GOAL]
case refine'_2
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x => f x i) (g i) s
x : α
hx : x ∈ s
⊢ f x = (fun x i => g i x) x
[PROOFSTEP]
ext1 i
[GOAL]
case refine'_2.h
α : Type u
β : Type v
γ : Type w
ι : Type x
inst✝¹ : PseudoMetricSpace α
inst✝ : Fintype ι
f : α → ι → ℝ
s : Set α
K : ℝ≥0
hf : LipschitzOnWith K f s
g : ι → α → ℝ
hg : ∀ (i : ι), LipschitzWith K (g i) ∧ EqOn (fun x => f x i) (g i) s
x : α
hx : x ∈ s
i : ι
⊢ f x i = (fun x i => g i x) x i
[PROOFSTEP]
exact (hg i).2 hx
