lipschitzOnWith_iff_restrict
theorem lipschitzOnWith_iff_restrict :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β}
{s : Set α}, LipschitzOnWith K f s ↔ LipschitzWith K (s.restrict f)
This theorem states that for any two types `α` and `β` equipped with pseudo-emetric space structures, a nonnegative real number `K`, a function `f` from `α` to `β`, and a set `s` of `α`, the function `f` is Lipschitz continuous with constant `K` on the set `s` if and only if the function `f`, when restricted to the set `s`, is Lipschitz continuous with constant `K`. In mathematical terms, for all `x, y` in `s`, the extended distance between `f(x)` and `f(y)` is less than or equal to `K` times the extended distance between `x` and `y`. The restriction of the function `f` to the set `s` is the function that maps each element of `s` to its image under `f`.
More concisely: Given pseudo-metric spaces `α` and `β` with types `α` and `β`, a nonnegative real number `K`, a Lipschitz continuous function `f` from `α` to `β` with constant `K`, and a set `s` of `α`, the restriction of `f` to `s` is Lipschitz continuous with constant `K` on `s`. That is, for all `x, y` in `s`, `d(f(x), f(y)) ≤ K * d(x, y)` where `d` denotes the extended distance.
|
continuous_prod_of_dense_continuous_lipschitzWith
theorem continuous_prod_of_dense_continuous_lipschitzWith :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : TopologicalSpace β]
[inst_2 : PseudoEMetricSpace γ] (f : α × β → γ) (K : NNReal) {s : Set α},
Dense s →
(∀ a ∈ s, Continuous fun y => f (a, y)) → (∀ (b : β), LipschitzWith K fun x => f (x, b)) → Continuous f
This theorem states that for a function `f` mapping from a pair of types `α` and `β` to a type `γ`, if `f` is continuous for each "vertical section" (that is, subsets of the form `{a} × univ`, where `a` is an element of a dense set `s` in `α`), and `f` is Lipschitz continuous with the same Lipschitz constant `K` for each "horizontal section" (subsets of the form `univ × {b}`, `b : β`), then `f` is continuous. Note that in this context, continuity of `f` on subsets of the product space is defined in terms of continuity of functions `fun y ↦ f (a, y)` and `fun x ↦ f (x, b)`, not of `f` itself.
More concisely: If a function `f` from the product of dense sets `α × β` to `γ` is continuous on all vertical and horizontal sections with the same Lipschitz constant `K`, then `f` is continuous.
|
continuousOn_prod_of_continuousOn_lipschitzOnWith
theorem continuousOn_prod_of_continuousOn_lipschitzOnWith :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : TopologicalSpace β]
[inst_2 : PseudoEMetricSpace γ] (f : α × β → γ) {s : Set α} {t : Set β} (K : NNReal),
(∀ a ∈ s, ContinuousOn (fun y => f (a, y)) t) →
(∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s) → ContinuousOn f (s ×ˢ t)
The theorem `continuousOn_prod_of_continuousOn_lipschitzOnWith` states that for a given function `f` mapping from a product of two types `α` and `β` to a type `γ`, if the function `f` is continuous on each "vertical fiber" `{a} × t` for `a` in set `s`, and Lipschitz continuous on each "horizontal fiber" `s × {b}` for `b` in set `t` with the same Lipschitz constant `K`, then `f` is continuous on the product of sets `s` and `t`. It's important to note that the theorem considers the Lipschitz continuity of `fun y ↦ f (a, y)` and `fun x ↦ f (x, b)` rather than the continuity of `f` on subsets of the product space.
More concisely: If a function `f` from the product of sets `α × β` to `γ` is continuous on each vertical fiber `{a} × β` for `a` in `α`, and Lipschitz continuous on each horizontal fiber `α × {b}` for `b` in `β` with the same constant `K`, then `f` is continuous on the product `α × β`.
|
LipschitzWith.ediam_image_le
theorem LipschitzWith.ediam_image_le :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
LipschitzWith K f → ∀ (s : Set α), EMetric.diam (f '' s) ≤ ↑K * EMetric.diam s
This theorem states that for any two types `α` and `β` that are pseudo emetric spaces, for any nonnegative real number `K`, and for any function `f` from `α` to `β`, if `f` is Lipschitz continuous with constant `K`, then for any set `s` of type `α`, the pseudo emetric diameter of the image of `s` under `f` is less than or equal to `K` times the pseudo emetric diameter of `s`. In other words, a Lipschitz continuous function does not expand the pseudo emetric diameter of a set by more than its Lipschitz constant.
More concisely: Given pseudo metric spaces `α` and `β`, if `f` is a Lipschitz continuous function from `α` to `β` with constant `K`, then the pseudo metric diameter of `f`'s image of a set `s` in `α` is less than or equal to `K` times the pseudo metric diameter of `s`.
|
LipschitzWith.uniformContinuous
theorem LipschitzWith.uniformContinuous :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
LipschitzWith K f → UniformContinuous f
This theorem states that a Lipschitz continuous function is uniformly continuous. In more detail, for any two types `α` and `β` that form pseudo-emetric spaces, a function `f` from `α` to `β` that is Lipschitz continuous with a non-negative constant `K`, is also uniformly continuous. In mathematical terms, if for every pair of points `x` and `y` 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 uniformly continuous, meaning that as `x` gets arbitrarily close to `y`, `f(x)` gets arbitrarily close to `f(y)` regardless of the location of `x` and `y` in their space.
More concisely: A Lipschitz continuous function between pseudo-metric spaces is uniformly continuous.
|
lipschitzOn_univ
theorem lipschitzOn_univ :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
LipschitzOnWith K f Set.univ ↔ LipschitzWith K f
The theorem `lipschitzOn_univ` states that a function `f` mapping from a pseudometric space `α` to a pseudometric space `β` is Lipschitz continuous with a nonnegative constant `K` if and only if it is Lipschitz continuous with the same constant `K` over the entire set of `α`. In other words, the Lipschitz continuity of `f` over all elements of `α` (the universal set of `α`) is equivalent to the Lipschitz continuity of `f` under any subset of `α`. This is formalized in the context of pseudometric spaces, where the notion of distance is generalized with the extended distance `edist`, and the Lipschitz condition is expressed in terms of this `edist`.
More concisely: A function between pseudometric spaces is Lipschitz continuous with a constant K over the entire space if and only if it is Lipschitz continuous with the same constant K over any subset.
|
continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith
theorem continuousOn_prod_of_subset_closure_continuousOn_lipschitzOnWith :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : TopologicalSpace β]
[inst_2 : PseudoEMetricSpace γ] (f : α × β → γ) {s s' : Set α} {t : Set β},
s' ⊆ s →
s ⊆ closure s' →
∀ (K : NNReal),
(∀ a ∈ s', ContinuousOn (fun y => f (a, y)) t) →
(∀ b ∈ t, LipschitzOnWith K (fun x => f (x, b)) s) → ContinuousOn f (s ×ˢ t)
This theorem states that for a function `f` mapping from the product of two sets `α` and `β` to a set `γ`, given that `α` and `γ` are pseudo-emetric spaces and `β` is a topological space. If there exists a subset `s'` of `s` that's dense within `s`, and `f` is continuous on each "vertical fiber" `{a} × t, a ∈ s'`, and Lipshitz continuous on each "horizontal fiber" `s × {b}, b ∈ t` with the same Lipshitz constant `K`, then `f` is continuous on the product `s × t`. This means that restricting the domain of `f` to these fibers doesn't disrupt its continuity or Lipschitz continuity properties. This theorem essentially provides a condition under which continuity and Lipschitz continuity can be guaranteed on the product of two sets.
More concisely: If a function between the product of two sets, one being a pseudo-metric space with a dense subset and the other a topological space, is continuous on each vertical fiber over the dense subset and Lipshitz continuous on each horizontal fiber with the same constant, then it is continuous on the product space.
|
LipschitzWith.prod_fst
theorem LipschitzWith.prod_fst :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β],
LipschitzWith 1 Prod.fst
This theorem states that for any types `α` and `β` that are both instances of a `PseudoEMetricSpace`, the first projection function `Prod.fst` is Lipschitz continuous with a Lipschitz constant of `1`. In mathematical terms, this means that for any pair of points `(x, y)` and `(w, z)` in the product space `α × β`, the distance between `x` and `w` in the space `α` is less than or equal to the distance between `(x, y)` and `(w, z)` in the product space `α × β`.
More concisely: The first projection function of a product of two pseudo-metric spaces is Lipschitz continuous with Lipschitz constant 1.
|
LipschitzWith.of_edist_le
theorem LipschitzWith.of_edist_le :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
(∀ (x y : α), edist (f x) (f y) ≤ edist x y) → LipschitzWith 1 f
The theorem `LipschitzWith.of_edist_le` states that for any two types `α` and `β`, where both `α` and `β` are pseudo emetric spaces, and for any function `f` from `α` to `β`, if for all `x` and `y` in `α` the extended distance (`edist`) between `f(x)` and `f(y)` is less than or equal to the extended distance between `x` and `y`, then the function `f` is Lipschitz continuous with a Lipschitz constant of `1`. That is, the theorem states that if `edist (f x) (f y) ≤ edist x y` for all `x` and `y` in `α`, then the distance between any two images under `f` is at most the distance between their pre-images.
More concisely: If `f: α → β` is a function between pseudo metric spaces `α` and `β` such that `edist (f x) (f y) ≤ edist x y` for all `x, y ∈ α`, then `f` is Lipschitz continuous with Lipschitz constant 1.
|
LipschitzOnWith.to_restrict
theorem LipschitzOnWith.to_restrict :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β}
{s : Set α}, LipschitzOnWith K f s → LipschitzWith K (s.restrict f)
This theorem states that given two types `α` and `β`, both equipped with a pseudo emetric space structure, a nonnegative real `K`, a function `f` from `α` to `β`, and a set `s` of type `α`, if the function `f` is Lipschitz continuous with constant `K` on the set `s`, then the function `f`, when restricted to the set `s`, is Lipschitz continuous with the same constant `K`. This property is an alias of the forward direction of the theorem `lipschitzOnWith_iff_restrict`. In other words, it guarantees the Lipschitz continuity of a function when its domain is reduced to a specific set.
More concisely: Given two pseudo metric spaces `(α, dα)` and `(β, dβ)`, a Lipschitz continuous function `f : α → β` with constant `K` on a subset `s ⊆ α`, the restriction of `f` to `s` is also Lipschitz continuous with constant `K`.
|
LipschitzWith.restrict
theorem LipschitzWith.restrict :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
LipschitzWith K f → ∀ (s : Set α), LipschitzWith K (s.restrict f)
This theorem states that the restriction of a `K`-Lipschitz function remains `K`-Lipschitz. Given a function `f` from a type `α` to a type `β`, both endowed with a pseudo-emetric space structure, if this function is `K`-Lipschitz continuous, then for any subset `s` of `α`, the restriction of the function `f` to the set `s` is also `K`-Lipschitz continuous. A function is `K`-Lipschitz continuous if the distance (`edist`) between its values at any two points is less than or equal to `K` times the distance between the points themselves. The restriction of a function to a subset is the function defined only on that subset.
More concisely: If a function between pseudometric spaces is K-Lipschitz, then its restriction to any subset is also K-Lipschitz.
|
LipschitzWith.subtype_val
theorem LipschitzWith.subtype_val :
∀ {α : Type u} [inst : PseudoEMetricSpace α] (s : Set α), LipschitzWith 1 Subtype.val
This theorem states that for any set 's' in a type 'α' that has a pseudo-emetric space structure, the function 'Subtype.val' (which maps an element of the subtype defined by set 's' to its underlying element in the base type) is Lipschitz continuous with a constant of 1. In other words, for all elements 'x' and 'y' of the subtype, the distance in the pseudo-emetric space between the images of 'x' and 'y' under 'Subtype.val' is less than or equal to the distance between 'x' and 'y' itself.
More concisely: For any subtype 's' of a pseudo-metric space 'α', the function 'Subtype.val' is 1-Lipschitz continuous.
|
LipschitzWith.prod
theorem LipschitzWith.prod :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
[inst_2 : PseudoEMetricSpace γ] {f : α → β} {Kf : NNReal},
LipschitzWith Kf f →
∀ {g : α → γ} {Kg : NNReal}, LipschitzWith Kg g → LipschitzWith (max Kf Kg) fun x => (f x, g x)
This theorem states that if you have two functions `f` and `g` that are Lipschitz continuous, with Lipschitz constants `Kf` and `Kg` respectively, then the function that maps `x` to the pair `(f x, g x)` is also Lipschitz continuous. The Lipschitz constant of this composite function is the maximum of `Kf` and `Kg`.
More concisely: If functions `f` and `g` are Lipschitz continuous with constants `Kf` and `Kg` respectively, then the function `(x ↔⟩ (f x, g x))` is Lipschitz continuous with constant `max Kf Kg`.
|
LocallyLipschitz.const
theorem LocallyLipschitz.const :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (b : β),
LocallyLipschitz fun x => b
The theorem `LocallyLipschitz.const` states that all constant functions are locally Lipschitz continuous. In other words, for any types `α` and `β` that are pseudo emetric spaces and any value `b` of type `β`, the function that maps every point in `α` to `b` is locally Lipschitz continuous. This means that for every point `x` in `α`, there exists a neighborhood of `x` on which the function is Lipschitz with some Lipschitz constant `K`.
More concisely: For any pseudo metric spaces `α` and `β`, and any constant value `b` in `β`, the function mapping every point in `α` to `b` is locally Lipschitz continuous with some constant `K`.
|
LipschitzWith.eval
theorem LipschitzWith.eval :
∀ {ι : Type x} {α : ι → Type u} [inst : (i : ι) → PseudoEMetricSpace (α i)] [inst_1 : Fintype ι] (i : ι),
LipschitzWith 1 (Function.eval i)
This theorem states that for any type `ι`, any function `α` from `ι` to a type, where each type `α i` is a pseudoemetric space, and for any `ι` that is a finite type, the evaluation function at any `ι` is Lipschitz continuous with constant 1. In other words, the distance between the function values at any two points is less than or equal to the distance between the points themselves in the pseudoemetric space.
More concisely: For any finite type `ι` and a function `α:` `ι` → `M` with each `M(i)` being a pseudo-metric space, the evaluation function `α` is Lipschitz continuous with constant 1.
|
LipschitzOnWith.prod
theorem LipschitzOnWith.prod :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
[inst_2 : PseudoEMetricSpace γ] {s : Set α} {f : α → β} {g : α → γ} {Kf Kg : NNReal},
LipschitzOnWith Kf f s → LipschitzOnWith Kg g s → LipschitzOnWith (max Kf Kg) (fun x => (f x, g x)) s
The theorem `LipschitzOnWith.prod` states that if we have two functions `f` and `g` that are Lipschitz continuous on a set `s`, then the function that maps `x` in `s` to the pair `(f(x), g(x))` is also Lipschitz continuous on `s`. Here, the Lipschitz continuity of a function is gauged by a nonnegative real number known as the Lipschitz constant, and for the pair function `(f(x), g(x))`, the Lipschitz constant is the maximum of the Lipschitz constants of `f` and `g`. The Lipschitz continuity means that the distance between `f(x)` and `f(y)` (or `g(x)` and `g(y)`), as measured in a pseudoemetric space, is at most `K` times the distance between `x` and `y` for all `x` and `y` in `s`. In the case of the pair function, the distance is measured according to the pseudoemetric on the product of the pseudoemetric spaces of `f` and `g`.
More concisely: If `f` and `g` are Lipschitz continuous functions on a set `s` with Lipschitz constants `K_f` and `K_g` respectively, then the function mapping `x` in `s` to the pair `(f(x), g(x))` is a Lipschitz continuous function on `s` with Lipschitz constant `max(K_f, K_g)`.
|
LipschitzWith.id
theorem LipschitzWith.id : ∀ {α : Type u} [inst : PseudoEMetricSpace α], LipschitzWith 1 id
This theorem states that the identity function is 1-Lipschitz. In other words, in any pseudoemetric space, the distance between the images of any two points under the identity function is less than or equal to one times the distance between the points themselves. This is generally expressed as `dist(f(x), f(y)) ≤ K * dist(x, y)`, where `f` is the function in question (in this case, the identity function), `x` and `y` are any two points in the space, and `K` is the Lipschitz constant (in this case, 1).
More concisely: In any pseudometric space, the distance between the identity function's images of any two points is no greater than the distance between the points themselves.
|
LipschitzOnWith.mono
theorem LipschitzOnWith.mono :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {s t : Set α}
{f : α → β}, LipschitzOnWith K f t → s ⊆ t → LipschitzOnWith K f s
The theorem `LipschitzOnWith.mono` states that if a function `f` is Lipschitz continuous with a nonnegative real constant `K` on a set `t` in a pseudo emetric space, and if `s` is a subset of `t`, then `f` is also Lipschitz continuous with the same constant `K` on `s`. In other words, the property of a function being Lipschitz continuous on a set is monotone with respect to that set.
More concisely: If a function is Lipschitz continuous on a set with constant K, then it is also Lipschitz continuous on any subset with the same constant.
|
LipschitzWith.locallyLipschitz
theorem LipschitzWith.locallyLipschitz :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β} {K : NNReal},
LipschitzWith K f → LocallyLipschitz f
This theorem states that a Lipschitz continuous function is also locally Lipschitz continuous. In more detail, it says that for any pseudometric spaces `α` and `β`, and any function `f` from `α` to `β`, if `f` is Lipschitz continuous with some nonnegative real constant `K` (i.e., the distance between `f(x)` and `f(y)` is less than or equal to `K` times the distance between `x` and `y` for all `x` and `y`), then `f` is also locally Lipschitz continuous. Being locally Lipschitz continuous means that for every point `x` in the domain, there exists a neighborhood around `x` such that within this neighborhood, `f` is Lipschitz continuous with some constant.
More concisely: A Lipschitz continuous function is locally Lipschitz continuous.
|
LipschitzWith.prod_snd
theorem LipschitzWith.prod_snd :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β],
LipschitzWith 1 Prod.snd
The theorem `LipschitzWith.prod_snd` states that for any types `α` and `β` which are equipped with a pseudo emetric space structure, the second projection function `Prod.snd`, which takes a pair and returns its second component, is Lipschitz continuous with constant `1`. In mathematical terms, this means that for any pair of points `x` and `y` in the product space `α × β`, the distance between the second components of `x` and `y` (using the metric of `β`) is less than or equal to the distance between `x` and `y` (using the product metric).
More concisely: Given two pseudo metric spaces `(α, dα)` and `(β, dβ)`, the second projection function of their product space `(α × β, dₓ)` is 1-Lipschitz with respect to the second component metric `dβ`.
|
LipschitzOnWith.ediam_image2_le
theorem LipschitzOnWith.ediam_image2_le :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
[inst_2 : PseudoEMetricSpace γ] (f : α → β → γ) {K₁ K₂ : NNReal} (s : Set α) (t : Set β),
(∀ b ∈ t, LipschitzOnWith K₁ (fun x => f x b) s) →
(∀ a ∈ s, LipschitzOnWith K₂ (f a) t) →
EMetric.diam (Set.image2 f s t) ≤ ↑K₁ * EMetric.diam s + ↑K₂ * EMetric.diam t
The theorem `LipschitzOnWith.ediam_image2_le` states that for any three types `α`, `β`, and `γ` equipped with pseudoemetric spaces, and for any binary function `f : α → β → γ`, if for every `b` in a set `t` the function `f(_ , b)` is Lipschitz continuous with constant `K₁` on a set `s`, and for every `a` in the set `s` the function `f(a, _)` is Lipschitz continuous with constant `K₂` on the set `t`, then the diameter of the image of the function `f` on the sets `s` and `t`, denoted `EMetric.diam (Set.image2 f s t)`, is less than or equal to `K₁` times the diameter of `s` plus `K₂` times the diameter of `t`. Here, the diameter of a set is the supremum of the distances between all pairs of points in the set.
More concisely: For any three pseudometric spaces `α × β → γ` with functions `f : α → β → γ`, if `f(_, b)` is Lipschitz continuous on `s ⊆ α` with constant `K₁` for each `b ∈ t ⊆ β`, and `f(a, _)` is Lipschitz continuous on `t` with constant `K₂` for each `a ∈ s`, then the diameter of `f(s × t)` is at most `K₁ * ∇(s) + K₂ * ∇(t)`, where `∇` denotes the diameter.
|
LocallyLipschitz.id
theorem LocallyLipschitz.id : ∀ {α : Type u} [inst : PseudoEMetricSpace α], LocallyLipschitz id
The theorem `LocallyLipschitz.id` states that the identity function is locally Lipschitz continuous in any pseudo-emetric space. This essentially means that for any point `x` in the space, there exists a neighborhood around `x` where the identity function follows Lipschitz continuity. Here, Lipschitz continuity implies that the distance between the output values of any two points in the neighborhood is less than or equal to a constant `K` times the distance between the two points themselves.
More concisely: In any pseudo-metric space, the identity function is locally Lipschitz continuous with constant K for some neighborhood around each point x, meaning the distance between identity function outputs of any two points in the neighborhood is at most K times their distance apart.
|
lipschitzOnWith_empty
theorem lipschitzOnWith_empty :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (K : NNReal) (f : α → β),
LipschitzOnWith K f ∅
This theorem states that every function is Lipschitz continuous on the empty set, regardless of the Lipschitz constant. In more detail, given any types `α` and `β` that are equipped with pseudo emetric spaces and any function `f` from `α` to `β`, as well as any nonnegative real number `K`, the function `f` is Lipschitz continuous with constant `K` on the empty set. This essentially means that the distance between the images of any two points under the function (which doesn't exist since the set is empty) is less than or equal to `K` times the distance between the two points themselves.
More concisely: Every function is Lipschitz continuous on the empty set with any non-negative real constant. (Since there are no distinct points in the empty set, the notion of distance between images under the function is moot.)
|
LipschitzWith.continuous
theorem LipschitzWith.continuous :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
LipschitzWith K f → Continuous f
The theorem states that a Lipschitz function is always continuous. More specifically, for any two types `α` and `β` that are equipped with a pseudo emetric space structure, any function `f` from `α` to `β` that is Lipschitz continuous with a nonnegative real number `K`, is also a continuous function. In mathematical terms, if for all `x` and `y` in `α`, the extended distance between `f(x)` and `f(y)` is less than or equal to `K` times the extended distance between `x` and `y`, then `f` is a continuous function.
More concisely: If a function between two metric spaces is Lipschitz continuous with a finite Lipschitz constant, then it is continuous.
|
LocallyLipschitz.comp
theorem LocallyLipschitz.comp :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
[inst_2 : PseudoEMetricSpace γ] {f : β → γ} {g : α → β},
LocallyLipschitz f → LocallyLipschitz g → LocallyLipschitz (f ∘ g)
The theorem `LocallyLipschitz.comp` states that if we have two functions, `f` and `g`, where `f` is a function from a pseudometric space `β` to another pseudometric space `γ`, and `g` is a function from a pseudometric space `α` to `β`, and both these functions are locally Lipschitz continuous, then the composition of `f` and `g`, denoted as `(f ∘ g)`, is also locally Lipschitz continuous. In other words, for every point in the domain of the composition, there exists a neighbourhood of that point on which the composed function is Lipschitz continuous. The Lipschitz continuity ensures that the rate of change of the function is bounded by a constant `K` on the neighbourhood.
More concisely: If functions `f: β -> γ` and `g: α -> β` are locally Lipschitz continuous, then their composition `f ∘ g: α -> γ` is also locally Lipschitz continuous.
|
LocallyLipschitz.prod
theorem LocallyLipschitz.prod :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
[inst_2 : PseudoEMetricSpace γ] {f : α → β},
LocallyLipschitz f → ∀ {g : α → γ}, LocallyLipschitz g → LocallyLipschitz fun x => (f x, g x)
The theorem `LocallyLipschitz.prod` states that if functions `f` and `g` are locally Lipschitz continuous, then the map `f × g` to the product type, defined by `(f x, g x)` for each `x`, is also locally Lipschitz continuous. Here, a function is locally Lipschitz continuous if for every point `x`, there exists a neighborhood on which the function is Lipschitz continuous. This is defined in the context of pseudoemetric spaces, which are sets equipped with a function that gives a 'distance' between two elements of the set.
More concisely: If functions `f` and `g` are locally Lipschitz continuous, then the product function `(x ↔о X) ↔o (f x, g x)` is also locally Lipschitz continuous in the pseudometric space `X`.
|
LipschitzWith.list_prod
theorem LipschitzWith.list_prod :
∀ {α : Type u} {ι : Type x} [inst : PseudoEMetricSpace α] (f : ι → Function.End α) (K : ι → NNReal),
(∀ (i : ι), LipschitzWith (K i) (f i)) → ∀ (l : List ι), LipschitzWith (List.map K l).prod (List.map f l).prod
This theorem states that the product of a list of Lipschitz continuous endomorphisms is a Lipschitz continuous endomorphism. More specifically, given a pseudometric space `α`, a function `f` that maps values in type `ι` to endomorphisms on `α`, and a function `K` that maps `ι` to nonnegative real numbers, if for every `i` in `ι`, `f(i)` is Lipschitz continuous with constant `K(i)`, then for any list `l` of type `ι`, the product of the mapped list of `f` on `l` is Lipschitz continuous with the product of the mapped list of `K` on `l` as the Lipschitz constant.
In mathematical terms, it means that if each function in a list is Lipschitz continuous with its respective Lipschitz constant, then the product of these functions is also Lipschitz continuous with the product of their Lipschitz constants as the Lipschitz constant.
This property is important in metric space theory and functional analysis, as it suggests the preservation of Lipschitz continuity under multiplication of Lipschitz continuous functions.
More concisely: If each function in a list of Lipschitz continuous endomorphisms on a pseudometric space has a Lipschitz constant, then the product of these functions is a Lipschitz continuous endomorphism with the product of their Lipschitz constants as its Lipschitz constant.
|
LipschitzWith.const
theorem LipschitzWith.const :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (b : β),
LipschitzWith 0 fun x => b
This theorem states that constant functions are Lipschitz continuous with any constant. Specifically, for any types `α` and `β` that are pseudo-emetric spaces, and for any element `b` of type `β`, the function that maps every element of `α` to `b` is Lipschitz continuous with a Lipschitz constant of `0`. In other words, the distance between the images of any two distinct points in `α` under this function is less than or equal to `0` times the distance between these two points, which is always true since the images are always the same (i.e., `b`).
More concisely: For any pseudo-metric spaces `α` and `β` and any constant `b` in `β`, the function mapping every element in `α` to `b` is a Lipschitz continuous function with Lipschitz constant 0.
|
LipschitzWith.iterate
theorem LipschitzWith.iterate :
∀ {α : Type u} [inst : PseudoEMetricSpace α] {K : NNReal} {f : α → α},
LipschitzWith K f → ∀ (n : ℕ), LipschitzWith (K ^ n) f^[n]
This theorem states that the iterates of a Lipschitz continuous function are also Lipschitz continuous. Specifically, if a function `f` from a pseudo-emetric space to itself is Lipschitz continuous with a nonnegative real constant `K`, then for any natural number `n`, the `n`-th iterate of `f` (i.e., the function obtained by composing `f` with itself `n` times) is Lipschitz continuous with the constant `K` to the power of `n`. The distance between the image of any two points under the `n`-th iterate of `f` is not more than `K^n` times the distance between the two points.
More concisely: If a Lipschitz continuous function with constant K from a pseudo-metric space to itself is composed n times, then the resulting function is also Lipschitz continuous with constant K^n.
|
LocallyLipschitz.continuous
theorem LocallyLipschitz.continuous :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
LocallyLipschitz f → Continuous f
This theorem states that if a function `f` from a pseudoemetric space `α` to another pseudoemetric space `β` is locally Lipschitz continuous, then that function `f` is also continuous. Being locally Lipschitz continuous means that for every point `x` in the domain, there exists a neighborhood around `x` where `f` satisfies the Lipschitz condition. It's worth noting that while every locally Lipschitz continuous function is continuous, the converse is not always true. An example of this is the function $f(x) = \sqrt{x}$, which is continuous but not locally Lipschitz continuous at the point 0.
More concisely: If a function between two pseudometric spaces is locally Lipschitz continuous, then it is continuous.
|
LipschitzWith.lipschitzOnWith
theorem LipschitzWith.lipschitzOnWith :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β},
LipschitzWith K f → ∀ (s : Set α), LipschitzOnWith K f s
The theorem `LipschitzWith.lipschitzOnWith` states that for any set `s`, if a function `f` from a pseudometric space `α` to another pseudometric space `β` is Lipschitz continuous with a nonnegative real constant `K`, then `f` is also Lipschitz continuous on the set `s` with the same constant `K`. In other words, if the distance between the images of any two points under `f` is at most `K` times the distance between the points themselves, then this property still holds when those points are restricted to belong to a particular set `s`.
More concisely: If `f:` `α` → `β` is a Lipschitz continuous function with constant `K` from the pseudometric space `α` to the pseudometric space `β`, then `f` is Lipschitz continuous on any set `s` ⊆ `α` with the same constant `K`.
|
LipschitzWith.comp
theorem LipschitzWith.comp :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
[inst_2 : PseudoEMetricSpace γ] {Kf Kg : NNReal} {f : β → γ} {g : α → β},
LipschitzWith Kf f → LipschitzWith Kg g → LipschitzWith (Kf * Kg) (f ∘ g)
The theorem `LipschitzWith.comp` asserts that the composition of Lipschitz continuous functions is also Lipschitz continuous. More formally, given two functions `f` and `g` of types `β → γ` and `α → β` respectively, if `f` is Lipschitz continuous with a nonnegative real constant `Kf` and `g` is Lipschitz continuous with a nonnegative real constant `Kg`, then their composition `(f ∘ g)` is Lipschitz continuous with the constant being the product of `Kf` and `Kg`. Here, `α`, `β`, and `γ` are types equipped with a pseudo emetric space structure which allows us to measure distance between elements of these types.
More concisely: If functions `f: β → γ` and `g: α → β` are Lipschitz continuous with constants `Kf` and `Kg` respectively, then their composition `f ∘ g: α → γ` is Lipschitz continuous with constant `Kf * Kg`.
|
LipschitzOnWith.to_restrict_mapsTo
theorem LipschitzOnWith.to_restrict_mapsTo :
∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {K : NNReal} {f : α → β}
{s : Set α} {t : Set β} (h : Set.MapsTo f s t),
LipschitzOnWith K f s → LipschitzWith K (Set.MapsTo.restrict f s t h)
This theorem states that for any two types `α` and `β`, that both have a pseudo emetric space structure, a nonnegative real number `K`, a function `f` from `α` to `β`, and two sets `s` and `t` of type `α` and `β` respectively, if `f` maps `s` to `t` (i.e., the image of `s` under `f` is contained in `t`) and `f` is Lipschitz continuous with constant `K` on `s` (meaning that the extended distance between `f(x)` and `f(y)` is less than or equal to `K` times the extended distance between `x` and `y` for all `x` and `y` in `s`), then the function obtained by restricting the domain of `f` to `s` and the codomain to `t` is Lipschitz continuous with constant `K`. In other words, any Lipschitz continuous function remains Lipschitz continuous after the restriction of its domain and codomain.
More concisely: If `f` is a Lipschitz continuous function from type `α` to type `β` with constant `K`, and `s` is a subset of `α` such that the image of `s` under `f` is contained in `t`, then the restriction of `f` to `s` is a Lipschitz continuous function from `s` to `t` with the same constant `K`.
|
continuous_prod_of_continuous_lipschitzWith
theorem continuous_prod_of_continuous_lipschitzWith :
∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : TopologicalSpace β]
[inst_2 : PseudoEMetricSpace γ] (f : α × β → γ) (K : NNReal),
(∀ (a : α), Continuous fun y => f (a, y)) → (∀ (b : β), LipschitzWith K fun x => f (x, b)) → Continuous f
This theorem states that if you have a function `f : α × β → γ`, where `α`, `β`, and `γ` are types associated with pseudo-emetric spaces (for `α` and `γ`) and a topological space (for `β`, essentially stating that these types have some notion of "closeness" or "distance"), and if this function is continuous on all "vertical sections" (meaning for each fixed `a : α`, the function `y ↦ f(a, y)` is continuous) and is Lipschitz continuous on all "horizontal sections" (meaning for each fixed `b : β`, the function `x ↦ f(x, b)` is Lipschitz continuous with the same Lipschitz constant `K > 0`), then the function `f` is continuous over the entire product space `α × β`. This essentially means that small changes in the input to `f` only result in small changes in its output, and this holds true no matter how you slice or fix one of the input dimensions.
More concisely: If `f : α × β → γ` is a continuous function on all vertical sections and Lipschitz continuous on all horizontal sections with constant `K`, then `f` is a continuous function on the product space `α × β`.
|