LipschitzOnWith.of_le_add_mul
theorem LipschitzOnWith.of_le_add_mul :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {f : α → ℝ} (K : NNReal),
(∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + ↑K * dist x y) → LipschitzOnWith K f s
The theorem `LipschitzOnWith.of_le_add_mul` states that for a given function `f` mapping from a set `s` in a pseudometric space `α` to real numbers, if it is known that for all `x` and `y` in `s`, `f(x)` is less than or equal to `f(y) + K * dist(x, y)`, where `K` is a non-negative real number, then the function `f` is Lipschitz continuous on `s` with Lipschitz constant `K`. This theorem simplifies the conditions for Lipschitz continuity, allowing the proof with an inequality involving function values and distances.
More concisely: If a real-valued function on a pseudometric space is known to satisfy the condition that for all x and y, |f(x) - f(y)| ≤ K * dist(x, y), then f is Lipschitz continuous on the space with constant K.
|
LipschitzOnWith.of_le_add_mul'
theorem LipschitzOnWith.of_le_add_mul' :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} {f : α → ℝ} (K : ℝ),
(∀ x ∈ s, ∀ y ∈ s, f x ≤ f y + K * dist x y) → LipschitzOnWith K.toNNReal f s
This theorem is stating that for functions mapping to the real numbers (`ℝ`), if for all `x` and `y` in a set `s`, the value of the function `f` at `x` is less than or equal to the value of `f` at `y` added to the product of a real number `K` and the distance between `x` and `y`, then the function `f` is Lipschitz continuous with constant `K` on `s`. Here, Lipschitz continuity is defined in terms of the extended metric (`edist`). The theorem does not require `K` to be non-negative.
More concisely: If a real-valued function `f` on a set `s` satisfies `|f(x) - f(y)| ≤ K * edist(x, y)` for all `x, y ∈ s`, then `f` is Lipschitz continuous on `s` with constant `K`.
|
lipschitzWith_max
theorem lipschitzWith_max : LipschitzWith 1 fun p => max p.1 p.2
The theorem `lipschitzWith_max` states that the function that takes a pair of points `p` and returns the maximum of the two points `p.1` and `p.2` is Lipschitz continuous with a Lipschitz constant of `1`. In other words, for any two pairs of points `x` and `y`, the distance between `max x.1 x.2` and `max y.1 y.2` is less than or equal to the distance between `x` and `y`.
More concisely: The function that maps a pair of real numbers to their maximum is 1-Lipschitz continuous.
|
LipschitzOnWith.extend_real
theorem LipschitzOnWith.extend_real :
∀ {α : Type u} [inst : PseudoMetricSpace α] {f : α → ℝ} {s : Set α} {K : NNReal},
LipschitzOnWith K f s → ∃ g, LipschitzWith K g ∧ Set.EqOn f g s
The theorem `LipschitzOnWith.extend_real` states that for any function `f` which maps from an arbitrary type `α` to the real numbers (`ℝ`), given that `f` is `K`-Lipschitz continuous on a subset `s` of `α`, there exists another function `g` that is `K`-Lipschitz continuous on the entire space and coincides with `f` on the subset `s`. Here, `K`-Lipschitz continuity for a function means that for every pair of points, the distance between their images under the function is at most `K` times the distance between the points themselves.
More concisely: Given a `K`-Lipschitz continuous function `f` on subset `s` of type `α`, there exists a `K`-Lipschitz continuous extension `g` of `f` to all of `α`.
|
LipschitzOnWith.dist_le_mul
theorem LipschitzOnWith.dist_le_mul :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {s : Set α}
{f : α → β}, LipschitzOnWith K f s → ∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ ↑K * dist x y
The theorem `LipschitzOnWith.dist_le_mul` states that for any Lipschitz continuous function `f` with constant `K` on a set `s` in pseudometric spaces `α` and `β`, for all `x` and `y` in `s`, the distance between `f(x)` and `f(y)` is less than or equal to `K` times the distance between `x` and `y`. This theorem is just an alias of the forward direction of another theorem `lipschitzOnWith_iff_dist_le_mul`.
More concisely: For any Lipschitz continuous function `f` with constant `K` on a set `s` in pseudometric spaces `α` and `β`, the distance `d(f(x), f(y))` between `f(x)` and `f(y)` is less than or equal to `K * d(x, y)` for all `x, y` in `s`.
|
LipschitzWith.of_le_add_mul
theorem LipschitzWith.of_le_add_mul :
∀ {α : Type u} [inst : PseudoMetricSpace α] {f : α → ℝ} (K : NNReal),
(∀ (x y : α), f x ≤ f y + ↑K * dist x y) → LipschitzWith K f
The theorem `LipschitzWith.of_le_add_mul` states that for any function `f` mapping from a space `α` to the real numbers `ℝ`, if for all `x` and `y` in `α` the function value at `x` is less than or equal to the function value at `y` plus a nonnegative real number `K` times the distance between `x` and `y`, then `f` is Lipschitz continuous with Lipschitz constant `K`. Here, `α` is a space equipped with a pseudo-metric, and Lipschitz continuity means that the distance between the function values at two points is less than or equal to `K` times the distance between the points.
More concisely: If a function from a pseudo-metric space to the real numbers satisfies the condition that the function value at any point is less than or equal to the value at another point plus a constant times the distance between them, then the function is Lipschitz continuous with the given constant as its Lipschitz constant.
|
LipschitzWith.dist_le_mul
theorem LipschitzWith.dist_le_mul :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
LipschitzWith K f → ∀ (x y : α), dist (f x) (f y) ≤ ↑K * dist x y
The theorem `LipschitzWith.dist_le_mul` asserts that for any objects `α` and `β` (which are types equipped with a pseudo metric space structure), a nonnegative real number `K`, and a function `f` mapping from `α` to `β`, if `f` is Lipschitz continuous with constant `K`, then for any two elements `x` and `y` in `α`, the distance between `f(x)` and `f(y)` is less than or equal to `K` times the distance between `x` and `y`. This theorem is a restatement or alias of the forward direction of a related theorem `lipschitzWith_iff_dist_le_mul`.
More concisely: Given types `α` and `β` with pseudo metric spaces structures, a Lipschitz continuous function `f` from `α` to `β` with constant `K`, and elements `x` and `y` in `α`, we have `dist(f(x), f(y)) ≤ K * dist(x, y)`.
|
LipschitzWith.of_dist_le'
theorem LipschitzWith.of_dist_le' :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β} {K : ℝ},
(∀ (x y : α), dist (f x) (f y) ≤ K * dist x y) → LipschitzWith K.toNNReal f
The theorem `LipschitzWith.of_dist_le'` states that for any types `α` and `β`, any pseudo metric spaces over these types, any function `f` from `α` to `β`, and any real number `K`, if for all `x` and `y` in `α`, the distance between `f(x)` and `f(y)` is less than or equal to `K` times the distance between `x` and `y`, then `f` is Lipschitz continuous with the non-negative real number equivalent of `K`. Here, the non-negative real number equivalent of `K` is obtained by taking the maximum of `K` and `0`, ensuring a non-negative result.
More concisely: If a function between pseudo metric spaces satisfies the condition that the distance between its images of any two points is less than or equal to a constant times the distance between the points, then the function is Lipschitz continuous with the given constant.
|
LipschitzWith.dist_right
theorem LipschitzWith.dist_right : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x : α), LipschitzWith 1 (dist x) := by
sorry
The theorem `LipschitzWith.dist_right` states that for any type `α` with a pseudo-metric space structure and for any point `x` of type `α`, the function that measures the distance from `x` is Lipschitz continuous with a constant of 1. This means that for any two points `y` and `z` in the pseudo-metric space, the distance between the images under the function (i.e., the absolute differences between the distances from `x` to `y` and `z`) is less than or equal to the distance between the points `y` and `z` themselves.
More concisely: For any pseudo-metric space `(α, d)` and point `x ∈ α`, the function `d(x, *) : α → ℝ` is Lipschitz continuous with constant 1, i.e., `|d(x, y) - d(x, z)| ≤ d(y, z)` for all `y, z ∈ α`.
|
LipschitzWith.of_le_add_mul'
theorem LipschitzWith.of_le_add_mul' :
∀ {α : Type u} [inst : PseudoMetricSpace α] {f : α → ℝ} (K : ℝ),
(∀ (x y : α), f x ≤ f y + K * dist x y) → LipschitzWith K.toNNReal f
The theorem `LipschitzWith.of_le_add_mul'` states that for any function `f` mapping from a pseudometric space `α` to the real numbers `ℝ`, given a real number `K`, if for all `x` and `y` in the domain `α`, the function value of `x` is less than or equal to the function value of `y` plus `K` times the distance between `x` and `y`, then `f` is Lipschitz continuous with Lipschitz constant `K` converted to a non-negative real number (i.e., `K.toNNReal`). This version of the theorem does not make the assumption that `K` is non-negative.
More concisely: If a function from a pseudometric space to the real numbers satisfies the condition that the function value of any two points is related by the triangle inequality with a constant, then the function is Lipschitz continuous with the given constant as the Lipschitz constant.
|
LipschitzWith.comap_cobounded_le
theorem LipschitzWith.comap_cobounded_le :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
LipschitzWith K f → Filter.comap f (Bornology.cobounded β) ≤ Bornology.cobounded α
The theorem `LipschitzWith.comap_cobounded_le` states that for any two types `α` and `β` equipped with a pseudo metric space structure, a nonnegative real number `K`, and a function `f` from `α` to `β`, if `f` is Lipschitz continuous with Lipschitz constant `K` (i.e., the distance between `f(x)` and `f(y)` is at most `K` times the distance between `x` and `y`), then the preimage filter under `f` of the filter of cobounded sets in the bornology of `β` is a subset of the filter of cobounded sets in the bornology of `α`. In other words, Lipschitz continuous functions preserve the structure of cobounded sets in a bornology when mapping from `β` to `α`.
More concisely: If `f: α → β` is Lipschitz continuous with constant `K` between pseudo metric spaces `(α, dα)` and `(β, dβ)`, then for any cobounded set `C ∈ bornology β`, the preimage `f⁻¹(C)` is a cobounded set in `bornology α`.
|
continuousAt_of_locally_lipschitz
theorem continuousAt_of_locally_lipschitz :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β} {x : α} {r : ℝ},
0 < r → ∀ (K : ℝ), (∀ (y : α), dist y x < r → dist (f y) (f x) ≤ K * dist y x) → ContinuousAt f x
The theorem `continuousAt_of_locally_lipschitz` states that if a function is locally Lipschitz around a point, then it is continuous at that point. More precisely, for any points in pseudometric spaces `α` and `β`, a function `f` from `α` to `β`, a point `x` from `α`, and a positive real number `r`, if for some real number `K`, the distance from any point `y` to `x` is less than `r` implies the distance from `f(y)` to `f(x)` is less than or equal to `K` times the distance from `y` to `x`, then `f` is continuous at `x`. In mathematical terms, this can be written as: if ∀ `y` in `α`, `dist y x < r` implies `dist (f y) (f x) ≤ K * dist y x`, then `f` is continuous at `x`.
More concisely: If a function is locally Lipschitz around a point, then it is continuous at that point.
|
LipschitzWith.of_dist_le_mul
theorem LipschitzWith.of_dist_le_mul :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
(∀ (x y : α), dist (f x) (f y) ≤ ↑K * dist x y) → LipschitzWith K f
The theorem `LipschitzWith.of_dist_le_mul` states that for any two types `α` and `β`, where both are equipped with a pseudo metric space structure, and for any nonnegative real number `K` and function `f` that maps `α` to `β`, if for all `x` and `y` in `α`, the distance between `f(x)` and `f(y)` is less than or equal to `K` times the distance between `x` and `y`, then the function `f` is Lipschitz continuous with constant `K`. This theorem is an alias of the reverse direction of `lipschitzWith_iff_dist_le_mul`.
More concisely: For any types equipped with pseudo metric spaces `α` and `β`, and for any function `f` from `α` to `β` and non-negative real `K`, if `d(f(x), f(y)) ≤ K * d(x, y)` for all `x, y` in `α`, then `f` is Lipschitz continuous with constant `K`.
|
LocallyLipschitz.min
theorem LocallyLipschitz.min :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {f g : α → ℝ},
LocallyLipschitz f → LocallyLipschitz g → LocallyLipschitz fun x => min (f x) (g x)
The theorem `LocallyLipschitz.min` states that the minimum of two locally Lipschitz functions is also a locally Lipschitz function. In other words, given two functions `f` and `g` from a type `α` to real numbers `ℝ`, where `α` is a pseudoemetric space, if both `f` and `g` are locally Lipschitz, then the function that maps each `x` in `α` to the minimum of `f(x)` and `g(x)` is also locally Lipschitz. Here, a function is locally Lipschitz if every point in its domain has a neighborhood on which the function is Lipschitz.
More concisely: Given two locally Lipschitz functions from a pseudometric space to real numbers, their pointwise minimum is also a locally Lipschitz function.
|
LipschitzWith.mk_one
theorem LipschitzWith.mk_one :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
(∀ (x y : α), dist (f x) (f y) ≤ dist x y) → LipschitzWith 1 f
This theorem, `LipschitzWith.mk_one`, states that for any two types `α` and `β` equipped with pseudo metric spaces, and any function `f` from `α` to `β`, if for every pair of elements `x` and `y` in `α`, the distance between `f(x)` and `f(y)` is less than or equal to the distance between `x` and `y`, then the function `f` is Lipschitz continuous with constant `1`. In mathematical terms, a function `f` is Lipschitz continuous with constant `1` if for all `x, y`, we have `d(f(x), f(y)) ≤ d(x, y)`, where `d` denotes the distance in the respective metric spaces.
More concisely: If a function between two pseudo metric spaces satisfies the condition that the distance between its images of any two points is less than or equal to the distance between the points themselves, then the function is Lipschitz continuous with constant 1.
|
LipschitzOnWith.extend_pi
theorem LipschitzOnWith.extend_pi :
∀ {α : Type u} {ι : Type x} [inst : PseudoMetricSpace α] [inst_1 : Fintype ι] {f : α → ι → ℝ} {s : Set α}
{K : NNReal}, LipschitzOnWith K f s → ∃ g, LipschitzWith K g ∧ Set.EqOn f g s
The theorem `LipschitzOnWith.extend_pi` states that if a function `f` of type `α → ι → ℝ` is `K`-Lipschitz continuous on a subset `s` of `α`, then there exists an extension of `f` to the entire space `α` that is also `K`-Lipschitz continuous and agrees with `f` on the subset `s`. This means that the function `f` can be extended in a way that preserves its Lipschitz continuity property. The same result also holds for the space `ℓ^∞ (ι, ℝ)` over a possibly infinite type `ι` as implemented in `LipschitzOnWith.extend_lp_infty`.
More concisely: Given a `K`-Lipschitz function `f` on a subset `s` of type `α`, there exists an extending function `g : α → ℝ` that is also `K`-Lipschitz and agrees with `f` on `s`. This holds for both finite and infinite types `α` and `ι` in the spaces `α → ι → ℝ` and `ℓ^∞ (ι, ℝ)`.
|
LipschitzWith.isBounded_image
theorem LipschitzWith.isBounded_image :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
LipschitzWith K f → ∀ {s : Set α}, Bornology.IsBounded s → Bornology.IsBounded (f '' s)
The theorem `LipschitzWith.isBounded_image` states that if a function `f` from a type `α` to a type `β` is Lipschitz continuous with a nonnegative real constant `K` and if a set `s` of type `α` is bounded, then the image of `s` under `f` is also bounded. Here, both `α` and `β` are equipped with pseudometric spaces and the concept of boundedness comes from a bornology on `α` and `β`. In mathematical terms, if a function satisfies a Lipschitz condition, it does not amplify the distance between two points in a set when mapping them from one space to another.
More concisely: If `f` is a Lipschitz continuous function from the bounded set `s` in the pseudometric spaces `α` and `β` with constant `K`, then the image `f''(s)` is also a bounded subset of `β`.
|
LocallyLipschitz.max
theorem LocallyLipschitz.max :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {f g : α → ℝ},
LocallyLipschitz f → LocallyLipschitz g → LocallyLipschitz fun x => max (f x) (g x)
The theorem `LocallyLipschitz.max` states that for any two functions `f` and `g` from a pseudometric space `α` to the real numbers `ℝ` that are locally Lipschitz continuous, the function that takes a point `x` in `α` to the maximum of `f(x)` and `g(x)` is also locally Lipschitz continuous. In mathematical terms, if for every point `x` in `α`, there exist a neighborhood and a constant such that `f` and `g` are Lipschitz on that neighborhood, then the same property holds for the function that yields the maximum of `f` and `g` at each point.
More concisely: If `f` and `g` are locally Lipschitz continuous functions from a pseudometric space `α` to `ℝ`, then the function `x ↦ max(f x, g x)` is also locally Lipschitz continuous.
|
LipschitzOnWith.of_dist_le_mul
theorem LipschitzOnWith.of_dist_le_mul :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {s : Set α}
{f : α → β}, (∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ ↑K * dist x y) → LipschitzOnWith K f s
This theorem, referred to as an alias of the reverse direction of `lipschitzOnWith_iff_dist_le_mul`, states that for any two types `α` and `β` with a `PseudoMetricSpace` structure, a nonnegative real number `K`, a set `s` of elements from `α`, and a function `f` from `α` to `β`, if for every pair of elements `x` and `y` from the set `s`, the distance between `f(x)` and `f(y)` is less than or equal to `K` times the distance between `x` and `y`, then the function `f` is Lipschitz continuous with constant `K` on the set `s`. In mathematical terms, a function is Lipschitz continuous on a set if there exists a nonnegative real number such that for every pair of points in the set, the distance between the images of the points under the function is less than or equal to that number times the distance between the points themselves.
More concisely: If for all x, y in a set S of a PseudoMetricSpace (α), the distance between f(x) and f(y) is less than or equal to K times the distance between x and y, then f is Lipschitz continuous on S with constant K.
|
LipschitzWith.dist_le_mul_of_le
theorem LipschitzWith.dist_le_mul_of_le :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β}
{x y : α} {r : ℝ}, LipschitzWith K f → dist x y ≤ r → dist (f x) (f y) ≤ ↑K * r
The theorem `LipschitzWith.dist_le_mul_of_le` states that, for all types `α` and `β` equipped with a pseudometric space structure, a nonnegative real number `K`, a function `f` from `α` to `β`, elements `x` and `y` of `α`, and a real number `r`, if the function `f` is Lipschitz continuous with constant `K` and the distance between `x` and `y` is less than or equal to `r`, then the distance between `f(x)` and `f(y)` is less than or equal to `K` times `r`. In other words, the distance between the images under a Lipschitz continuous function does not exceed the Lipschitz constant times the original distance.
More concisely: For all pseudometric spaces (α, d\_α) and (β, d\_β), and for all Lipschitz continuous functions f : α --> β with constant K, x, y in α, and r in R, if d\_α(x, y) <= r then d\_β(f(x), f(y)) <= K * r.
|
lipschitzWith_iff_dist_le_mul
theorem lipschitzWith_iff_dist_le_mul :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {K : NNReal} {f : α → β},
LipschitzWith K f ↔ ∀ (x y : α), dist (f x) (f y) ≤ ↑K * dist x y
The theorem `lipschitzWith_iff_dist_le_mul` states that for any two types `α` and `β`, given that they are instances of a PseudoMetricSpace, and given a nonnegative real number `K` and a function `f` from `α` to `β`, then `f` is Lipschitz continuous with constant `K` if and only if, for all `x, y` in `α`, the distance between `f(x)` and `f(y)` is less than or equal to `K` times the distance between `x` and `y`. In mathematical terms, this can be represented as: \(f\) is Lipschitz continuous with constant \(K \geq 0\) if and only if \(d(f(x), f(y)) \leq K * d(x, y)\) for all \(x, y\).
More concisely: A function between two pseudo-metric spaces is Lipschitz continuous with constant K if and only if the distance between its values on any two points is less than or equal to K times the distance between the points in the original space.
|
LipschitzWith.of_le_add
theorem LipschitzWith.of_le_add :
∀ {α : Type u} [inst : PseudoMetricSpace α] {f : α → ℝ}, (∀ (x y : α), f x ≤ f y + dist x y) → LipschitzWith 1 f
The theorem `LipschitzWith.of_le_add` states that for any type `α` equipped with a PseudoMetricSpace structure, and any function `f` from `α` to the real numbers (ℝ), if for all `x` and `y` from `α`, the value of `f` at `x` is less than or equal to the value of `f` at `y` plus the distance between `x` and `y`, then `f` is Lipschitz continuous with a constant `1`. In mathematical terms, this asserts that if `f(x) ≤ f(y) + dist(x, y)` for all `x` and `y`, then `f` satisfies the Lipschitz condition `dist(f(x), f(y)) ≤ 1 * dist(x, y)` for all `x` and `y`. This condition is a fundamental one in mathematical analysis, ensuring key properties like stability and robustness of the function.
More concisely: If a real-valued function on a PseudoMetricSpace satisfies `f(x) ≤ f(y) + dist(x, y)` for all `x` and `y`, then it is Lipschitz continuous with constant 1.
|