Mathlib.Topology.EMetricSpace.Lipschitz

LipschitzWith definition

(K : ℝ≥0) (f : α → β)

Full source

/-- A function `f` is **Lipschitz continuous** with constant `K ≥ 0` if for all `x, y`
we have `dist (f x) (f y) ≤ K * dist x y`. -/
def LipschitzWith (K : ℝ≥0) (f : α → β) := ∀ x y, edist (f x) (f y) ≤ K * edist x y

Lipschitz continuous function

Informal description

A function $f : \alpha \to \beta$ between two (extended) metric spaces is called *Lipschitz continuous* with constant $K \geq 0$ if for all $x, y \in \alpha$, the inequality $\text{edist}(f x, f y) \leq K \cdot \text{edist}(x, y)$ holds. For a metric space, this is equivalent to $\text{dist}(f x, f y) \leq K \cdot \text{dist}(x, y)$.

LipschitzOnWith definition

(K : ℝ≥0) (f : α → β) (s : Set α)

Full source

/-- A function `f` is **Lipschitz continuous** with constant `K ≥ 0` **on `s`** if
for all `x, y` in `s` we have `dist (f x) (f y) ≤ K * dist x y`. -/
def LipschitzOnWith (K : ℝ≥0) (f : α → β) (s : Set α) :=
  ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → edist (f x) (f y) ≤ K * edist x y

Lipschitz continuity on a set with constant $ K $

Informal description

A function $ f : \alpha \to \beta $ between two (extended) metric spaces is called *Lipschitz continuous on a set $ s $* with constant $ K \geq 0 $ if for all $ x, y \in s $, the inequality $ \text{edist}(f x, f y) \leq K \cdot \text{edist}(x, y) $ holds. For a metric space, this is equivalent to $ \text{dist}(f x, f y) \leq K \cdot \text{dist}(x, y) $.

LocallyLipschitz definition

(f : α → β) : Prop

Full source

/-- `f : α → β` is called **locally Lipschitz continuous** iff every point `x`
has a neighbourhood on which `f` is Lipschitz. -/
def LocallyLipschitz (f : α → β) : Prop := ∀ x, ∃ K, ∃ t ∈ 𝓝 x, LipschitzOnWith K f t

Locally Lipschitz continuous function

Informal description

A function $ f : \alpha \to \beta $ between two (extended) metric spaces is called *locally Lipschitz continuous* if for every point $ x \in \alpha $, there exists a constant $ K \geq 0 $ and a neighborhood $ t $ of $ x $ such that $ f $ is Lipschitz continuous with constant $ K $ on $ t $.

LocallyLipschitzOn definition

(s : Set α) (f : α → β) : Prop

Full source

/-- `f : α → β` is called **locally Lipschitz continuous** on `s` iff every point `x` of `s`
has a neighbourhood within `s` on which `f` is Lipschitz. -/
def LocallyLipschitzOn (s : Set α) (f : α → β) : Prop :=
  ∀ ⦃x⦄, x ∈ s → ∃ K, ∃ t ∈ 𝓝[s] x, LipschitzOnWith K f t

Local Lipschitz continuity on a set

Informal description

A function $ f : \alpha \to \beta $ between two (extended) metric spaces is called *locally Lipschitz continuous on a set $ s $* if for every point $ x \in s $, there exists a constant $ K \geq 0 $ and a neighborhood $ t $ of $ x $ within $ s $ such that $ f $ is Lipschitz continuous on $ t $ with constant $ K $.

lipschitzOnWith_empty theorem

(K : ℝ≥0) (f : α → β) : LipschitzOnWith K f ∅

Full source

/-- Every function is Lipschitz on the empty set (with any Lipschitz constant). -/
@[simp]
theorem lipschitzOnWith_empty (K : ℝ≥0) (f : α → β) : LipschitzOnWith K f ∅ := fun _ => False.elim

Vacuously Lipschitz on Empty Set

Informal description

For any extended nonnegative real number $K \geq 0$ and any function $f : \alpha \to \beta$ between (extended) metric spaces, $f$ is Lipschitz continuous on the empty set with constant $K$. That is, the condition $\text{edist}(f x, f y) \leq K \cdot \text{edist}(x, y)$ holds vacuously for all $x, y \in \emptyset$.

locallyLipschitzOn_empty theorem

(f : α → β) : LocallyLipschitzOn ∅ f

Full source

@[simp] lemma locallyLipschitzOn_empty (f : α → β) : LocallyLipschitzOn ∅ f := fun _ ↦ False.elim

Vacuously Locally Lipschitz on Empty Set

Informal description

For any function $f : \alpha \to \beta$ between (extended) metric spaces, $f$ is locally Lipschitz continuous on the empty set.

LipschitzOnWith.mono theorem

(hf : LipschitzOnWith K f t) (h : s ⊆ t) : LipschitzOnWith K f s

Full source

/-- Being Lipschitz on a set is monotone w.r.t. that set. -/
theorem LipschitzOnWith.mono (hf : LipschitzOnWith K f t) (h : s ⊆ t) : LipschitzOnWith K f s :=
  fun _x x_in _y y_in => hf (h x_in) (h y_in)

Monotonicity of Lipschitz Continuity with Respect to Subsets

Informal description

Let $f : \alpha \to \beta$ be a function between metric spaces, and let $K \geq 0$ be a constant. If $f$ is Lipschitz continuous on a set $t$ with constant $K$, then for any subset $s \subseteq t$, the function $f$ is also Lipschitz continuous on $s$ with the same constant $K$.

LocallyLipschitzOn.mono theorem

(hf : LocallyLipschitzOn t f) (h : s ⊆ t) : LocallyLipschitzOn s f

Full source

lemma LocallyLipschitzOn.mono (hf : LocallyLipschitzOn t f) (h : s ⊆ t) : LocallyLipschitzOn s f :=
  fun x hx ↦ by obtain ⟨K, u, hu, hfu⟩ := hf (h hx); exact ⟨K, u, nhdsWithin_mono _ h hu, hfu⟩

Local Lipschitz Continuity is Preserved Under Subset Inclusion

Informal description

Let $f : \alpha \to \beta$ be a function between (extended) metric spaces. If $f$ is locally Lipschitz continuous on a set $t$, then for any subset $s \subseteq t$, the function $f$ is also locally Lipschitz continuous on $s$.

lipschitzOnWith_univ theorem

: LipschitzOnWith K f univ ↔ LipschitzWith K f

Full source

/-- `f` is Lipschitz iff it is Lipschitz on the entire space. -/
@[simp] lemma lipschitzOnWith_univ : LipschitzOnWithLipschitzOnWith K f univ ↔ LipschitzWith K f := by
  simp [LipschitzOnWith, LipschitzWith]

Lipschitz Continuity on Entire Space vs. Subsets: $\text{LipschitzOnWith}~K~f~\text{univ} \leftrightarrow \text{LipschitzWith}~K~f$

Informal description

A function $f \colon \alpha \to \beta$ between two (extended) metric spaces is Lipschitz continuous with constant $K \geq 0$ on the entire space $\alpha$ if and only if it is Lipschitz continuous with the same constant $K$ on every subset of $\alpha$. In other words, $f$ satisfies $\text{edist}(f x, f y) \leq K \cdot \text{edist}(x, y)$ for all $x, y \in \alpha$ if and only if it satisfies this inequality for all $x, y$ in any subset $s \subseteq \alpha$.

locallyLipschitzOn_univ theorem

: LocallyLipschitzOn univ f ↔ LocallyLipschitz f

Full source

@[simp] lemma locallyLipschitzOn_univ : LocallyLipschitzOnLocallyLipschitzOn univ f ↔ LocallyLipschitz f := by
  simp [LocallyLipschitzOn, LocallyLipschitz]

Local Lipschitz Continuity on Entire Space vs. Globally Local Lipschitz Continuity

Informal description

A function $f \colon \alpha \to \beta$ between two (extended) metric spaces is locally Lipschitz continuous on the entire space $\alpha$ if and only if it is locally Lipschitz continuous.

LocallyLipschitz.locallyLipschitzOn theorem

(h : LocallyLipschitz f) : LocallyLipschitzOn s f

Full source

protected lemma LocallyLipschitz.locallyLipschitzOn (h : LocallyLipschitz f) :
    LocallyLipschitzOn s f := (locallyLipschitzOn_univ.2 h).mono s.subset_univ

Local Lipschitz continuity implies local Lipschitz continuity on any subset

Informal description

If a function $f \colon \alpha \to \beta$ between two (extended) metric spaces is locally Lipschitz continuous, then for any subset $s \subseteq \alpha$, the function $f$ is locally Lipschitz continuous on $s$.

lipschitzOnWith_iff_restrict theorem

: LipschitzOnWith K f s ↔ LipschitzWith K (s.restrict f)

Full source

theorem lipschitzOnWith_iff_restrict : LipschitzOnWithLipschitzOnWith K f s ↔ LipschitzWith K (s.restrict f) := by
  simp [LipschitzOnWith, LipschitzWith]

Lipschitz Continuity on Set is Equivalent to Lipschitz Continuity of Restriction

Informal description

A function $f : \alpha \to \beta$ is Lipschitz continuous on a set $s \subseteq \alpha$ with constant $K \geq 0$ if and only if the restriction of $f$ to $s$ is Lipschitz continuous with the same constant $K$.

lipschitzOnWith_restrict theorem

{t : Set s} : LipschitzOnWith K (s.restrict f) t ↔ LipschitzOnWith K f (s ∩ Subtype.val '' t)

Full source

lemma lipschitzOnWith_restrict {t : Set s} :
    LipschitzOnWithLipschitzOnWith K (s.restrict f) t ↔ LipschitzOnWith K f (s ∩ Subtype.val '' t) := by
  simp [LipschitzOnWith, LipschitzWith]

Lipschitz Continuity of Restriction vs. Original Function on Subset

Informal description

For any subset $t$ of $s$, the restriction of $f$ to $s$ is Lipschitz continuous on $t$ with constant $K$ if and only if $f$ is Lipschitz continuous on the intersection of $s$ with the image of $t$ under the inclusion map, with the same constant $K$.

locallyLipschitzOn_iff_restrict theorem

: LocallyLipschitzOn s f ↔ LocallyLipschitz (s.restrict f)

Full source

lemma locallyLipschitzOn_iff_restrict :
    LocallyLipschitzOnLocallyLipschitzOn s f ↔ LocallyLipschitz (s.restrict f) := by
  simp only [LocallyLipschitzOn, LocallyLipschitz, SetCoe.forall', restrict_apply,
    Subtype.edist_mk_mk, ← lipschitzOnWith_iff_restrict, lipschitzOnWith_restrict,
    nhds_subtype_eq_comap_nhdsWithin, mem_comap]
  congr! with x K
  constructor
  · rintro ⟨t, ht, hft⟩
    exact ⟨_, ⟨t, ht, Subset.rfl⟩, hft.mono <| inter_subset_right.trans <| image_preimage_subset ..⟩
  · rintro ⟨t, ⟨u, hu, hut⟩, hft⟩
    exact ⟨s ∩ u, Filter.inter_mem self_mem_nhdsWithin hu,
      hft.mono fun x hx ↦ ⟨hx.1, ⟨x, hx.1⟩, hut hx.2, rfl⟩⟩

Local Lipschitz Continuity on Set is Equivalent to Local Lipschitz Continuity of Restriction

Informal description

A function $f : \alpha \to \beta$ is locally Lipschitz continuous on a set $s \subseteq \alpha$ if and only if the restriction of $f$ to $s$ is locally Lipschitz continuous.

Set.MapsTo.lipschitzOnWith_iff_restrict theorem

{t : Set β} (h : MapsTo f s t) : LipschitzOnWith K f s ↔ LipschitzWith K (h.restrict f s t)

Full source

lemma Set.MapsTo.lipschitzOnWith_iff_restrict {t : Set β} (h : MapsTo f s t) :
    LipschitzOnWithLipschitzOnWith K f s ↔ LipschitzWith K (h.restrict f s t) :=
  _root_.lipschitzOnWith_iff_restrict

Lipschitz continuity on a set is equivalent to Lipschitz continuity of its restriction

Informal description

Let $f : \alpha \to \beta$ be a function, $s \subseteq \alpha$ and $t \subseteq \beta$ be sets such that $f$ maps $s$ into $t$ (i.e., $f(x) \in t$ for all $x \in s$). Then $f$ is Lipschitz continuous on $s$ with constant $K \geq 0$ if and only if the restricted function $f|_s : s \to t$ is Lipschitz continuous with the same constant $K$.

LipschitzWith.lipschitzOnWith theorem

(h : LipschitzWith K f) : LipschitzOnWith K f s

Full source

protected theorem lipschitzOnWith (h : LipschitzWith K f) : LipschitzOnWith K f s :=
  fun x _ y _ => h x y

Restriction of Lipschitz Continuous Function to Subset Preserves Lipschitz Constant

Informal description

If a function $f : \alpha \to \beta$ is Lipschitz continuous with constant $K \geq 0$ on the entire space $\alpha$, then it is Lipschitz continuous with the same constant $K$ on any subset $s \subseteq \alpha$.

LipschitzWith.edist_le_mul theorem

(h : LipschitzWith K f) (x y : α) : edist (f x) (f y) ≤ K * edist x y

Full source

theorem edist_le_mul (h : LipschitzWith K f) (x y : α) : edist (f x) (f y) ≤ K * edist x y :=
  h x y

Lipschitz Condition for Extended Distance

Informal description

For any Lipschitz continuous function $f \colon \alpha \to \beta$ with constant $K \geq 0$, and for any two points $x, y \in \alpha$, the extended distance between $f(x)$ and $f(y)$ is bounded by $K$ times the extended distance between $x$ and $y$, i.e., \[ \text{edist}(f(x), f(y)) \leq K \cdot \text{edist}(x, y). \]

LipschitzWith.edist_le_mul_of_le theorem

(h : LipschitzWith K f) (hr : edist x y ≤ r) : edist (f x) (f y) ≤ K * r

Full source

theorem edist_le_mul_of_le (h : LipschitzWith K f) (hr : edist x y ≤ r) :
    edist (f x) (f y) ≤ K * r :=
  (h x y).trans <| mul_left_mono hr

Lipschitz Condition for Extended Distance with Upper Bound

Informal description

Let $f \colon \alpha \to \beta$ be a Lipschitz continuous function with constant $K \geq 0$ between two extended metric spaces. For any $x, y \in \alpha$ and $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if the extended distance $\text{edist}(x, y) \leq r$, then the extended distance between the images satisfies $\text{edist}(f(x), f(y)) \leq K \cdot r$.

LipschitzWith.edist_lt_mul_of_lt theorem

(h : LipschitzWith K f) (hK : K ≠ 0) (hr : edist x y < r) : edist (f x) (f y) < K * r

Full source

theorem edist_lt_mul_of_lt (h : LipschitzWith K f) (hK : K ≠ 0) (hr : edist x y < r) :
    edist (f x) (f y) < K * r :=
  (h x y).trans_lt <| (ENNReal.mul_lt_mul_left (ENNReal.coe_ne_zero.2 hK) ENNReal.coe_ne_top).2 hr

Lipschitz Continuity Preserves Strict Inequality for Extended Distances

Informal description

Let $f : \alpha \to \beta$ be a Lipschitz continuous function with constant $K \neq 0$ between two extended metric spaces. For any $x, y \in \alpha$ and $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, if the extended distance $\text{edist}(x, y) < r$, then the extended distance between the images satisfies $\text{edist}(f x, f y) < K \cdot r$.

LipschitzWith.mapsTo_emetric_closedBall theorem

(h : LipschitzWith K f) (x : α) (r : ℝ≥0∞) : MapsTo f (closedBall x r) (closedBall (f x) (K * r))

Full source

theorem mapsTo_emetric_closedBall (h : LipschitzWith K f) (x : α) (r : ℝ≥0∞) :
    MapsTo f (closedBall x r) (closedBall (f x) (K * r)) := fun _y hy => h.edist_le_mul_of_le hy

Lipschitz Functions Preserve Closed Balls with Scaled Radius

Informal description

Let $f \colon \alpha \to \beta$ be a Lipschitz continuous function with constant $K \geq 0$ between two extended metric spaces. For any point $x \in \alpha$ and radius $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the function $f$ maps the closed ball $\overline{B}(x, r)$ into the closed ball $\overline{B}(f(x), K \cdot r)$. In other words, for all $y \in \overline{B}(x, r)$, we have $f(y) \in \overline{B}(f(x), K \cdot r)$.

LipschitzWith.mapsTo_emetric_ball theorem

(h : LipschitzWith K f) (hK : K ≠ 0) (x : α) (r : ℝ≥0∞) : MapsTo f (ball x r) (ball (f x) (K * r))

Full source

theorem mapsTo_emetric_ball (h : LipschitzWith K f) (hK : K ≠ 0) (x : α) (r : ℝ≥0∞) :
    MapsTo f (ball x r) (ball (f x) (K * r)) := fun _y hy => h.edist_lt_mul_of_lt hK hy

Lipschitz Functions Preserve Open Balls with Scaled Radius

Informal description

Let $f : \alpha \to \beta$ be a Lipschitz continuous function with constant $K \neq 0$ between two extended metric spaces. For any $x \in \alpha$ and $r \in \mathbb{R}_{\geq 0} \cup \{\infty\}$, the function $f$ maps the open ball $\text{ball}(x, r)$ into the open ball $\text{ball}(f x, K \cdot r)$. In other words, for all $y \in \text{ball}(x, r)$, we have $f(y) \in \text{ball}(f x, K \cdot r)$.

LipschitzWith.edist_lt_top theorem

(hf : LipschitzWith K f) {x y : α} (h : edist x y ≠ ⊤) : edist (f x) (f y) < ⊤

Full source

theorem edist_lt_top (hf : LipschitzWith K f) {x y : α} (h : edistedist x y ≠ ⊤) :
    edist (f x) (f y) < ⊤ :=
  (hf x y).trans_lt <| ENNReal.mul_lt_top ENNReal.coe_lt_top h.lt_top

Finite Distance Preservation under Lipschitz Maps

Informal description

Let $f \colon \alpha \to \beta$ be a Lipschitz continuous function with constant $K \geq 0$ between two extended metric spaces. For any points $x, y \in \alpha$ such that the extended distance $\text{edist}(x, y)$ is finite, the extended distance $\text{edist}(f(x), f(y))$ is also finite.

LipschitzWith.mul_edist_le theorem

(h : LipschitzWith K f) (x y : α) : (K⁻¹ : ℝ≥0∞) * edist (f x) (f y) ≤ edist x y

Full source

theorem mul_edist_le (h : LipschitzWith K f) (x y : α) :
    (K⁻¹ : ℝ≥0∞) * edist (f x) (f y) ≤ edist x y := by
  rw [mul_comm, ← div_eq_mul_inv]
  exact ENNReal.div_le_of_le_mul' (h x y)

Inverse Lipschitz Inequality for Extended Distances

Informal description

Let $f \colon \alpha \to \beta$ be a Lipschitz continuous function with constant $K \geq 0$ between two extended metric spaces. Then for any points $x, y \in \alpha$, the following inequality holds: $$(K^{-1}) \cdot \text{edist}(f(x), f(y)) \leq \text{edist}(x, y)$$ where $K^{-1}$ is the multiplicative inverse of $K$ in the extended nonnegative real numbers $\mathbb{R}_{\geq 0} \cup \{\infty\}$.

LipschitzWith.of_edist_le theorem

(h : ∀ x y, edist (f x) (f y) ≤ edist x y) : LipschitzWith 1 f

Full source

protected theorem of_edist_le (h : ∀ x y, edist (f x) (f y) ≤ edist x y) : LipschitzWith 1 f :=
  fun x y => by simp only [ENNReal.coe_one, one_mul, h]

Lipschitz condition with constant 1 via extended distance bound

Informal description

A function $f : \alpha \to \beta$ between two (extended) metric spaces is Lipschitz continuous with constant $K = 1$ if for all $x, y \in \alpha$, the extended distance satisfies $\text{edist}(f x, f y) \leq \text{edist}(x, y)$.

LipschitzWith.weaken theorem

(hf : LipschitzWith K f) {K' : ℝ≥0} (h : K ≤ K') : LipschitzWith K' f

Full source

protected theorem weaken (hf : LipschitzWith K f) {K' : ℝ≥0} (h : K ≤ K') : LipschitzWith K' f :=
  fun x y => le_trans (hf x y) <| mul_right_mono (ENNReal.coe_le_coe.2 h)

Weakening of Lipschitz Constant for Lipschitz Continuous Functions

Informal description

If a function $f : \alpha \to \beta$ between two (extended) metric spaces is Lipschitz continuous with constant $K \geq 0$, and $K' \geq 0$ satisfies $K \leq K'$, then $f$ is also Lipschitz continuous with constant $K'$.

LipschitzWith.ediam_image_le theorem

(hf : LipschitzWith K f) (s : Set α) : EMetric.diam (f '' s) ≤ K * EMetric.diam s

Full source

theorem ediam_image_le (hf : LipschitzWith K f) (s : Set α) :
    EMetric.diam (f '' s) ≤ K * EMetric.diam s := by
  apply EMetric.diam_le
  rintro _ ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩
  exact hf.edist_le_mul_of_le (EMetric.edist_le_diam_of_mem hx hy)

Lipschitz Image Diameter Bound: $\text{diam}(f(s)) \leq K \cdot \text{diam}(s)$

Informal description

Let $f \colon \alpha \to \beta$ be a Lipschitz continuous function with constant $K \geq 0$ between two extended metric spaces. For any subset $s \subseteq \alpha$, the extended diameter of the image $f(s)$ satisfies $\text{diam}(f(s)) \leq K \cdot \text{diam}(s)$.

LipschitzWith.edist_lt_of_edist_lt_div theorem

(hf : LipschitzWith K f) {x y : α} {d : ℝ≥0∞} (h : edist x y < d / K) : edist (f x) (f y) < d

Full source

theorem edist_lt_of_edist_lt_div (hf : LipschitzWith K f) {x y : α} {d : ℝ≥0∞}
    (h : edist x y < d / K) : edist (f x) (f y) < d :=
  calc
    edist (f x) (f y) ≤ K * edist x y := hf x y
    _ < d := ENNReal.mul_lt_of_lt_div' h

Lipschitz Distance Bound: $\text{edist}(x,y) < d/K \Rightarrow \text{edist}(f x, f y) < d$

Informal description

Let $f \colon \alpha \to \beta$ be a Lipschitz continuous function with constant $K \geq 0$ between two extended metric spaces. For any points $x, y \in \alpha$ and any extended nonnegative real number $d$, if the extended distance between $x$ and $y$ satisfies $\text{edist}(x, y) < d / K$, then the extended distance between their images satisfies $\text{edist}(f x, f y) < d$.

LipschitzWith.uniformContinuous theorem

(hf : LipschitzWith K f) : UniformContinuous f

Full source

/-- A Lipschitz function is uniformly continuous. -/
protected theorem uniformContinuous (hf : LipschitzWith K f) : UniformContinuous f :=
  EMetric.uniformContinuous_iff.2 fun ε εpos =>
    ⟨ε / K, ENNReal.div_pos_iff.2 ⟨ne_of_gt εpos, ENNReal.coe_ne_top⟩, hf.edist_lt_of_edist_lt_div⟩

Lipschitz Continuous Functions are Uniformly Continuous

Informal description

Let $f \colon \alpha \to \beta$ be a Lipschitz continuous function with constant $K \geq 0$ between two (extended) metric spaces. Then $f$ is uniformly continuous.

LipschitzWith.continuous theorem

(hf : LipschitzWith K f) : Continuous f

Full source

/-- A Lipschitz function is continuous. -/
protected theorem continuous (hf : LipschitzWith K f) : Continuous f :=
  hf.uniformContinuous.continuous

Lipschitz Continuous Functions are Continuous

Informal description

Let $f \colon \alpha \to \beta$ be a Lipschitz continuous function with constant $K \geq 0$ between two (extended) metric spaces. Then $f$ is continuous.

LipschitzWith.const theorem

(b : β) : LipschitzWith 0 fun _ : α => b

Full source

/-- Constant functions are Lipschitz (with any constant). -/
protected theorem const (b : β) : LipschitzWith 0 fun _ : α => b := fun x y => by
  simp only [edist_self, zero_le]

Constant Functions are $0$-Lipschitz

Informal description

For any constant function $f : \alpha \to \beta$ defined by $f(x) = b$ for some $b \in \beta$, $f$ is Lipschitz continuous with constant $0$. In other words, for all $x, y \in \alpha$, the inequality $\text{edist}(f(x), f(y)) \leq 0 \cdot \text{edist}(x, y)$ holds.

LipschitzWith.const' theorem

(b : β) {K : ℝ≥0} : LipschitzWith K fun _ : α => b

Full source

protected theorem const' (b : β) {K : ℝ≥0} : LipschitzWith K fun _ : α => b := fun x y => by
  simp only [edist_self, zero_le]

Constant Function is Lipschitz Continuous with Any Constant $K \geq 0$

Informal description

For any constant function $f : \alpha \to \beta$ defined by $f(x) = b$ for some $b \in \beta$ and any nonnegative real number $K \geq 0$, the function $f$ is Lipschitz continuous with constant $K$.

LipschitzWith.id theorem

: LipschitzWith 1 (@id α)

Full source

/-- The identity is 1-Lipschitz. -/
protected theorem id : LipschitzWith 1 (@id α) :=
  LipschitzWith.of_edist_le fun _ _ => le_rfl

Identity Function is 1-Lipschitz

Informal description

The identity function $\mathrm{id} : \alpha \to \alpha$ on an (extended) metric space $\alpha$ is Lipschitz continuous with constant $1$, i.e., for all $x, y \in \alpha$, we have $\mathrm{edist}(\mathrm{id}(x), \mathrm{id}(y)) \leq \mathrm{edist}(x, y)$.

LipschitzWith.subtype_val theorem

(s : Set α) : LipschitzWith 1 (Subtype.val : s → α)

Full source

/-- The inclusion of a subset is 1-Lipschitz. -/
protected theorem subtype_val (s : Set α) : LipschitzWith 1 (Subtype.val : s → α) :=
  LipschitzWith.of_edist_le fun _ _ => le_rfl

Inclusion Map is 1-Lipschitz

Informal description

For any subset $s$ of a metric space $\alpha$, the inclusion map $\text{Subtype.val} : s \to \alpha$ is Lipschitz continuous with constant $1$, i.e., for all $x, y \in s$, the distance satisfies $\text{dist}(x, y) \leq \text{dist}(x, y)$.

LipschitzWith.subtype_mk theorem

 (hf : LipschitzWith K f) {p : β → Prop} (hp : ∀ x, p (f x)) : LipschitzWith K (fun x => ⟨f x, hp x⟩ : α → { y // p y })

Full source

theorem subtype_mk (hf : LipschitzWith K f) {p : β → Prop} (hp : ∀ x, p (f x)) :
    LipschitzWith K (fun x => ⟨f x, hp x⟩ : α → { y // p y }) :=
  hf

Lipschitz continuity is preserved under restriction to a subtype

Informal description

Let $f : \alpha \to \beta$ be a Lipschitz continuous function with constant $K \geq 0$, and let $p : \beta \to \text{Prop}$ be a predicate such that $p(f x)$ holds for all $x \in \alpha$. Then the function $\lambda x, \langle f x, hp x \rangle : \alpha \to \{y \in \beta \mid p y\}$ is also Lipschitz continuous with the same constant $K$.

LipschitzWith.eval theorem

 {α : ι → Type u} [∀ i, PseudoEMetricSpace (α i)] [Fintype ι] (i : ι) :
  LipschitzWith 1 (Function.eval i : (∀ i, α i) → α i)

Full source

protected theorem eval {α : ι → Type u} [∀ i, PseudoEMetricSpace (α i)] [Fintype ι] (i : ι) :
    LipschitzWith 1 (Function.eval i : (∀ i, α i) → α i) :=
  LipschitzWith.of_edist_le fun f g => by convert edist_le_pi_edist f g i

1-Lipschitz Continuity of Evaluation Maps on Finite Product Spaces

Informal description

Let $\{\alpha_i\}_{i \in \iota}$ be a family of pseudo-extended metric spaces indexed by a finite type $\iota$. For any fixed index $i \in \iota$, the evaluation map $\operatorname{eval}_i : (\prod_{i \in \iota} \alpha_i) \to \alpha_i$, defined by $\operatorname{eval}_i(f) = f(i)$, is Lipschitz continuous with constant $1$. That is, for all $f, g \in \prod_{i \in \iota} \alpha_i$, we have: \[ \text{edist}(\operatorname{eval}_i(f), \operatorname{eval}_i(g)) \leq \text{edist}(f, g). \]

LipschitzWith.restrict theorem

(hf : LipschitzWith K f) (s : Set α) : LipschitzWith K (s.restrict f)

Full source

/-- The restriction of a `K`-Lipschitz function is `K`-Lipschitz. -/
protected theorem restrict (hf : LipschitzWith K f) (s : Set α) : LipschitzWith K (s.restrict f) :=
  fun x y => hf x y

Restriction of a Lipschitz Continuous Function Preserves Lipschitz Constant

Informal description

If a function $f \colon \alpha \to \beta$ is Lipschitz continuous with constant $K \geq 0$, then its restriction to any subset $s \subseteq \alpha$ is also Lipschitz continuous with the same constant $K$.

LipschitzWith.comp theorem

 {Kf Kg : ℝ≥0} {f : β → γ} {g : α → β} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :
  LipschitzWith (Kf * Kg) (f ∘ g)

Full source

/-- The composition of Lipschitz functions is Lipschitz. -/
protected theorem comp {Kf Kg : ℝ≥0} {f : β → γ} {g : α → β} (hf : LipschitzWith Kf f)
    (hg : LipschitzWith Kg g) : LipschitzWith (Kf * Kg) (f ∘ g) := fun x y =>
  calc
    edist (f (g x)) (f (g y)) ≤ Kf * edist (g x) (g y) := hf _ _
    _ ≤ Kf * (Kg * edist x y) := mul_left_mono (hg _ _)
    _ = (Kf * Kg : ℝ≥0) * edist x y := by rw [← mul_assoc, ENNReal.coe_mul]

Composition of Lipschitz Continuous Functions is Lipschitz with Product Constant

Informal description

Let $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$ be Lipschitz continuous functions with constants $K_f \geq 0$ and $K_g \geq 0$ respectively. Then the composition $f \circ g \colon \alpha \to \gamma$ is Lipschitz continuous with constant $K_f \cdot K_g$.

LipschitzWith.comp_lipschitzOnWith theorem

 {Kf Kg : ℝ≥0} {f : β → γ} {g : α → β} {s : Set α} (hf : LipschitzWith Kf f) (hg : LipschitzOnWith Kg g s) :
  LipschitzOnWith (Kf * Kg) (f ∘ g) s

Full source

theorem comp_lipschitzOnWith {Kf Kg : ℝ≥0} {f : β → γ} {g : α → β} {s : Set α}
    (hf : LipschitzWith Kf f) (hg : LipschitzOnWith Kg g s) : LipschitzOnWith (Kf * Kg) (f ∘ g) s :=
  lipschitzOnWith_iff_restrict.mpr <| hf.comp hg.to_restrict

Composition of Lipschitz Continuous Function with Lipschitz Continuous Function on a Set

Informal description

Let $f \colon \beta \to \gamma$ be a Lipschitz continuous function with constant $K_f \geq 0$, and let $g \colon \alpha \to \beta$ be a function that is Lipschitz continuous on a set $s \subseteq \alpha$ with constant $K_g \geq 0$. Then the composition $f \circ g$ is Lipschitz continuous on $s$ with constant $K_f \cdot K_g$.

LipschitzWith.prod_fst theorem

: LipschitzWith 1 (@Prod.fst α β)

Full source

protected theorem prod_fst : LipschitzWith 1 (@Prod.fst α β) :=
  LipschitzWith.of_edist_le fun _ _ => le_max_left _ _

First Projection is 1-Lipschitz Continuous

Informal description

The projection function $\text{fst} : \alpha \times \beta \to \alpha$ from the product of two (extended) metric spaces to the first component is Lipschitz continuous with constant $1$. That is, for any $(x_1, y_1), (x_2, y_2) \in \alpha \times \beta$, we have $\text{edist}(\text{fst}(x_1, y_1), \text{fst}(x_2, y_2)) \leq \text{edist}((x_1, y_1), (x_2, y_2))$.

LipschitzWith.prod_snd theorem

: LipschitzWith 1 (@Prod.snd α β)

Full source

protected theorem prod_snd : LipschitzWith 1 (@Prod.snd α β) :=
  LipschitzWith.of_edist_le fun _ _ => le_max_right _ _

Lipschitz continuity of the second projection with constant 1

Informal description

The second projection function $\text{snd} : \alpha \times \beta \to \beta$ is Lipschitz continuous with constant $K = 1$ with respect to the product metric on $\alpha \times \beta$ and the metric on $\beta$. In other words, for any pairs $(x_1, y_1), (x_2, y_2) \in \alpha \times \beta$, we have $\text{dist}(y_1, y_2) \leq \text{dist}((x_1, y_1), (x_2, y_2))$.

LipschitzWith.prodMk theorem

 {f : α → β} {Kf : ℝ≥0} (hf : LipschitzWith Kf f) {g : α → γ} {Kg : ℝ≥0} (hg : LipschitzWith Kg g) :
  LipschitzWith (max Kf Kg) fun x => (f x, g x)

Full source

/-- If `f` and `g` are Lipschitz functions, so is the induced map `f × g` to the product type. -/
protected theorem prodMk {f : α → β} {Kf : ℝ≥0} (hf : LipschitzWith Kf f) {g : α → γ} {Kg : ℝ≥0}
    (hg : LipschitzWith Kg g) : LipschitzWith (max Kf Kg) fun x => (f x, g x) := by
  intro x y
  rw [ENNReal.coe_mono.map_max, Prod.edist_eq, max_mul]
  exact max_le_max (hf x y) (hg x y)

Lipschitz continuity of the product map: $\text{Lip}(f \times g) \leq \max(\text{Lip}(f), \text{Lip}(g))$

Informal description

Let $f : \alpha \to \beta$ and $g : \alpha \to \gamma$ be Lipschitz continuous functions with constants $K_f$ and $K_g$ respectively. Then the induced map $x \mapsto (f(x), g(x))$ from $\alpha$ to $\beta \times \gamma$ is Lipschitz continuous with constant $\max(K_f, K_g)$.

LipschitzWith.prodMk_left theorem

(a : α) : LipschitzWith 1 (Prod.mk a : β → α × β)

Full source

protected theorem prodMk_left (a : α) : LipschitzWith 1 (Prod.mk a : β → α × β) := by
  simpa only [max_eq_right zero_le_one] using (LipschitzWith.const a).prodMk LipschitzWith.id

Left Projection is 1-Lipschitz

Informal description

For any fixed element $a \in \alpha$, the function $f : \beta \to \alpha \times \beta$ defined by $f(b) = (a, b)$ is Lipschitz continuous with constant $1$. That is, for all $b_1, b_2 \in \beta$, we have $\text{dist}((a, b_1), (a, b_2)) \leq \text{dist}(b_1, b_2)$.

LipschitzWith.prodMk_right theorem

(b : β) : LipschitzWith 1 fun a : α => (a, b)

Full source

protected theorem prodMk_right (b : β) : LipschitzWith 1 fun a : α => (a, b) := by
  simpa only [max_eq_left zero_le_one] using LipschitzWith.id.prodMk (LipschitzWith.const b)

Right Projection is 1-Lipschitz

Informal description

For any fixed element $b \in \beta$, the function $f \colon \alpha \to \alpha \times \beta$ defined by $f(a) = (a, b)$ is Lipschitz continuous with constant $1$. That is, for all $a_1, a_2 \in \alpha$, we have $\text{edist}(f(a_1), f(a_2)) \leq \text{edist}(a_1, a_2)$.

LipschitzWith.uncurry theorem

 {f : α → β → γ} {Kα Kβ : ℝ≥0} (hα : ∀ b, LipschitzWith Kα fun a => f a b) (hβ : ∀ a, LipschitzWith Kβ (f a)) :
  LipschitzWith (Kα + Kβ) (Function.uncurry f)

Full source

protected theorem uncurry {f : α → β → γ} {Kα Kβ : ℝ≥0} (hα : ∀ b, LipschitzWith Kα fun a => f a b)
    (hβ : ∀ a, LipschitzWith Kβ (f a)) : LipschitzWith (Kα + Kβ) (Function.uncurry f) := by
  rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩
  simp only [Function.uncurry, ENNReal.coe_add, add_mul]
  apply le_trans (edist_triangle _ (f a₂ b₁) _)
  exact
    add_le_add (le_trans (hα _ _ _) <| mul_left_mono <| le_max_left _ _)
      (le_trans (hβ _ _ _) <| mul_left_mono <| le_max_right _ _)

Lipschitz continuity of uncurried function with sum constant

Informal description

Let $f : \alpha \to \beta \to \gamma$ be a function between metric spaces, and let $K_\alpha, K_\beta \geq 0$ be constants. If for every $b \in \beta$, the function $a \mapsto f(a, b)$ is Lipschitz continuous with constant $K_\alpha$, and for every $a \in \alpha$, the function $f(a)$ is Lipschitz continuous with constant $K_\beta$, then the uncurried function $(a, b) \mapsto f(a, b)$ is Lipschitz continuous with constant $K_\alpha + K_\beta$.

LipschitzWith.iterate theorem

{f : α → α} (hf : LipschitzWith K f) : ∀ n, LipschitzWith (K ^ n) f^[n]

Full source

/-- Iterates of a Lipschitz function are Lipschitz. -/
protected theorem iterate {f : α → α} (hf : LipschitzWith K f) : ∀ n, LipschitzWith (K ^ n) f^[n]
  | 0 => by simpa only [pow_zero] using LipschitzWith.id
  | n + 1 => by rw [pow_succ]; exact (LipschitzWith.iterate hf n).comp hf

Lipschitz continuity of iterated functions: $\text{Lip}(f^{[n]}) \leq K^n$

Informal description

Let $f \colon \alpha \to \alpha$ be a Lipschitz continuous function with constant $K \geq 0$ on a metric space $\alpha$. Then for any natural number $n$, the $n$-th iterate $f^{[n]}$ of $f$ is Lipschitz continuous with constant $K^n$.

LipschitzWith.edist_iterate_succ_le_geometric theorem

{f : α → α} (hf : LipschitzWith K f) (x n) : edist (f^[n] x) (f^[n + 1] x) ≤ edist x (f x) * (K : ℝ≥0∞) ^ n

Full source

theorem edist_iterate_succ_le_geometric {f : α → α} (hf : LipschitzWith K f) (x n) :
    edist (f^[n] x) (f^[n + 1] x) ≤ edist x (f x) * (K : ℝ≥0∞) ^ n := by
  rw [iterate_succ, mul_comm]
  simpa only [ENNReal.coe_pow] using (hf.iterate n) x (f x)

Geometric Bound on Iterated Function Distances: $\text{edist}(f^{[n]}(x), f^{[n+1]}(x)) \leq \text{edist}(x, f(x)) \cdot K^n$

Informal description

Let $f \colon \alpha \to \alpha$ be a Lipschitz continuous function with constant $K \geq 0$ on an extended metric space $\alpha$. Then for any point $x \in \alpha$ and natural number $n$, the extended distance between the $n$-th and $(n+1)$-th iterates of $f$ at $x$ satisfies the inequality: \[ \text{edist}(f^{[n]}(x), f^{[n+1]}(x)) \leq \text{edist}(x, f(x)) \cdot K^n. \]

LipschitzWith.mul_end theorem

 {f g : Function.End α} {Kf Kg} (hf : LipschitzWith Kf f) (hg : LipschitzWith Kg g) :
  LipschitzWith (Kf * Kg) (f * g : Function.End α)

Full source

protected theorem mul_end {f g : Function.End α} {Kf Kg} (hf : LipschitzWith Kf f)
    (hg : LipschitzWith Kg g) : LipschitzWith (Kf * Kg) (f * g : Function.End α) :=
  hf.comp hg

Product of Lipschitz Continuous Endomorphisms is Lipschitz with Product Constant

Informal description

Let $f, g \colon \alpha \to \alpha$ be Lipschitz continuous functions with constants $K_f \geq 0$ and $K_g \geq 0$ respectively. Then the product function $f \cdot g \colon \alpha \to \alpha$ is Lipschitz continuous with constant $K_f \cdot K_g$.

LipschitzWith.list_prod theorem

 (f : ι → Function.End α) (K : ι → ℝ≥0) (h : ∀ i, LipschitzWith (K i) (f i)) :
  ∀ l : List ι, LipschitzWith (l.map K).prod (l.map f).prod

Full source

/-- The product of a list of Lipschitz continuous endomorphisms is a Lipschitz continuous
endomorphism. -/
protected theorem list_prod (f : ι → Function.End α) (K : ι → ℝ≥0)
    (h : ∀ i, LipschitzWith (K i) (f i)) : ∀ l : List ι, LipschitzWith (l.map K).prod (l.map f).prod
  | [] => by simpa using LipschitzWith.id
  | i::l => by
    simp only [List.map_cons, List.prod_cons]
    exact (h i).mul_end (LipschitzWith.list_prod f K h l)

Lipschitz Property of Product of Lipschitz Endomorphisms

Informal description

Let $\alpha$ be an (extended) metric space and $\iota$ be an index type. Given a family of functions $f_i \colon \alpha \to \alpha$ and constants $K_i \geq 0$ for each $i \in \iota$, such that each $f_i$ is Lipschitz continuous with constant $K_i$, then for any list $l$ of indices in $\iota$, the product of the corresponding functions $\prod_{i \in l} f_i$ is Lipschitz continuous with constant $\prod_{i \in l} K_i$.

LipschitzWith.pow_end theorem

{f : Function.End α} {K} (h : LipschitzWith K f) : ∀ n : ℕ, LipschitzWith (K ^ n) (f ^ n : Function.End α)

Full source

protected theorem pow_end {f : Function.End α} {K} (h : LipschitzWith K f) :
    ∀ n : ℕ, LipschitzWith (K ^ n) (f ^ n : Function.End α)
  | 0 => by simpa only [pow_zero] using LipschitzWith.id
  | n + 1 => by
    rw [pow_succ, pow_succ]
    exact (LipschitzWith.pow_end h n).mul_end h

Lipschitz Constant of Iterated Function: $K^n$ for $f^n$

Informal description

Let $f \colon \alpha \to \alpha$ be a Lipschitz continuous function with constant $K \geq 0$. Then for any natural number $n$, the $n$-th iterate $f^n$ of $f$ is Lipschitz continuous with constant $K^n$.

LipschitzOnWith.uniformContinuousOn theorem

(hf : LipschitzOnWith K f s) : UniformContinuousOn f s

Full source

protected theorem uniformContinuousOn (hf : LipschitzOnWith K f s) : UniformContinuousOn f s :=
  uniformContinuousOn_iff_restrict.mpr hf.to_restrict.uniformContinuous

Lipschitz continuity on a set implies uniform continuity on that set

Informal description

Let $f \colon \alpha \to \beta$ be a function between (extended) metric spaces, and let $s \subseteq \alpha$. If $f$ is Lipschitz continuous on $s$ with constant $K \geq 0$, then $f$ is uniformly continuous on $s$.

LipschitzOnWith.continuousOn theorem

(hf : LipschitzOnWith K f s) : ContinuousOn f s

Full source

protected theorem continuousOn (hf : LipschitzOnWith K f s) : ContinuousOn f s :=
  hf.uniformContinuousOn.continuousOn

Lipschitz continuity on a set implies continuity on that set

Informal description

Let $f \colon \alpha \to \beta$ be a function between (extended) metric spaces, and let $s \subseteq \alpha$. If $f$ is Lipschitz continuous on $s$ with constant $K \geq 0$, then $f$ is continuous on $s$.

LipschitzOnWith.edist_le_mul_of_le theorem

 (h : LipschitzOnWith K f s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) {r : ℝ≥0∞} (hr : edist x y ≤ r) :
  edist (f x) (f y) ≤ K * r

Full source

theorem edist_le_mul_of_le (h : LipschitzOnWith K f s) {x y : α} (hx : x ∈ s) (hy : y ∈ s)
    {r : ℝ≥0∞} (hr : edist x y ≤ r) :
    edist (f x) (f y) ≤ K * r :=
  (h hx hy).trans <| mul_left_mono hr

Lipschitz condition implies extended distance bound: $\text{edist}(f(x), f(y)) \leq K \cdot r$

Informal description

Let $f : \alpha \to \beta$ be a function between extended metric spaces, and let $s$ be a subset of $\alpha$. If $f$ is Lipschitz continuous on $s$ with constant $K \geq 0$, then for any $x, y \in s$ and any extended nonnegative real number $r$ such that the extended distance $\text{edist}(x, y) \leq r$, the extended distance between the images satisfies $\text{edist}(f(x), f(y)) \leq K \cdot r$.

LipschitzOnWith.edist_lt_of_edist_lt_div theorem

 (hf : LipschitzOnWith K f s) {x y : α} (hx : x ∈ s) (hy : y ∈ s) {d : ℝ≥0∞} (hd : edist x y < d / K) :
  edist (f x) (f y) < d

Full source

theorem edist_lt_of_edist_lt_div (hf : LipschitzOnWith K f s) {x y : α} (hx : x ∈ s) (hy : y ∈ s)
    {d : ℝ≥0∞} (hd : edist x y < d / K) : edist (f x) (f y) < d :=
   hf.to_restrict.edist_lt_of_edist_lt_div <|
    show edist (⟨x, hx⟩ : s) ⟨y, hy⟩ < d / K from hd

Lipschitz condition implies $\text{edist}(f(x), f(y)) < d$ when $\text{edist}(x,y) < d/K$ on a set

Informal description

Let $f \colon \alpha \to \beta$ be a function between extended metric spaces that is Lipschitz continuous on a set $s \subseteq \alpha$ with constant $K \geq 0$. For any points $x, y \in s$ and any extended nonnegative real number $d$, if the extended distance between $x$ and $y$ satisfies $\text{edist}(x, y) < d / K$, then the extended distance between their images satisfies $\text{edist}(f(x), f(y)) < d$.

LipschitzOnWith.comp theorem

 {g : β → γ} {t : Set β} {Kg : ℝ≥0} (hg : LipschitzOnWith Kg g t) (hf : LipschitzOnWith K f s) (hmaps : MapsTo f s t) :
  LipschitzOnWith (Kg * K) (g ∘ f) s

Full source

protected theorem comp {g : β → γ} {t : Set β} {Kg : ℝ≥0} (hg : LipschitzOnWith Kg g t)
    (hf : LipschitzOnWith K f s) (hmaps : MapsTo f s t) : LipschitzOnWith (Kg * K) (g ∘ f) s :=
  lipschitzOnWith_iff_restrict.mpr <| hg.to_restrict.comp (hf.to_restrict_mapsTo hmaps)

Composition of Lipschitz Continuous Functions on Sets with Product Constant

Informal description

Let $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$ be functions between (extended) metric spaces, and let $s \subseteq \alpha$, $t \subseteq \beta$ be subsets. If $f$ is Lipschitz continuous on $s$ with constant $K \geq 0$, $g$ is Lipschitz continuous on $t$ with constant $K_g \geq 0$, and $f$ maps $s$ into $t$, then the composition $g \circ f$ is Lipschitz continuous on $s$ with constant $K_g \cdot K$.

LipschitzOnWith.prodMk theorem

 {g : α → γ} {Kf Kg : ℝ≥0} (hf : LipschitzOnWith Kf f s) (hg : LipschitzOnWith Kg g s) :
  LipschitzOnWith (max Kf Kg) (fun x => (f x, g x)) s

Full source

/-- If `f` and `g` are Lipschitz on `s`, so is the induced map `f × g` to the product type. -/
protected theorem prodMk {g : α → γ} {Kf Kg : ℝ≥0} (hf : LipschitzOnWith Kf f s)
    (hg : LipschitzOnWith Kg g s) : LipschitzOnWith (max Kf Kg) (fun x => (f x, g x)) s := by
  intro _ hx _ hy
  rw [ENNReal.coe_mono.map_max, Prod.edist_eq, max_mul]
  exact max_le_max (hf hx hy) (hg hx hy)

Lipschitz Continuity of Product Map: $\max(K_f, K_g)$

Informal description

Let $f : \alpha \to \beta$ and $g : \alpha \to \gamma$ be functions between (extended) metric spaces, and let $s \subseteq \alpha$ be a subset. If $f$ is Lipschitz continuous on $s$ with constant $K_f \geq 0$ and $g$ is Lipschitz continuous on $s$ with constant $K_g \geq 0$, then the product map $x \mapsto (f(x), g(x))$ is Lipschitz continuous on $s$ with constant $\max(K_f, K_g)$.

LipschitzOnWith.ediam_image2_le theorem

 (f : α → β → γ) {K₁ K₂ : ℝ≥0} (s : Set α) (t : Set β) (hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (f · b) s)
  (hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t) :
  EMetric.diam (Set.image2 f s t) ≤ ↑K₁ * EMetric.diam s + ↑K₂ * EMetric.diam t

Full source

theorem ediam_image2_le (f : α → β → γ) {K₁ K₂ : ℝ≥0} (s : Set α) (t : Set β)
    (hf₁ : ∀ b ∈ t, LipschitzOnWith K₁ (f · b) s) (hf₂ : ∀ a ∈ s, LipschitzOnWith K₂ (f a) t) :
    EMetric.diam (Set.image2 f s t) ≤ ↑K₁ * EMetric.diam s + ↑K₂ * EMetric.diam t := by
  simp only [EMetric.diam_le_iff, forall_mem_image2]
  intro a₁ ha₁ b₁ hb₁ a₂ ha₂ b₂ hb₂
  refine (edist_triangle _ (f a₂ b₁) _).trans ?_
  exact
    add_le_add
      ((hf₁ b₁ hb₁ ha₁ ha₂).trans <| mul_left_mono <| EMetric.edist_le_diam_of_mem ha₁ ha₂)
      ((hf₂ a₂ ha₂ hb₁ hb₂).trans <| mul_left_mono <| EMetric.edist_le_diam_of_mem hb₁ hb₂)

Diameter Bound for Image of a Bilipschitz Function on Sets

Informal description

Let $f : \alpha \to \beta \to \gamma$ be a function between (extended) metric spaces, and let $s \subseteq \alpha$, $t \subseteq \beta$ be subsets. Suppose that for every $b \in t$, the function $f(\cdot, b)$ is Lipschitz continuous on $s$ with constant $K_1 \geq 0$, and for every $a \in s$, the function $f(a, \cdot)$ is Lipschitz continuous on $t$ with constant $K_2 \geq 0$. Then the diameter of the image $\text{image2}(f, s, t)$ satisfies the inequality: \[ \text{diam}(\text{image2}(f, s, t)) \leq K_1 \cdot \text{diam}(s) + K_2 \cdot \text{diam}(t). \]

LipschitzWith.locallyLipschitz theorem

{K : ℝ≥0} (hf : LipschitzWith K f) : LocallyLipschitz f

Full source

/-- A Lipschitz function is locally Lipschitz. -/
protected lemma _root_.LipschitzWith.locallyLipschitz {K : ℝ≥0} (hf : LipschitzWith K f) :
    LocallyLipschitz f :=
  fun _ ↦ ⟨K, univ, Filter.univ_mem, lipschitzOnWith_univ.mpr hf⟩

Lipschitz continuity implies local Lipschitz continuity

Informal description

If a function $f \colon \alpha \to \beta$ between two (extended) metric spaces is Lipschitz continuous with constant $K \geq 0$, then it is locally Lipschitz continuous.

LocallyLipschitz.id theorem

: LocallyLipschitz (@id α)

Full source

/-- The identity function is locally Lipschitz. -/
protected lemma id : LocallyLipschitz (@id α) := LipschitzWith.id.locallyLipschitz

Identity Function is Locally Lipschitz Continuous

Informal description

The identity function $\mathrm{id} : \alpha \to \alpha$ on an (extended) metric space $\alpha$ is locally Lipschitz continuous. That is, for every point $x \in \alpha$, there exists a neighborhood of $x$ on which $\mathrm{id}$ is Lipschitz continuous with some constant $K \geq 0$.

LocallyLipschitz.const theorem

(b : β) : LocallyLipschitz (fun _ : α ↦ b)

Full source

/-- Constant functions are locally Lipschitz. -/
protected lemma const (b : β) : LocallyLipschitz (fun _ : α ↦ b) :=
  (LipschitzWith.const b).locallyLipschitz

Constant Functions are Locally Lipschitz Continuous

Informal description

For any constant function $f : \alpha \to \beta$ defined by $f(x) = b$ for some fixed $b \in \beta$, the function $f$ is locally Lipschitz continuous.

LocallyLipschitz.continuous theorem

{f : α → β} (hf : LocallyLipschitz f) : Continuous f

Full source

/-- A locally Lipschitz function is continuous. (The converse is false: for example,
$x ↦ \sqrt{x}$ is continuous, but not locally Lipschitz at 0.) -/
protected theorem continuous {f : α → β} (hf : LocallyLipschitz f) : Continuous f := by
  rw [continuous_iff_continuousAt]
  intro x
  rcases (hf x) with ⟨K, t, ht, hK⟩
  exact (hK.continuousOn).continuousAt ht

Continuity of Locally Lipschitz Functions

Informal description

If a function $f \colon \alpha \to \beta$ between (extended) metric spaces is locally Lipschitz continuous, then it is continuous.

LocallyLipschitz.comp theorem

{f : β → γ} {g : α → β} (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) : LocallyLipschitz (f ∘ g)

Full source

/-- The composition of locally Lipschitz functions is locally Lipschitz. -/
protected lemma comp  {f : β → γ} {g : α → β}
    (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) : LocallyLipschitz (f ∘ g) := by
  intro x
  -- g is Lipschitz on t ∋ x, f is Lipschitz on u ∋ g(x)
  rcases hg x with ⟨Kg, t, ht, hgL⟩
  rcases hf (g x) with ⟨Kf, u, hu, hfL⟩
  refine ⟨Kf * Kg, t ∩ g⁻¹' u, inter_mem ht (hg.continuous.continuousAt hu), ?_⟩
  exact hfL.comp (hgL.mono inter_subset_left)
    ((mapsTo_preimage g u).mono_left inter_subset_right)

Composition of Locally Lipschitz Continuous Functions is Locally Lipschitz Continuous

Informal description

Let $f \colon \beta \to \gamma$ and $g \colon \alpha \to \beta$ be locally Lipschitz continuous functions between (extended) metric spaces. Then the composition $f \circ g \colon \alpha \to \gamma$ is also locally Lipschitz continuous.

LocallyLipschitz.prodMk theorem

 {f : α → β} (hf : LocallyLipschitz f) {g : α → γ} (hg : LocallyLipschitz g) : LocallyLipschitz fun x => (f x, g x)

Full source

/-- If `f` and `g` are locally Lipschitz, so is the induced map `f × g` to the product type. -/
protected lemma prodMk {f : α → β} (hf : LocallyLipschitz f) {g : α → γ} (hg : LocallyLipschitz g) :
    LocallyLipschitz fun x => (f x, g x) := by
  intro x
  rcases hf x with ⟨Kf, t₁, h₁t, hfL⟩
  rcases hg x with ⟨Kg, t₂, h₂t, hgL⟩
  refine ⟨max Kf Kg, t₁ ∩ t₂, Filter.inter_mem h₁t h₂t, ?_⟩
  exact (hfL.mono inter_subset_left).prodMk (hgL.mono inter_subset_right)

Local Lipschitz continuity of product maps

Informal description

Let $f : \alpha \to \beta$ and $g : \alpha \to \gamma$ be locally Lipschitz continuous functions between (extended) metric spaces. Then the product map $x \mapsto (f(x), g(x))$ is also locally Lipschitz continuous.

LocallyLipschitz.prodMk_left theorem

(a : α) : LocallyLipschitz (Prod.mk a : β → α × β)

Full source

protected theorem prodMk_left (a : α) : LocallyLipschitz (Prod.mk a : β → α × β) :=
  (LipschitzWith.prodMk_left a).locallyLipschitz

Local Lipschitz continuity of the left projection map $(a, \cdot)$

Informal description

For any fixed element $a$ in a metric space $\alpha$, the function $f \colon \beta \to \alpha \times \beta$ defined by $f(b) = (a, b)$ is locally Lipschitz continuous. That is, for every $b \in \beta$, there exists a neighborhood of $b$ on which $f$ is Lipschitz continuous with some constant.

LocallyLipschitz.prodMk_right theorem

(b : β) : LocallyLipschitz (fun a : α => (a, b))

Full source

protected theorem prodMk_right (b : β) : LocallyLipschitz (fun a : α => (a, b)) :=
  (LipschitzWith.prodMk_right b).locallyLipschitz

Local Lipschitz continuity of the right projection map

Informal description

For any fixed element $b \in \beta$, the function $f \colon \alpha \to \alpha \times \beta$ defined by $f(a) = (a, b)$ is locally Lipschitz continuous. That is, for every point $a \in \alpha$, there exists a neighborhood $t$ of $a$ and a constant $K \geq 0$ such that for all $a_1, a_2 \in t$, the extended distance satisfies $\text{edist}(f(a_1), f(a_2)) \leq K \cdot \text{edist}(a_1, a_2)$.

LocallyLipschitz.iterate theorem

{f : α → α} (hf : LocallyLipschitz f) : ∀ n, LocallyLipschitz f^[n]

Full source

protected theorem iterate {f : α → α} (hf : LocallyLipschitz f) : ∀ n, LocallyLipschitz f^[n]
  | 0 => by simpa only [pow_zero] using LocallyLipschitz.id
  | n + 1 => by rw [iterate_add, iterate_one]; exact (hf.iterate n).comp hf

Iterates of Locally Lipschitz Continuous Functions are Locally Lipschitz Continuous

Informal description

Let $f \colon \alpha \to \alpha$ be a locally Lipschitz continuous function between (extended) metric spaces. Then for any natural number $n$, the $n$-th iterate $f^{[n]}$ is also locally Lipschitz continuous.

LocallyLipschitz.mul_end theorem

 {f g : Function.End α} (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) : LocallyLipschitz (f * g : Function.End α)

Full source

protected theorem mul_end {f g : Function.End α} (hf : LocallyLipschitz f)
    (hg : LocallyLipschitz g) : LocallyLipschitz (f * g : Function.End α) := hf.comp hg

Product of Locally Lipschitz Continuous Endomorphisms is Locally Lipschitz Continuous

Informal description

Let $f, g \colon \alpha \to \alpha$ be locally Lipschitz continuous functions on a metric space $\alpha$. Then the product function $f \cdot g \colon \alpha \to \alpha$ is also locally Lipschitz continuous.

LocallyLipschitz.pow_end theorem

{f : Function.End α} (h : LocallyLipschitz f) : ∀ n : ℕ, LocallyLipschitz (f ^ n : Function.End α)

Full source

protected theorem pow_end {f : Function.End α} (h : LocallyLipschitz f) :
    ∀ n : ℕ, LocallyLipschitz (f ^ n : Function.End α)
  | 0 => by simpa only [pow_zero] using LocallyLipschitz.id
  | n + 1 => by
    rw [pow_succ]
    exact (h.pow_end n).mul_end h

Powers of Locally Lipschitz Continuous Endomorphisms are Locally Lipschitz Continuous

Informal description

Let $f \colon \alpha \to \alpha$ be a locally Lipschitz continuous function on a metric space $\alpha$. Then for any natural number $n$, the $n$-th power $f^n$ (i.e., the $n$-fold composition of $f$ with itself) is also locally Lipschitz continuous.

continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith theorem

 [PseudoEMetricSpace α] [TopologicalSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) {s s' : Set α} {t : Set β}
  (hs' : s' ⊆ s) (hss' : s ⊆ closure s') (K : ℝ≥0) (ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t)
  (hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s) : ContinuousOn f (s ×ˢ t)

Full source

/-- Consider a function `f : α × β → γ`. Suppose that it is continuous on each “vertical fiber”
`{a} × t`, `a ∈ s`, and is Lipschitz continuous on each “horizontal fiber” `s × {b}`, `b ∈ t`
with the same Lipschitz constant `K`. Then it is continuous on `s × t`. Moreover, it suffices
to require continuity on vertical fibers for `a` from a subset `s' ⊆ s` that is dense in `s`.

The actual statement uses (Lipschitz) continuity of `fun y ↦ f (a, y)` and `fun x ↦ f (x, b)`
instead of continuity of `f` on subsets of the product space. -/
theorem continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith [PseudoEMetricSpace α]
    [TopologicalSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) {s s' : Set α} {t : Set β}
    (hs' : s' ⊆ s) (hss' : s ⊆ closure s') (K : ℝ≥0)
    (ha : ∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t)
    (hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s) : ContinuousOn f (s ×ˢ t) := by
  rintro ⟨x, y⟩ ⟨hx : x ∈ s, hy : y ∈ t⟩
  refine EMetric.nhds_basis_closed_eball.tendsto_right_iff.2 fun ε (ε0 : 0 < ε) => ?_
  replace ε0 : 0 < ε / 2 := ENNReal.half_pos ε0.ne'
  obtain ⟨δ, δpos, hδ⟩ : ∃ δ : ℝ≥0, 0 < δ ∧ (δ : ℝ≥0∞) * ↑(3 * K) < ε / 2 :=
    ENNReal.exists_nnreal_pos_mul_lt ENNReal.coe_ne_top ε0.ne'
  rw [← ENNReal.coe_pos] at δpos
  rcases EMetric.mem_closure_iff.1 (hss' hx) δ δpos with ⟨x', hx', hxx'⟩
  have A : s ∩ EMetric.ball x δs ∩ EMetric.ball x δ ∈ 𝓝[s] x :=
    inter_mem_nhdsWithin _ (EMetric.ball_mem_nhds _ δpos)
  have B : t ∩ { b | edist (f (x', b)) (f (x', y)) ≤ ε / 2 }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))
  filter_upwards [nhdsWithin_prod A B] with ⟨a, b⟩ ⟨⟨has, hax⟩, ⟨hbt, hby⟩⟩
  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') ?_
        exact (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 _

Continuity on Product Set via Fiberwise Continuity and Lipschitz Conditions

Informal description

Let $f \colon \alpha \times \beta \to \gamma$ be a function between pseudometric spaces, where $\alpha$ and $\gamma$ are equipped with extended pseudometrics. Suppose there exist subsets $s' \subseteq s \subseteq \alpha$ and $t \subseteq \beta$ such that $s$ is contained in the closure of $s'$. If for every $a \in s'$, the function $y \mapsto f(a, y)$ is continuous on $t$, and for every $b \in t$, the function $x \mapsto f(x, b)$ is Lipschitz continuous on $s$ with a uniform Lipschitz constant $K \geq 0$, then $f$ is continuous on the product set $s \times t$.

continuousOn_prod_of_continuousOn_lipschitzOnWith theorem

 [PseudoEMetricSpace α] [TopologicalSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) {s : Set α} {t : Set β} (K : ℝ≥0)
  (ha : ∀ a ∈ s, ContinuousOn (fun y => f (a, y)) t) (hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s) :
  ContinuousOn f (s ×ˢ t)

Full source

/-- Consider a function `f : α × β → γ`. Suppose that it is continuous on each “vertical fiber”
`{a} × t`, `a ∈ s`, and is Lipschitz continuous on each “horizontal fiber” `s × {b}`, `b ∈ t`
with the same Lipschitz constant `K`. Then it is continuous on `s × t`.

The actual statement uses (Lipschitz) continuity of `fun y ↦ f (a, y)` and `fun x ↦ f (x, b)`
instead of continuity of `f` on subsets of the product space. -/
theorem continuousOn_prod_of_continuousOn_lipschitzOnWith [PseudoEMetricSpace α]
    [TopologicalSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) {s : Set α} {t : Set β} (K : ℝ≥0)
    (ha : ∀ a ∈ s, ContinuousOn (fun y => f (a, y)) t)
    (hb : ∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s) : ContinuousOn f (s ×ˢ t) :=
  continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith
    f Subset.rfl subset_closure K ha hb

Continuity on Product Set via Fiberwise Continuity and Uniform Lipschitz Condition

Informal description

Let $f \colon \alpha \times \beta \to \gamma$ be a function between pseudometric spaces, where $\alpha$ and $\gamma$ are equipped with extended pseudometrics. Suppose $s \subseteq \alpha$ and $t \subseteq \beta$ are subsets. If for every $a \in s$, the function $y \mapsto f(a, y)$ is continuous on $t$, and for every $b \in t$, the function $x \mapsto f(x, b)$ is Lipschitz continuous on $s$ with a uniform Lipschitz constant $K \geq 0$, then $f$ is continuous on the product set $s \times t$.

continuous_prod_of_dense_continuous_lipschitzWith theorem

 [PseudoEMetricSpace α] [TopologicalSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) (K : ℝ≥0) {s : Set α} (hs : Dense s)
  (ha : ∀ a ∈ s, Continuous fun y => f (a, y)) (hb : ∀ b, LipschitzWith K fun x => f (x, b)) : Continuous f

Full source

/-- Consider a function `f : α × β → γ`. Suppose that it is continuous on each “vertical section”
`{a} × univ` for `a : α` from a dense set. Suppose that it is Lipschitz continuous on each
“horizontal section” `univ × {b}`, `b : β` with the same Lipschitz constant `K`. Then it is
continuous.

The actual statement uses (Lipschitz) continuity of `fun y ↦ f (a, y)` and `fun x ↦ f (x, b)`
instead of continuity of `f` on subsets of the product space. -/
theorem continuous_prod_of_dense_continuous_lipschitzWith [PseudoEMetricSpace α]
    [TopologicalSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) (K : ℝ≥0) {s : Set α}
    (hs : Dense s) (ha : ∀ a ∈ s, Continuous fun y => f (a, y))
    (hb : ∀ b, LipschitzWith K fun x => f (x, b)) : Continuous f := by
  simp only [continuous_iff_continuousOn_univ, ← univ_prod_univ, ← lipschitzOnWith_univ] at *
  exact continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith f (subset_univ _)
    hs.closure_eq.ge K ha fun b _ => hb b

Continuity of a Function on Product Space via Dense Fiberwise Continuity and Uniform Lipschitz Condition

Informal description

Let $f \colon \alpha \times \beta \to \gamma$ be a function between pseudometric spaces, where $\alpha$ and $\gamma$ are equipped with extended pseudometrics. Suppose there exists a dense subset $s \subseteq \alpha$ such that for every $a \in s$, the function $y \mapsto f(a, y)$ is continuous on $\beta$, and for every $b \in \beta$, the function $x \mapsto f(x, b)$ is Lipschitz continuous on $\alpha$ with a uniform Lipschitz constant $K \geq 0$. Then $f$ is continuous on $\alpha \times \beta$.

continuous_prod_of_continuous_lipschitzWith theorem

 [PseudoEMetricSpace α] [TopologicalSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) (K : ℝ≥0)
  (ha : ∀ a, Continuous fun y => f (a, y)) (hb : ∀ b, LipschitzWith K fun x => f (x, b)) : Continuous f

Full source

/-- Consider a function `f : α × β → γ`. Suppose that it is continuous on each “vertical section”
`{a} × univ`, `a : α`, and is Lipschitz continuous on each “horizontal section”
`univ × {b}`, `b : β` with the same Lipschitz constant `K`. Then it is continuous.

The actual statement uses (Lipschitz) continuity of `fun y ↦ f (a, y)` and `fun x ↦ f (x, b)`
instead of continuity of `f` on subsets of the product space. -/
theorem continuous_prod_of_continuous_lipschitzWith [PseudoEMetricSpace α] [TopologicalSpace β]
    [PseudoEMetricSpace γ] (f : α × β → γ) (K : ℝ≥0) (ha : ∀ a, Continuous fun y => f (a, y))
    (hb : ∀ b, LipschitzWith K fun x => f (x, b)) : Continuous f :=
  continuous_prod_of_dense_continuous_lipschitzWith f K dense_univ (fun _ _ ↦ ha _) hb

Continuity of Product Function via Fiberwise Continuity and Uniform Lipschitz Condition

Informal description

Let $f \colon \alpha \times \beta \to \gamma$ be a function between pseudometric spaces, where $\alpha$ and $\gamma$ are equipped with extended pseudometrics. Suppose that for every $a \in \alpha$, the function $y \mapsto f(a, y)$ is continuous on $\beta$, and for every $b \in \beta$, the function $x \mapsto f(x, b)$ is Lipschitz continuous on $\alpha$ with a uniform Lipschitz constant $K \geq 0$. Then $f$ is continuous on $\alpha \times \beta$.

continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith' theorem

 [TopologicalSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) {s : Set α} {t t' : Set β}
  (ht' : t' ⊆ t) (htt' : t ⊆ closure t') (K : ℝ≥0) (ha : ∀ a ∈ s, LipschitzOnWith K (fun y => f (a, y)) t)
  (hb : ∀ b ∈ t', ContinuousOn (fun x => f (x, b)) s) : ContinuousOn f (s ×ˢ t)

Full source

theorem continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith' [TopologicalSpace α]
    [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) {s : Set α} {t t' : Set β}
    (ht' : t' ⊆ t) (htt' : t ⊆ closure t') (K : ℝ≥0)
    (ha : ∀ a ∈ s, LipschitzOnWith K (fun y => f (a, y)) t)
    (hb : ∀ b ∈ t', ContinuousOn (fun x => f (x, b)) s) : ContinuousOn f (s ×ˢ t) :=
  have : ContinuousOn (f ∘ Prod.swap) (t ×ˢ s) :=
    continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith _ ht' htt' K hb ha
  this.comp continuous_swap.continuousOn (mapsTo_swap_prod _ _)

Continuity on Product Set via Fiberwise Lipschitz and Continuous Conditions

Informal description

Let $f \colon \alpha \times \beta \to \gamma$ be a function between topological spaces, where $\beta$ and $\gamma$ are equipped with extended pseudometrics. Suppose there exist subsets $t' \subseteq t \subseteq \beta$ such that $t$ is contained in the closure of $t'$. If for every $a \in s$, the function $y \mapsto f(a, y)$ is Lipschitz continuous on $t$ with a uniform Lipschitz constant $K \geq 0$, and for every $b \in t'$, the function $x \mapsto f(x, b)$ is continuous on $s$, then $f$ is continuous on the product set $s \times t$.

continuousOn_prod_of_continuousOn_lipschitzOnWith' theorem

 [TopologicalSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) {s : Set α} {t : Set β} (K : ℝ≥0)
  (ha : ∀ a ∈ s, LipschitzOnWith K (fun y => f (a, y)) t) (hb : ∀ b ∈ t, ContinuousOn (fun x => f (x, b)) s) :
  ContinuousOn f (s ×ˢ t)

Full source

theorem continuousOn_prod_of_continuousOn_lipschitzOnWith' [TopologicalSpace α]
    [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) {s : Set α} {t : Set β} (K : ℝ≥0)
    (ha : ∀ a ∈ s, LipschitzOnWith K (fun y => f (a, y)) t)
    (hb : ∀ b ∈ t, ContinuousOn (fun x => f (x, b)) s) : ContinuousOn f (s ×ˢ t) :=
  have : ContinuousOn (f ∘ Prod.swap) (t ×ˢ s) :=
    continuousOn_prod_of_continuousOn_lipschitzOnWith _ K hb ha
  this.comp continuous_swap.continuousOn (mapsTo_swap_prod _ _)

Continuity on Product Set via Fiberwise Lipschitz and Continuous Conditions with Uniform Constant

Informal description

Let $f \colon \alpha \times \beta \to \gamma$ be a function between topological spaces, where $\beta$ and $\gamma$ are equipped with extended pseudometrics. Given subsets $s \subseteq \alpha$ and $t \subseteq \beta$, suppose that for every $a \in s$, the function $y \mapsto f(a, y)$ is Lipschitz continuous on $t$ with a uniform Lipschitz constant $K \geq 0$, and for every $b \in t$, the function $x \mapsto f(x, b)$ is continuous on $s$. Then $f$ is continuous on the product set $s \times t$.

continuous_prod_of_dense_continuous_lipschitzWith' theorem

 [TopologicalSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) (K : ℝ≥0) {t : Set β} (ht : Dense t)
  (ha : ∀ a, LipschitzWith K fun y => f (a, y)) (hb : ∀ b ∈ t, Continuous fun x => f (x, b)) : Continuous f

Full source

theorem continuous_prod_of_dense_continuous_lipschitzWith' [TopologicalSpace α]
    [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) (K : ℝ≥0) {t : Set β}
    (ht : Dense t) (ha : ∀ a, LipschitzWith K fun y => f (a, y))
    (hb : ∀ b ∈ t, Continuous fun x => f (x, b)) : Continuous f :=
  have : Continuous (f ∘ Prod.swap) :=
    continuous_prod_of_dense_continuous_lipschitzWith _ K ht hb ha
  this.comp continuous_swap

Continuity of a Function on Product Space via Dense Fiberwise Continuity and Uniform Lipschitz Condition (Variant)

Informal description

Let $\alpha$ be a topological space, and $\beta$, $\gamma$ be extended pseudometric spaces. Given a function $f \colon \alpha \times \beta \to \gamma$, a constant $K \geq 0$, and a dense subset $t \subseteq \beta$, suppose that: 1. For every $a \in \alpha$, the function $y \mapsto f(a, y)$ is Lipschitz continuous on $\beta$ with constant $K$. 2. For every $b \in t$, the function $x \mapsto f(x, b)$ is continuous on $\alpha$. Then $f$ is continuous on $\alpha \times \beta$.

continuous_prod_of_continuous_lipschitzWith' theorem

 [TopologicalSpace α] [PseudoEMetricSpace β] [PseudoEMetricSpace γ] (f : α × β → γ) (K : ℝ≥0)
  (ha : ∀ a, LipschitzWith K fun y => f (a, y)) (hb : ∀ b, Continuous fun x => f (x, b)) : Continuous f

Full source

theorem continuous_prod_of_continuous_lipschitzWith' [TopologicalSpace α] [PseudoEMetricSpace β]
    [PseudoEMetricSpace γ] (f : α × β → γ) (K : ℝ≥0) (ha : ∀ a, LipschitzWith K fun y => f (a, y))
    (hb : ∀ b, Continuous fun x => f (x, b)) : Continuous f :=
  have : Continuous (f ∘ Prod.swap) :=
    continuous_prod_of_continuous_lipschitzWith _ K hb ha
  this.comp continuous_swap

Continuity of Product Function via Uniform Lipschitz and Fiberwise Continuous Conditions

Informal description

Let $\alpha$ be a topological space, and $\beta$, $\gamma$ be extended pseudometric spaces. Given a function $f \colon \alpha \times \beta \to \gamma$ and a constant $K \geq 0$, suppose that: 1. For every $a \in \alpha$, the function $y \mapsto f(a, y)$ is Lipschitz continuous on $\beta$ with constant $K$. 2. For every $b \in \beta$, the function $x \mapsto f(x, b)$ is continuous on $\alpha$. Then $f$ is continuous on $\alpha \times \beta$.

Mathlib.Topology.EMetricSpace.Lipschitz

Main definitions and lemmas

Implementation notes