Metric.equicontinuousAt_iff
theorem Metric.equicontinuousAt_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] {ι : Type u_4} [inst_1 : PseudoMetricSpace β]
{F : ι → β → α} {x₀ : β},
EquicontinuousAt F x₀ ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x : β), dist x x₀ < δ → ∀ (i : ι), dist (F i x₀) (F i x) < ε
This theorem provides a characterization of equicontinuity for families of functions between (pseudo) metric spaces. In particular, a family of functions `F : ι → β → α` is equicontinuous at a point `x₀ : β` if and only if for every positive real number `ε`, there exists a positive real number `δ` such that for all `x : β` within `δ` distance of `x₀`, the distance between `F i x₀` and `F i x` is less than `ε` for every `i : ι`. This means that around any point `x₀`, there is always a neighborhood within which all the functions `F i` change by less than `ε` when moving from `x₀` to any other point within the neighborhood.
More concisely: A family of functions between metric spaces is equicontinuous at a point if and only if for every ε, there exists δ such that the distance between each function's value at the point and its value at any point within δ distance is less than ε.
|
Metric.uniformEquicontinuous_iff
theorem Metric.uniformEquicontinuous_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] {ι : Type u_4} [inst_1 : PseudoMetricSpace β]
{F : ι → β → α},
UniformEquicontinuous F ↔ ∀ ε > 0, ∃ δ > 0, ∀ (x y : β), dist x y < δ → ∀ (i : ι), dist (F i x) (F i y) < ε
The theorem `Metric.uniformEquicontinuous_iff` is a characterization of uniform equicontinuity for families of functions between pseudometric spaces. It states that a family of functions `F` from `ι` to `β → α` is uniformly equicontinuous if and only if for every positive number `ε`, there exists a positive number `δ` such that for all pairs of points `(x, y)` in `β` with a distance less than `δ`, the distance between `F i x` and `F i y` is less than `ε` for all `i` in `ι`. In simpler terms, no matter how small we make `ε`, we can always find a `δ` so that whenever any two points in `β` are `δ`-close, their images under any function in the family `F` are `ε`-close.
More concisely: A family of functions from a pseudometric space to another is uniformly equicontinuous if and only if for every ε > 0, there exists δ > 0 such that the distance between any two points with distance less than δ in the domain results in functions values with distance less than ε.
|
Metric.uniformEquicontinuous_iff_right
theorem Metric.uniformEquicontinuous_iff_right :
∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] {ι : Type u_4} [inst_1 : UniformSpace β]
{F : ι → β → α},
UniformEquicontinuous F ↔ ∀ ε > 0, ∀ᶠ (xy : β × β) in uniformity β, ∀ (i : ι), dist (F i xy.1) (F i xy.2) < ε
This theorem is a characterization of uniform equicontinuity for families of functions that map into a pseudometric space. It states that a family of functions `F : ι → β → α`, where `α` is a pseudometric space and `β` is a uniform space, is uniformly equicontinuous if and only if, for every positive number `ε`, there exists an entourage (set of close pairs) in the uniform space `β` such that for any pair of points `(x, y)` in this entourage and for all `i : ι`, the distance between `F i x` and `F i y` in the pseudometric space `α` is less than `ε`. This essentially means that, as points in `β` come closer together, the images of these points under all functions in the family `F` also come closer together in `α`, uniformly for all functions in the family.
More concisely: A family of functions `F : ι → β → α` from a uniform space `β` to a pseudometric space `α` is uniformly equicontinuous if and only if for every `ε > 0`, there exists an entourage `E` in `β` such that for all `i : ι` and `(x, y)` in `E`, the distance between `F i x` and `F i y` in `α` is less than `ε`.
|
Metric.equicontinuousAt_iff_pair
theorem Metric.equicontinuousAt_iff_pair :
∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] {ι : Type u_4} [inst_1 : TopologicalSpace β]
{F : ι → β → α} {x₀ : β},
EquicontinuousAt F x₀ ↔ ∀ ε > 0, ∃ U ∈ nhds x₀, ∀ x ∈ U, ∀ x' ∈ U, ∀ (i : ι), dist (F i x) (F i x') < ε
The theorem `Metric.equicontinuousAt_iff_pair` is a reformulation of `equicontinuousAt_iff_pair` for families of functions taking values in a pseudo metric space. It states that a family of functions `F` from a topological space `β` to a pseudometric space `α` is equicontinuous at a point `x₀` in `β` if and only if for all real numbers `ε` greater than zero, there exists a neighborhood `U` of `x₀` such that for all points `x` and `x'` in `U` and for all indices `i` from set `ι`, the distance between `F(i, x)` and `F(i, x')` is less than `ε`.
More concisely: A family of functions from a topological space to a pseudometric space is equicontinuous at a point if and only if for every ε > 0, there exists a neighborhood of the point such that the distance between any two points in the neighborhood and the corresponding function values is less than ε for all functions in the family.
|
Metric.uniformEquicontinuous_of_continuity_modulus
theorem Metric.uniformEquicontinuous_of_continuity_modulus :
∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] {ι : Type u_4} [inst_1 : PseudoMetricSpace β]
(b : ℝ → ℝ),
Filter.Tendsto b (nhds 0) (nhds 0) →
∀ (F : ι → β → α), (∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)) → UniformEquicontinuous F
This theorem provides a convenient method to establish uniform equicontinuity for a family of functions mapping between pseudometric spaces. Specifically, it states that if all functions in the family share a common global continuity modulus represented by a function `b`, which tends to 0 as its input tends to 0, then the family of functions is uniformly equicontinuous. In other words, if for every two points `x` and `y` in the domain space, and every function `F i` in the family, the distance between `F i x` and `F i y` in the range space is less than or equal to `b` of the distance between `x` and `y`, then the family of functions is uniformly equicontinuous.
More concisely: If a family of functions between pseudometric spaces shares a common continuity modulus `b` such that for all `x, y` in the domain and all `F i` in the family, `d(F i x, F i y) ≤ b(d(x, y))`, then the family is uniformly equicontinuous.
|
Metric.equicontinuousAt_of_continuity_modulus
theorem Metric.equicontinuousAt_of_continuity_modulus :
∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] {ι : Type u_4} [inst_1 : TopologicalSpace β] {x₀ : β}
(b : β → ℝ),
Filter.Tendsto b (nhds x₀) (nhds 0) →
∀ (F : ι → β → α), (∀ᶠ (x : β) in nhds x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x) → EquicontinuousAt F x₀
The theorem `Metric.equicontinuousAt_of_continuity_modulus` states that for a family of functions from a topological space to a pseudometric space, a useful method to establish equicontinuity at a point is to demonstrate that all the functions have the same local continuity modulus. More formally, given any point `x₀` in the topological space, a function `b` from the topological space to the real numbers, and a family of functions `F`, if the function `b` tends to 0 as it approaches `x₀` and for every point `x` in the neighborhood of `x₀` the distance between `F i x₀` and `F i x` is less than or equal to `b x` for all `i`, then `F` is equicontinuous at `x₀`. This means that for every neighborhood of `F i x₀` in the pseudometric space, there exists a neighborhood of `x₀` such that all the values of `F i x` for `x` in this neighborhood and for all `i` are in the given neighborhood of `F i x₀`.
More concisely: If a family of functions from a topological space to a pseudometric space has the same local continuity modulus at a point, then the family is equicontinuous at that point.
|
Metric.equicontinuous_of_continuity_modulus
theorem Metric.equicontinuous_of_continuity_modulus :
∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] {ι : Type u_4} [inst_1 : PseudoMetricSpace β]
(b : ℝ → ℝ),
Filter.Tendsto b (nhds 0) (nhds 0) →
∀ (F : ι → β → α), (∀ (x y : β) (i : ι), dist (F i x) (F i y) ≤ b (dist x y)) → Equicontinuous F
The theorem `Metric.equicontinuous_of_continuity_modulus` states that for a family of functions `F` mapping from a pseudo metric space `β` to another pseudo metric space `α`, equicontinuity across the family can be established by demonstrating a common global continuity modulus. This common global continuity modulus is represented as a function `b` from real numbers to real numbers. It is required that `b` tends towards 0 as its input tends towards 0. The condition that serves as the definition of this common continuity modulus is that for every pair of points `x` and `y` in `β`, and for every function `i` in the family `F`, the distance between the images of `x` and `y` under `i` is less than or equal to `b` applied to the distance between `x` and `y`.
More concisely: A family of functions from a pseudo metric space to another pseudo metric space is equicontinuous if there exists a common continuity modulus function tending to 0, such that the image distance is less than or equal to the function value for all pairs of points and functions in the family.
|
Metric.equicontinuousAt_iff_right
theorem Metric.equicontinuousAt_iff_right :
∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] {ι : Type u_4} [inst_1 : TopologicalSpace β]
{F : ι → β → α} {x₀ : β},
EquicontinuousAt F x₀ ↔ ∀ ε > 0, ∀ᶠ (x : β) in nhds x₀, ∀ (i : ι), dist (F i x₀) (F i x) < ε
The theorem `Metric.equicontinuousAt_iff_right` provides a characterization of equicontinuity for families of functions `F : ι → β → α` mapping from a topological space `β` into a (pseudo)metric space `α`. Specifically, it states that a family `F` is equicontinuous at a point `x₀` in `β` if and only if for every positive real number `ε`, eventually for every `x` in the neighborhood of `x₀` (relative to the neighborhood filter at `x₀`), for every `i` in `ι`, the distance between `F i x₀` and `F i x` in `α` is less than `ε`. In other words, given any positive `ε`, there is a neighborhood around `x₀` such that the images under `F` of all points in the neighborhood are all within `ε` distance of `F i x₀`, for all `i`.
More concisely: A family of functions from a topological space into a (pseudo)metric space is equicontinuous at a point if and only if for every ε > 0, there exists a neighborhood of that point such that for all i and x in the neighborhood, the distance between F i(x₀) and F i(x) is less than ε.
|