LipschitzOnWith.holderOnWith
theorem LipschitzOnWith.holderOnWith :
∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C : NNReal}
{f : X → Y} {s : Set X}, LipschitzOnWith C f s → HolderOnWith C 1 f s
The theorem `LipschitzOnWith.holderOnWith` states that for any two types `X` and `Y` equipped with PseudoEMetricSpace structures, a nonnegative real number `C`, a function `f` from `X` to `Y`, and a set `s` of type `X`, if the function `f` is Lipschitz continuous with constant `C` on the set `s`, then `f` is also Hölder continuous on `s` with constant `C` and exponent `1`. Here, being Lipschitz continuous means that the distance (in the sense of the PseudoEMetricSpace structure) between `f(x)` and `f(y)` is at most `C` times the distance between `x` and `y` for all `x` and `y` in `s`, while being Hölder continuous means that the distance between `f(x)` and `f(y)` is at most `C` times the distance between `x` and `y` raised to the power `1` for all `x` and `y` in `s`.
More concisely: If a function between two metric spaces is Lipschitz continuous on a set with constant C, then it is also Hölder continuous on that set with exponent 1 and constant C.
|
HolderOnWith.uniformContinuousOn
theorem HolderOnWith.uniformContinuousOn :
∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal}
{f : X → Y} {s : Set X}, HolderOnWith C r f s → 0 < r → UniformContinuousOn f s
The theorem states that for any two given pseudo-emetric spaces `X` and `Y`, a function `f` mapping from `X` to `Y`, and a set `s` of type `X`, if the function `f` is Hölder continuous with constants `C` and `r`, and `r` is greater than 0, then the function `f` is uniformly continuous on the set `s`. In simple terms, this theorem shows that a Hölder continuous function, where the Hölder constant is positive, is also uniformly continuous.
More concisely: If `f` is a Hölder continuous function from a pseudo-metric space `X` to another pseudo-metric space `Y` with constant `C` and `r > 0`, then `f` is uniformly continuous on any subset `s` of `X`.
|
HolderOnWith.edist_le_of_le
theorem HolderOnWith.edist_le_of_le :
∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal}
{f : X → Y} {s : Set X},
HolderOnWith C r f s →
∀ {x y : X}, x ∈ s → y ∈ s → ∀ {d : ENNReal}, edist x y ≤ d → edist (f x) (f y) ≤ ↑C * d ^ ↑r
This theorem states that for any types `X` and `Y` with `PseudoEMetricSpace` structures, given any nonnegative real numbers `C` and `r`, a function `f` from `X` to `Y`, and a set `s` of `X`, if the function `f` is Hölder continuous with constant `C` and exponent `r` on the set `s`, then for any elements `x` and `y` in the set `s` and any extended nonnegative real number `d`, if the extended distance between `x` and `y` is less than or equal to `d`, the extended distance between `f(x)` and `f(y)` is less than or equal to `C` times `d` to the power of `r`. This theorem thus provides a bound on the distance between the images under `f` of two points in the set `s` based on the distance between the points and the Hölder continuity of `f`.
More concisely: Given two Pseudo-Metric Spaces X and Y, a Hölder continuous function f from X to Y with constant C and exponent r on a set s, and any x, y in s, the extended distance between f(x) and f(y) is less than or equal to C * (extended distance between x and y) ^ r.
|
HolderWith.holderOnWith
theorem HolderWith.holderOnWith :
∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal}
{f : X → Y}, HolderWith C r f → ∀ (s : Set X), HolderOnWith C r f s
The theorem `HolderWith.holderOnWith` states that for all spaces `X` and `Y` that are pseudo emetric spaces, for any nonnegative real numbers `C` and `r`, and any function `f` from `X` to `Y`, if `f` is Hölder continuous with constant `C` and exponent `r`, then for any set `s` within `X`, `f` is also Hölder continuous with constant `C` and exponent `r` on the set `s`. In other words, if a function is Hölder continuous in the whole space, it is also Hölder continuous when restricted to any subset of that space.
More concisely: If `f` is a Hölder continuous function from a pseudo metric space `X` to another pseudo metric space `Y` with constant `C` and exponent `r`, then `f` restricted to any subset `s` of `X` is also Hölder continuous with constant `C` and exponent `r`.
|
LipschitzWith.holderWith
theorem LipschitzWith.holderWith :
∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C : NNReal}
{f : X → Y}, LipschitzWith C f → HolderWith C 1 f
The theorem `LipschitzWith.holderWith` states that for any two types `X` and `Y` that are both pseudoemetric spaces, and any function `f` from `X` to `Y` with a nonnegative real number `C`, if the function `f` is Lipschitz continuous with constant `C`, then it is also Hölder continuous with constant `C` and exponent `1`. This means that if `f` satisfies the Lipschitz condition, `edist (f x) (f y) ≤ C * edist x y` for all `x, y`, then it also satisfies the Hölder condition, `edist (f x) (f y) ≤ C * edist x y ^ 1` for all `x, y`, where `edist` denotes the extended metric or distance function in the pseudoemetric spaces `X` and `Y`.
More concisely: If `f` is a Lipschitz continuous function from a pseudometric space `X` to another pseudometric space `Y` with constant `C`, then `f` is also Hölder continuous with constant `C` and exponent `1`.
|
HolderWith.uniformContinuous
theorem HolderWith.uniformContinuous :
∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal}
{f : X → Y}, HolderWith C r f → 0 < r → UniformContinuous f
The theorem `HolderWith.uniformContinuous` states that for any two types `X` and `Y` that are pseudo e-metric spaces, and any non-negative real numbers `C` and `r`, if a function `f` from `X` to `Y` is Hölder continuous with constant `C` and exponent `r`, and if `r` is greater than zero, then `f` is uniformly continuous. In other words, a Hölder continuous function, where the exponent is greater than zero, ensures that the output of the function changes at a rate that is no faster than a fixed multiple of the input change raised to the power of the exponent, is also uniformly continuous, i.e., if two input points are close to each other, their corresponding output points are also close to each other, regardless of their location in the input set.
More concisely: If `f` is a Hölder continuous function from a pseudo-metric space `X` to another pseudo-metric space `Y` with constant `C` and exponent `r` > 0, then `f` is uniformly continuous on `X`.
|
HolderOnWith.edist_le
theorem HolderOnWith.edist_le :
∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal}
{f : X → Y} {s : Set X},
HolderOnWith C r f s → ∀ {x y : X}, x ∈ s → y ∈ s → edist (f x) (f y) ≤ ↑C * edist x y ^ ↑r
The theorem `HolderOnWith.edist_le` states that for any two types `X` and `Y` that each forms a PseudoEMetricSpace, any non-negative real numbers `C` and `r`, any function `f` from `X` to `Y`, and any set `s` of elements of type `X`, if `f` is Hölder continuous with constant `C` and exponent `r` on the set `s`, then for any two elements `x` and `y` in the set `s`, the extended distance between `f(x)` and `f(y)` is less than or equal to `C` times the extended distance between `x` and `y` raised to the power `r`. In other words, `edist (f x) (f y) ≤ C * edist x y ^ r` for all `x,y ∈ s`.
More concisely: For any Hölder continuous function f between two pseudo-metric spaces X and Y with constant C and exponent r, and for any x, y in X, the extended distance between f(x) and f(y) is less than or equal to C times the extended distance between x and y raised to the power of r.
|
holderOnWith_univ
theorem holderOnWith_univ :
∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal}
{f : X → Y}, HolderOnWith C r f Set.univ ↔ HolderWith C r f
This theorem is about the equivalence of the two definitions of Hölder continuity in the context of pseudo-emetric spaces. For all pseudo-emetric spaces `X` and `Y`, a non-negative real number `C`, a non-negative real number `r`, and a function `f` from `X` to `Y`, the theorem states that `f` is Hölder continuous with constant `C` and exponent `r` on the universal set of `X` (which includes all elements of `X`) if and only if `f` is Hölder continuous with constant `C` and exponent `r` on `X`. In other words, a function is Hölder continuous on the entire space `X` if and only if it is Hölder continuous for every pair of points in `X`.
More concisely: A function between pseudo-metric spaces is Hölder continuous with constant C and exponent r on the entire space if and only if it is Hölder continuous with that constant and exponent between any two points in the space.
|