CauSeq.const_lt
theorem CauSeq.const_lt :
∀ {α : Type u_1} [inst : LinearOrderedField α] {x y : α}, CauSeq.const abs x < CauSeq.const abs y ↔ x < y := by
sorry
The theorem `CauSeq.const_lt` states that for any type `α`, which forms a linearly ordered field, and for any two elements `x` and `y` of type `α`, the constant Cauchy sequence constructed from the absolute value of `x` is less than the constant Cauchy sequence constructed from the absolute value of `y` if and only if `x` is less than `y`. Essentially, this theorem is about the order preservation of constant Cauchy sequences with respect to the underlying field elements they are constructed from.
More concisely: For any linearly ordered field type `α`, the constant Cauchy sequence constructed from the absolute value of `x` is less element-wise than the constant Cauchy sequence constructed from the absolute value of `y` if and only if `x` is less than `y`.
|
CauSeq.lt_of_eq_of_lt
theorem CauSeq.lt_of_eq_of_lt :
∀ {α : Type u_1} [inst : LinearOrderedField α] {f g h : CauSeq α abs}, f ≈ g → g < h → f < h
The theorem `CauSeq.lt_of_eq_of_lt` states that for any linear ordered field `α` and for any Cauchy sequences `f`, `g`, and `h` of `α` with respect to the absolute value, if `f` is equivalent to `g` and `g` is less than `h`, then `f` is less than `h`. Essentially, this theorem is about the transitivity of inequality for Cauchy sequences in a specific context.
More concisely: For any linear ordered field `α` and Cauchy sequences `f`, `g`, and `h` of `α`, if `f` is equivalent to `g` and `g` is less than `h`, then `f` is less than `h`.
|
CauSeq.cauchy₃
theorem CauSeq.cauchy₃ :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst_1 : Ring β] {abv : β → α}
[inst_2 : IsAbsoluteValue abv] (f : CauSeq β abv) {ε : α}, 0 < ε → ∃ i, ∀ j ≥ i, ∀ k ≥ j, abv (↑f k - ↑f j) < ε
This theorem, named `CauSeq.cauchy₃`, states that for any types `α` and `β` where `α` is a linearly ordered field and `β` is a ring, and for any function `abv : β → α` that is an absolute value, any Cauchy sequence `f : CauSeq β abv` satisfies the following property: given any positive ε (`0 < ε`), there exists an index `i` such that for all indices `j` and `k` where `k` is greater than or equal to `j` and `j` is greater than or equal to `i`, the absolute value of the difference between the `k`-th term and the `j`-th term of the sequence (`abv (↑f k - ↑f j)`) is less than ε.
In other words, beyond a certain point in the sequence, the absolute difference between any two terms is less than any given positive number, which is a key characteristic of Cauchy sequences in mathematical analysis.
More concisely: For any Cauchy sequence `f` in a linearly ordered field `α` with absolute value function `abv : β → α`, where `β` is a ring, there exists an index `i` such that for all `j` and `k` with `k ≥ j ≥ i`, `|abv(f(k) - f(j))| < ε`.
|
CauSeq.lt_of_lt_of_eq
theorem CauSeq.lt_of_lt_of_eq :
∀ {α : Type u_1} [inst : LinearOrderedField α] {f g h : CauSeq α abs}, f < g → g ≈ h → f < h
This theorem states that for any linear ordered field `α`, if you have three Cauchy sequences `f`, `g`, and `h` of `α` with respect to the absolute value, and if `f` is less than `g` and `g` is approximately equal to `h`, then `f` is less than `h`. In terms of mathematical notation, this can be expressed as: for all `f, g, h ∈ CauSeq α abs`, if `f < g` and `g ≈ h`, then `f < h`. Essentially, this theorem captures a form of transitivity property of "less than" relation under the approximation in the context of Cauchy sequences.
More concisely: If `f`, `g`, and `h` are Cauchy sequences in a linear ordered field `α` such that `f < g` and `g` is close to `h`, then `f < h`.
|
CauSeq.le_of_exists
theorem CauSeq.le_of_exists :
∀ {α : Type u_1} [inst : LinearOrderedField α] {f g : CauSeq α abs}, (∃ i, ∀ j ≥ i, ↑f j ≤ ↑g j) → f ≤ g
This theorem asserts that, for any two Cauchy sequences `f` and `g` of elements from a linearly ordered field `α`, if there exists an index `i` such that for all indices `j` greater than or equal to `i`, the `j`-th term of `f` is less than or equal to the `j`-th term of `g`, then `f` is less than or equal to `g`. The function `abs` is used here to define the absolute value on the field `α`.
More concisely: If two Cauchy sequences in a linearly ordered field have `f(i) ≤ g(i)` for all `i` greater than some index, then `f ≤ g`.
|
CauSeq.ext
theorem CauSeq.ext :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst_1 : Ring β] {abv : β → α} {f g : CauSeq β abv},
(∀ (i : ℕ), ↑f i = ↑g i) → f = g
The theorem `CauSeq.ext` states that for any types `α` and `β`, where `α` is a linearly ordered field and `β` is a ring, given an absolute value function `abv` from `β` to `α` and any two Cauchy sequences `f` and `g` of `β` with respect to `abv`, if for every natural number `i`, the `i`-th term of `f` equals the `i`-th term of `g`, then `f` and `g` are the same Cauchy sequence. In other words, two Cauchy sequences are equal if and only if their corresponding elements are equal for all indices.
More concisely: If two Cauchy sequences over a linearly ordered field `α` and a ring `β` with respect to an absolute value function `abv` have equal terms for all indices, then they are equal Cauchy sequences.
|
CauSeq.coe_smul
theorem CauSeq.coe_smul :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst_1 : Ring β] {abv : β → α}
[inst_2 : IsAbsoluteValue abv] {G : Type u_3} [inst_3 : SMul G β] [inst_4 : IsScalarTower G β β] (a : G)
(f : CauSeq β abv), ↑(a • f) = a • ↑f
The theorem `CauSeq.coe_smul` states that for any linear ordered field α, ring β, an absolute value function 'abv' of β into α, a type G that is a scalar multiple on β, and an instance where β is a scalar tower over G and β, and given any element 'a' of G and any Cauchy sequence 'f' of type β with respect to the absolute value function 'abv', the coercion of the scalar multiplication of 'a' and 'f' equals to the scalar multiplication of 'a' and the coercion of 'f'.
More concisely: For any linear ordered field α, ring β with an absolute value function 'abv', scalar multiple type G over β and β, and elements 'a' in G and Cauchy sequence 'f' in β, the coercion of 'a' times 'f' equals 'a' times the coercion of 'f'.
|
IsCauSeq.cauchy₃
theorem IsCauSeq.cauchy₃ :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst_1 : Ring β] {abv : β → α}
[inst_2 : IsAbsoluteValue abv] {f : ℕ → β},
IsCauSeq abv f → ∀ {ε : α}, 0 < ε → ∃ i, ∀ j ≥ i, ∀ k ≥ j, abv (f k - f j) < ε
The theorem `IsCauSeq.cauchy₃` states that for any types `α` and `β`, where `α` is a linear ordered field and `β` is a ring, and for any function `abv` from `β` to `α` that is an absolute value, if a sequence of natural numbers to elements of `β` (`f` from `ℕ` to `β`) is a Cauchy sequence (as defined by `IsCauSeq`), then for any positive `ε` in `α`, there exists an index `i` such that for any indices `j` and `k` greater than or equal to `i` and `j` respectively, the absolute value of the difference between the `k`th and `j`th terms of the sequence is less than `ε`. In simple terms, the theorem asserts that if a sequence is Cauchy, then the distances between its later terms can be made as small as desired.
More concisely: Given a Cauchy sequence `f` of elements in a linear ordered field `α` with respect to an absolute value function `abv` from a ring `β` to `α`, for every positive `ε` in `α`, there exists an index `i` such that for all `j, k ≥ i`, `|abv(f(j) - f(k))| < ε`.
|
CauSeq.const_sub
theorem CauSeq.const_sub :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst_1 : Ring β] {abv : β → α}
[inst_2 : IsAbsoluteValue abv] (x y : β), CauSeq.const abv (x - y) = CauSeq.const abv x - CauSeq.const abv y
The theorem `CauSeq.const_sub` states that for any types `α` and `β`, where `α` is a linear ordered field and `β` is a ring, and for any absolute value function `abv : β → α`, the Cauchy sequence of the difference of two elements `x` and `y` in `β` (i.e. `CauSeq.const abv (x - y)`) is equal to the difference of the Cauchy sequences of `x` and `y` (i.e. `CauSeq.const abv x - CauSeq.const abv y`). This theorem shows that the constant Cauchy sequence operator distributes over subtraction in the ring `β`.
More concisely: For any linear ordered field `α` and ring `β` with an absolute value function `abv`, the constant Cauchy sequence of the difference of two elements in `β` is equal to the difference of their constant Cauchy sequences.
|
CauSeq.cauchy
theorem CauSeq.cauchy :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst_1 : Ring β] {abv : β → α} (f : CauSeq β abv)
{ε : α}, 0 < ε → ∃ i, ∀ j ≥ i, abv (↑f j - ↑f i) < ε
This theorem states that for any type `α` with a linearly ordered field structure and any type `β` with a ring structure, given an absolute value function `abv` from `β` to `α` and a Cauchy sequence `f` (with respect to the absolute value function `abv`), for any positive `ε` of type `α`, there exists an index `i` such that for all indices `j` greater than or equal to `i`, the absolute value of the difference between the `j`-th and `i`-th terms of the sequence `f` is less than `ε`. In other words, it states that a Cauchy sequence is such that, beyond some point, the elements of the sequence get arbitrarily close to each other.
More concisely: Given a linearly ordered field `α` and a ring `β` with an absolute value function `abv` from `β` to `α`, any Cauchy sequence in `β` with respect to `abv` converges to a limit in `β`.
|
CauSeq.bounded'
theorem CauSeq.bounded' :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst_1 : Ring β] {abv : β → α}
[inst_2 : IsAbsoluteValue abv] (f : CauSeq β abv) (x : α), ∃ r > x, ∀ (i : ℕ), abv (↑f i) < r
This theorem states that for any Cauchy sequence `f` of type `β` with respect to an absolute value function `abv`, and for any arbitrary number `x` of type `α`, there exists a number `r` greater than `x` such that the absolute value of the `i`-th term of the sequence `f` is less than `r` for all natural numbers `i`. In other words, every term of the Cauchy sequence `f` is bounded above by some number `r` that is greater than a given number `x`.
More concisely: For any Cauchy sequence `f` of type `β` with respect to an absolute value function `abv`, and for any `x` of type `α`, there exists a number `r > x` such that `|f i| < r` for all natural numbers `i`.
|
CauSeq.const_neg
theorem CauSeq.const_neg :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst_1 : Ring β] {abv : β → α}
[inst_2 : IsAbsoluteValue abv] (x : β), CauSeq.const abv (-x) = -CauSeq.const abv x
The theorem `CauSeq.const_neg` states that for any types `α` and `β`, where `α` is a linearly ordered field and `β` is a ring, and for any absolute value function `abv` from `β` to `α`, the constant Cauchy sequence of the negation of a value `x` (from the ring `β`) is equal to the negation of the constant Cauchy sequence of `x`. In mathematical terms, it's saying that in this setting, negating `x` before or after forming the constant Cauchy sequence doesn't make a difference—the two resulting sequences are the same.
More concisely: For any linearly ordered field `α`, ring `β`, and absolute value function `abv` from `β` to `α`, the constant Cauchy sequences of `x` and `-x` are equal for all `x` in `β`.
|
CauSeq.add_limZero
theorem CauSeq.add_limZero :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst_1 : Ring β] {abv : β → α}
[inst_2 : IsAbsoluteValue abv] {f g : CauSeq β abv}, f.LimZero → g.LimZero → (f + g).LimZero
The theorem `CauSeq.add_limZero` states that for any ordered field `α`, any ring `β`, and any absolute value `abv` from `β` to `α`, if `f` and `g` are Cauchy sequences with respect to the absolute value `abv` and both `f` and `g` approach zero, then the sum of `f` and `g` also approaches zero. This is a property of limit arithmetic in the context of Cauchy sequences, which extends the idea that the limit of the sum of two sequences is the sum of their limits.
More concisely: If `f` and `g` are Cauchy sequences over an ordered field `α` with respect to an absolute value `abv` and `abv(lim f) = abv(lim g) = 0`, then `abv(lim (f + g)) = 0`.
|
CauSeq.neg_limZero
theorem CauSeq.neg_limZero :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst_1 : Ring β] {abv : β → α}
[inst_2 : IsAbsoluteValue abv] {f : CauSeq β abv}, f.LimZero → (-f).LimZero
The theorem `CauSeq.neg_limZero` states that for any Cauchy sequence `f` of values from a ring `β` with respect to an absolute value function `abv` in a linearly ordered field `α`, if `f` approaches zero, then the negation of `f` also approaches zero. In other words, if `f` is a sequence such that the absolute value of its elements gets arbitrarily close to zero as we proceed further in the sequence, the same is true for the sequence formed by taking the negation of each element in `f`.
More concisely: If `f` is a Cauchy sequence in the ring `β` with respect to the absolute value `abv` in the linearly ordered field `α`, and `lim (abv (f.n)) = 0`, then `lim (abv (neg (f.n))) = 0`.
|
CauSeq.mul_limZero_right
theorem CauSeq.mul_limZero_right :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst_1 : Ring β] {abv : β → α}
[inst_2 : IsAbsoluteValue abv] (f : CauSeq β abv) {g : CauSeq β abv}, g.LimZero → (f * g).LimZero
The theorem `CauSeq.mul_limZero_right` states that for any given types `α` and `β` where `α` is a linear ordered field and `β` is a ring, and a function `abv` from `β` to `α` that is an absolute value, if `f` is a Cauchy sequence of `β` with respect to `abv` and `g` is another such Cauchy sequence that approaches zero, then the product of `f` and `g` also approaches zero. Here, a sequence is said to approach zero if for every positive number `ε`, there exists an index `i` such that the absolute value of every term indexed by `j ≥ i` is less than `ε`.
More concisely: If `f` and `g` are Cauchy sequences of a ring `β` with respect to an absolute value function `abv` from `β` to a linear ordered field `α`, then their product approaches zero if both `f` and `g` approach zero.
|
CauSeq.const_limZero
theorem CauSeq.const_limZero :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst_1 : Ring β] {abv : β → α}
[inst_2 : IsAbsoluteValue abv] {x : β}, (CauSeq.const abv x).LimZero ↔ x = 0
The theorem `CauSeq.const_limZero` states that for any types `α` and `β`, where `α` is a linearly ordered field and `β` is a ring, and for any absolute value function `abv` from `β` to `α`, and any element `x` of `β`, the constant Cauchy sequence `CauSeq.const abv x` approaches zero (i.e., `CauSeq.LimZero (CauSeq.const abv x)`) if and only if the constant value `x` is zero. In other words, a constant Cauchy sequence in a given ring converges to zero under a certain absolute value if and only if the constant of the sequence is zero.
More concisely: A constant Cauchy sequence in a ring with respect to a given absolute value function converges to zero if and only if the constant term is zero.
|
CauSeq.const_equiv
theorem CauSeq.const_equiv :
∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrderedField α] [inst_1 : Ring β] {abv : β → α}
[inst_2 : IsAbsoluteValue abv] {x y : β}, CauSeq.const abv x ≈ CauSeq.const abv y ↔ x = y
The theorem `CauSeq.const_equiv` states that for any types `α` and `β`, where `α` is a linear ordered field and `β` is a ring, and for any absolute value function `abv` from `β` to `α`, and any elements `x` and `y` of `β`, the constant Cauchy sequences with values `x` and `y` are equivalent (as defined by the equivalence relation ≈ on Cauchy sequences) if and only if `x` equals `y`. In other words, two constant Cauchy sequences are equivalent precisely when they are constant for the same value.
More concisely: For any linear ordered field `α`, ring `β`, absolute value function `abv` from `β` to `α`, and elements `x, y` of `β`, the constant Cauchy sequences over `β` with values `x` and `y` are equivalent if and only if `x = y`.
|