CauSeq.eq_lim_of_const_equiv
theorem CauSeq.eq_lim_of_const_equiv :
∀ {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst_1 : Ring β] {abv : β → α}
[inst_2 : IsAbsoluteValue abv] [inst_3 : CauSeq.IsComplete β abv] {f : CauSeq β abv} {x : β},
CauSeq.const abv x ≈ f → x = f.lim
The theorem `CauSeq.eq_lim_of_const_equiv` states that for any linearly ordered field `α`, a ring `β`, an absolute value function `abv` from `β` to `α`, a completeness instance for Cauchy sequences over `β` with respect to the absolute value `abv`, and a Cauchy sequence `f` over `β` with respect to the absolute value `abv` and an element `x` of `β`, if the constant Cauchy sequence at `x` is equivalent to `f`, then `x` is equal to the limit of the Cauchy sequence `f`. In other words, if a constant sequence and another sequence are 'close enough' (in the sense of Cauchy equivalence), then the value of the constant sequence is the limit of the other sequence.
More concisely: If a constant sequence is Cauchy equivalent to a sequence in a linearly ordered field with respect to an absolute value function and completeness instance, then the limit of the sequence equals the constant value.
|
CauSeq.lim_eq_of_equiv_const
theorem CauSeq.lim_eq_of_equiv_const :
∀ {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst_1 : Ring β] {abv : β → α}
[inst_2 : IsAbsoluteValue abv] [inst_3 : CauSeq.IsComplete β abv] {f : CauSeq β abv} {x : β},
f ≈ CauSeq.const abv x → f.lim = x
The theorem `CauSeq.lim_eq_of_equiv_const` states that for any type `α` that forms a linear ordered field, a type `β` that forms a ring, a function `abv` that assigns an absolute value from `β` to `α`, and given that `β` forms a complete Cauchy sequence with respect to `abv`, if a Cauchy sequence `f` is equivalent to a constant sequence with value `x`, then the limit of `f` is that same constant value `x`. In other words, if the difference between all the terms in the sequence `f` and a fixed constant `x` get arbitrarily small, then the limit of the sequence `f` is `x`.
More concisely: If `f` is a Cauchy sequence in a linearly ordered field `α` with respect to an absolute value from a complete ring `β`, and `f` is equivalent to the constant sequence with value `x`, then the limit of `f` equals `x`.
|
CauSeq.IsComplete.isComplete
theorem CauSeq.IsComplete.isComplete :
∀ {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst_1 : Ring β] {abv : β → α}
[inst_2 : IsAbsoluteValue abv] [self : CauSeq.IsComplete β abv] (s : CauSeq β abv), ∃ b, s ≈ CauSeq.const abv b
This theorem states that for any given Cauchy sequence `s`, there exists a limit `b`. In the context of a linearly ordered field `α` and a ring `β`, along with an absolute value function `abv` from `β` to `α`, the theorem asserts that every `β`-valued Cauchy sequence with respect to `abv` has a limit. Here, the equivalence of the Cauchy sequence `s` and the constant Cauchy sequence at `b` implies that `b` is the limit of the sequence `s`.
More concisely: In a linearly ordered field with an absolute value function, every Cauchy sequence has a limit.
|
CauSeq.Completion.mk_smul
theorem CauSeq.Completion.mk_smul :
∀ {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst_1 : Ring β] {abv : β → α}
[inst_2 : IsAbsoluteValue abv] {γ : Type u_3} [inst_3 : SMul γ β] [inst_4 : IsScalarTower γ β β] (c : γ)
(f : CauSeq β abv), c • CauSeq.Completion.mk f = CauSeq.Completion.mk (c • f)
This theorem, named `CauSeq.Completion.mk_smul`, states that for any scalar `c` of type `γ` and any Cauchy sequence `f` of type `β` with respect to an absolute value function `abv`, the action of scalar multiplication on the result of mapping `f` into the Cauchy completion (i.e., `c • CauSeq.Completion.mk f`) equals the result of mapping the scalar multiplication of `c` and `f` into the Cauchy completion (i.e., `CauSeq.Completion.mk (c • f)`). Here, the types `α`, `β`, and `γ` are equipped with the structures of a linear ordered field, a ring, and a scalar multiplication, respectively, and `abv` is an absolute value function on `β`. The scalar multiplication between `γ` and `β` forms a scalar tower over `β`, which means that scalar multiplication is associative between `γ` and `β`.
More concisely: For any scalar `c` of type `γ` and Cauchy sequence `f` of type `β` in a linear ordered field `α`, with respect to an absolute value function `abv`, the mapping of scalar multiplication `c • f` into the Cauchy completion is equal to scalar multiplication of `c` with the completion of `f`.
|
CauSeq.equiv_lim
theorem CauSeq.equiv_lim :
∀ {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst_1 : Ring β] {abv : β → α}
[inst_2 : IsAbsoluteValue abv] [inst_3 : CauSeq.IsComplete β abv] (s : CauSeq β abv),
s ≈ CauSeq.const abv s.lim
The theorem `CauSeq.equiv_lim` states that for any given Cauchy sequence `s` over a ring `β` with respect to an absolute value function `abv`, and given the conditions that `α` is a linearly ordered field, `abv` is a valid absolute value function and `β` is a complete ring with respect to `abv`, the sequence `s` is equivalent to the constant Cauchy sequence whose value is the limit of `s`. In other words, as you progress along the sequence, the elements of the sequence get arbitrarily close to the sequence's limit.
More concisely: For any Cauchy sequence `s` over a complete ring `β` with respect to an absolute value `abv` in a linearly ordered field `α`, the sequence `s` is equivalent to the constant sequence whose value is the limit of `s`.
|
CauSeq.Completion.mk_eq
theorem CauSeq.Completion.mk_eq :
∀ {α : Type u_1} [inst : LinearOrderedField α] {β : Type u_2} [inst_1 : Ring β] {abv : β → α}
[inst_2 : IsAbsoluteValue abv] {f g : CauSeq β abv}, CauSeq.Completion.mk f = CauSeq.Completion.mk g ↔ f ≈ g
The theorem `CauSeq.Completion.mk_eq` states that for any linearly ordered field `α` and ring `β` with a function `abv: β → α` that is an absolute value, and for any two Cauchy sequences `f, g` of `β` with respect to the absolute value `abv`, the sequences `f` and `g` are equivalent if and only if their respective completions under `CauSeq.Completion.mk` are equal. Here, a Cauchy sequence is a sequence where the difference between any two sufficiently far terms can be made arbitrarily small, and the completion refers to the process of filling in any "gaps" in a sequence to make it complete. The equivalence `f ≈ g` of two Cauchy sequences means that the difference between `f` and `g` becomes arbitrarily small for sufficiently large indices.
More concisely: For any linearly ordered field `α` and ring `β` with an absolute value function `abv`, two Cauchy sequences `f` and `g` in `β` with respect to `abv` are equivalent if and only if their completions under `CauSeq.Completion.mk` are equal.
|