Metric.uniformCauchySeqOn_iff
theorem Metric.uniformCauchySeqOn_iff :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : Nonempty β] [inst_2 : SemilatticeSup β]
{γ : Type u_3} {F : β → γ → α} {s : Set γ},
UniformCauchySeqOn F Filter.atTop s ↔ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, ∀ x ∈ s, dist (F m x) (F n x) < ε
This theorem states that in a pseudometric space, a sequence is uniformly Cauchy on a given set if and only if for any positive number ε, there exists some element of the sequence after which the distance between any two sequence elements is less than ε for all elements in the set. Here, the sequence is represented by a function from an ordered type with a least upper bound property into the set of elements in the pseudometric space. The sequence is considered to be uniformly Cauchy on a set of elements if the pairwise distances between sequence values (considering those elements from the set) are arbitrarily small from a certain point onwards. This characterizes the notion of the sequence "converging" in the pseudometric space.
More concisely: In a pseudometric space, a sequence is uniformly Cauchy on a set if and only if for every ε > 0, there exists an index N such that the distance between sequence elements i and j is less than ε for all i, j >= N and i, j in the set.
|
cauchySeq_bdd
theorem cauchySeq_bdd :
∀ {α : Type u} [inst : PseudoMetricSpace α] {u : ℕ → α}, CauchySeq u → ∃ R > 0, ∀ (m n : ℕ), dist (u m) (u n) < R
This theorem states that for every Cauchy sequence `u` of elements from a pseudo-metric space `α` indexed by the natural numbers, there exists a positive real number `R` such that the distance between any two elements `u m` and `u n` in the sequence is less than `R`. In other words, a Cauchy sequence on the natural numbers is always bounded.
More concisely: Every Cauchy sequence in a pseudo-metric space is bounded.
|
Metric.cauchySeq_iff
theorem Metric.cauchySeq_iff :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : Nonempty β] [inst_2 : SemilatticeSup β]
{u : β → α}, CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ m ≥ N, ∀ n ≥ N, dist (u m) (u n) < ε
In a pseudometric space, a sequence is a Cauchy sequence if and only if, given any positive number ε, there is a point in the sequence beyond which the distance between any two points is less than ε. This theorem is formally defined over any type α, with a pseudometric space structure, and any type β, which is nonempty and equipped with a semilattice sup structure. The sequence u is a function from β to α.
More concisely: In a pseudometric space, a sequence is Cauchy if and only if for every positive ε, there exists a index beyond which the distance between sequence elements is less than ε.
|
Metric.complete_of_cauchySeq_tendsto
theorem Metric.complete_of_cauchySeq_tendsto :
∀ {α : Type u} [inst : PseudoMetricSpace α],
(∀ (u : ℕ → α), CauchySeq u → ∃ a, Filter.Tendsto u Filter.atTop (nhds a)) → CompleteSpace α
This theorem states that a pseudo-metric space is complete if and only if every Cauchy sequence within that space converges. In the context of the theorem, a Cauchy sequence is defined as a sequence where the distance between any two later terms can be made arbitrarily small. Convergence here means that, given any sequence of elements in the pseudo-metric space, if the sequence is a Cauchy sequence, then there exists an element in the space such that the sequence approaches this element as it approaches infinity. The concept of approaching is defined using the notion of filters; in this case, `Filter.atTop` represents the limit of the sequence going to infinity, and `nhds a` represents the neighborhood of the element `a`. This theorem is a fundamental property of complete metric spaces in mathematics.
More concisely: A pseudo-metric space is complete if and only if every Cauchy sequence in it converges to a limit within the space.
|
cauchySeq_of_le_tendsto_0
theorem cauchySeq_of_le_tendsto_0 :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : Nonempty β] [inst_2 : SemilatticeSup β]
{s : β → α} (b : β → ℝ),
(∀ (n m N : β), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) → Filter.Tendsto b Filter.atTop (nhds 0) → CauchySeq s
This theorem states that for a sequence `s` indexed by a type `β`, if there exists a function `b` such that for all `n`, `m`, and `N` from `β` where `N` is less than or equal to `n` and `m`, the distance between the `n`th and `m`th terms of `s` is less than or equal to the `N`th term of `b`, and if `b` approaches 0 as `β` goes to infinity (i.e., `b` converges to zero), then `s` is a Cauchy sequence. A sequence is Cauchy if, as one goes further and further into the sequence, the elements get arbitrarily close to each other.
More concisely: If a sequence `s` indexed by `β` satisfies the condition that for all `n`, `m`, and `N` in `β` with `N ≤ m ≤ n`, the distance between `sn` and `sm` is less than or equal to the `N`th term of a converging-to-zero function `b`, then `s` is a Cauchy sequence.
|
cauchySeq_of_le_tendsto_0'
theorem cauchySeq_of_le_tendsto_0' :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : Nonempty β] [inst_2 : SemilatticeSup β]
{s : β → α} (b : β → ℝ),
(∀ (n m : β), n ≤ m → dist (s n) (s m) ≤ b n) → Filter.Tendsto b Filter.atTop (nhds 0) → CauchySeq s
The theorem `cauchySeq_of_le_tendsto_0'` states that for any type `α` with a pseudo metric space structure, any type `β` that is nonempty and has a sup-semilattice structure, and a function `s : β → α`, if there exists a function `b : β → ℝ` such that for all `n` and `m` in `β` with `n ≤ m`, the distance between `s n` and `s m` is less than or equal to `b n`, and `b` tends to 0 as `β` tends to infinity, then `s` is a Cauchy sequence. In other words, if the distance between each pair of terms of the sequence `s` is bounded by a function that converges to 0, then `s` is a Cauchy sequence.
More concisely: If for any pseudo metric space `(α, d)` and sup-semilattice `(β, ≤)`, and a function `s : β → α` with `β` nonempty, there exists a function `b : β → ℝ` such that `d(s n, s m) ≤ b n` for all `n ≤ m`, and `b` converges to 0, then `s` is a Cauchy sequence.
|
cauchySeq_iff_le_tendsto_0
theorem cauchySeq_iff_le_tendsto_0 :
∀ {α : Type u} [inst : PseudoMetricSpace α] {s : ℕ → α},
CauchySeq s ↔
∃ b,
(∀ (n : ℕ), 0 ≤ b n) ∧
(∀ (n m N : ℕ), N ≤ n → N ≤ m → dist (s n) (s m) ≤ b N) ∧ Filter.Tendsto b Filter.atTop (nhds 0)
This theorem provides another metric characterization of Cauchy sequences on integers. It states that for any sequence `s` of elements in a pseudometric space `α`, `s` is a Cauchy sequence if and only if there exists a sequence `b` of non-negative integers such that for any integers `n`, `m`, and `N`, if `N` is less than or equal to both `n` and `m`, then the distance between `s n` and `s m` is less than or equal to `b N` and also that `b` tends to zero as `N` tends to infinity. In other words, a sequence is Cauchy if it becomes arbitrarily close as we go far enough into the sequence.
More concisely: A sequence of elements in a pseudometric space is Cauchy if and only if there exists a sequence of non-negative integers tending to zero such that the sequence's pairwise distances are bounded by the corresponding terms.
|
Metric.cauchySeq_iff'
theorem Metric.cauchySeq_iff' :
∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : Nonempty β] [inst_2 : SemilatticeSup β]
{u : β → α}, CauchySeq u ↔ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (u n) (u N) < ε
This theorem establishes a variant of the pseudometric characterization of Cauchy sequences. Specifically, it states that for any types `α` and `β`, where `α` has a structure of a pseudometric space, `β` is nonempty and has a structure of a semilattice with supremum, and `u` is a function from `β` to `α`, then `u` is a Cauchy sequence if and only if for every positive real number `ε`, there exists an element `N` in `β` such that for all `n` in `β` greater than or equal to `N`, the distance between `u(n)` and `u(N)` is less than `ε`.
More concisely: A function from a semilattice with supremum to a pseudometric space is a Cauchy sequence if and only if for every ε > 0, there exists an element N such that the distance between f(N) and f(n) < ε for all n ≥ N.
|
Metric.complete_of_convergent_controlled_sequences
theorem Metric.complete_of_convergent_controlled_sequences :
∀ {α : Type u} [inst : PseudoMetricSpace α] (B : ℕ → ℝ),
(∀ (n : ℕ), 0 < B n) →
(∀ (u : ℕ → α),
(∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < B N) → ∃ x, Filter.Tendsto u Filter.atTop (nhds x)) →
CompleteSpace α
This theorem establishes a criterion for proving that a space is complete. In a pseudo-metric space, if there exists a sequence of real numbers (defined by `B : ℕ → ℝ`) such that every term is positive (`∀ (n : ℕ), 0 < B n`), and for any sequence in the space (`u : ℕ → α`), the distance between any two points in the sequence beyond a certain index `N` is less than the `N`'th term of the sequence of real numbers (`∀ (N n m : ℕ), N ≤ n → N ≤ m → dist (u n) (u m) < B N`); then, the sequence `u` converges in the space. If this holds true for all such sequences, then the pseudo-metric space is complete. The criterion is especially useful when `B N = 2^{-N}`, making it possible to use arguments of converging series.
More concisely: In a pseudo-metric space, if there exists a sequence `(B : ℕ → ℝ)` of positive real numbers such that for any `u : ℕ → α` sequence, if the distance between any two points `u n` and `u m` is less than `B n` for all `N ≤ n, m`, then `u` converges and the space is complete.
|