Hyperreal.ofSeq_surjective
theorem Hyperreal.ofSeq_surjective : Function.Surjective Hyperreal.ofSeq
The theorem `Hyperreal.ofSeq_surjective` asserts that the function `Hyperreal.ofSeq`, which constructs a hyperreal number from a sequence of real numbers, is surjective. In other words, for every hyperreal number, there exists a sequence of real numbers such that the hyperreal number is the image of this sequence under the `Hyperreal.ofSeq` function.
More concisely: For every hyperreal number, there exists a sequence of real numbers whose `Hyperreal.ofSeq` image equals that hyperreal number.
|
Hyperreal.IsSt.add
theorem Hyperreal.IsSt.add : ∀ {x y : ℝ*} {r s : ℝ}, x.IsSt r → y.IsSt s → (x + y).IsSt (r + s)
The theorem `Hyperreal.IsSt.add` states that for any hyperreal numbers `x` and `y`, and any real numbers `r` and `s`, if `x` is infinitesimally close to `r` and `y` is infinitesimally close to `s` (as defined by the `Hyperreal.IsSt` predicate), then the sum of `x` and `y` is infinitesimally close to the sum of `r` and `s`. This theorem essentially asserts the preservation of the "closeness" relation under addition in the hyperreal number system.
More concisely: For any hyperreal numbers `x` and `y` infinitesimally close to real numbers `r` and `s` respectively, `x + y` is infinitesimally close to `r + s`.
|
Hyperreal.coe_eq_coe
theorem Hyperreal.coe_eq_coe : ∀ {x y : ℝ}, ↑x = ↑y ↔ x = y
This theorem states that for all real numbers `x` and `y`, the hyperreal representation of `x` (notated as ↑x) is equal to the hyperreal representation of `y` (notated as ↑y) if and only if `x` is equal to `y`. In other words, the function that maps real numbers to their hyperreal counterparts preserves equality.
More concisely: For all real numbers x and y, ↑x = ↑y if and only if x = y.
|
Hyperreal.coe_le_coe
theorem Hyperreal.coe_le_coe : ∀ {x y : ℝ}, ↑x ≤ ↑y ↔ x ≤ y
This theorem establishes the relationship between the order of real numbers and their corresponding hyperreal numbers. Specifically, it states that for all real numbers 'x' and 'y', 'x' is less than or equal to 'y' if and only if the hyperreal number corresponding to 'x' is less than or equal to the hyperreal number corresponding to 'y'. In other words, the order is preserved when real numbers are embedded into the hyperreal numbers.
More concisely: For all real numbers x and y, x ≤ y if and only if x��uld ≤ y��uld, where x��uld and y��uld denote the hyperreal numbers corresponding to x and y, respectively.
|
Hyperreal.IsSt.map₂
theorem Hyperreal.IsSt.map₂ :
∀ {x y : ℝ*} {r s : ℝ},
x.IsSt r →
y.IsSt s →
∀ {f : ℝ → ℝ → ℝ},
ContinuousAt (Function.uncurry f) (r, s) → Hyperreal.IsSt (Filter.Germ.map₂ f x y) (f r s)
The theorem `Hyperreal.IsSt.map₂` states that for any two extended real numbers `x` and `y`, with corresponding standard parts `r` and `s`, and any binary function `f` from real numbers to real numbers, if `f` is continuous at the point `(r, s)`, then the standard part of the mapped germ of `f` on `x` and `y` is `f(r, s)`. In other words, if `f` is a continuous binary function, the standard part of the result of applying `f` to any two hyperreal numbers `x` and `y` is the same as applying `f` to the standard parts of `x` and `y`.
More concisely: For any continuous binary function f and hyperreal numbers x and y with standard parts r and s, respectively, the standard part of f(x, y) is f(r, s).
|
Hyperreal.infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos
theorem Hyperreal.infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos :
∀ {x y : ℝ*}, x.InfiniteNeg → ¬y.Infinitesimal → 0 < y → (x * y).InfiniteNeg
The theorem `Hyperreal.infiniteNeg_mul_of_infiniteNeg_not_infinitesimal_pos` asserts that for all hyperreal numbers 'x' and 'y', if 'x' is negative infinite (i.e., it is smaller than all real numbers) and 'y' is not infinitesimal (i.e., its standard part is not zero) with 'y' being positive, then the product of 'x' and 'y' is also negative infinite.
More concisely: If x is negative infinite and y is a positive hyperreal number that is not infinitesimal, then x * y is negative infinite.
|
Hyperreal.infiniteNeg_iff_infinitesimal_inv_neg
theorem Hyperreal.infiniteNeg_iff_infinitesimal_inv_neg : ∀ {x : ℝ*}, x.InfiniteNeg ↔ x⁻¹.Infinitesimal ∧ x⁻¹ < 0 := by
sorry
The theorem `Hyperreal.infiniteNeg_iff_infinitesimal_inv_neg` establishes an equivalence between two properties of hyperreal numbers. Specifically, it states that for any hyperreal number `x`, `x` is negatively infinite if and only if the inverse of `x` is infinitesimal and negative. In other words, a hyperreal number `x` is smaller than all real numbers if and only if the reciprocal of `x` is infinitesimally close to zero and is negative.
More concisely: A hyperreal number `x` is negatively infinite if and only if its multiplicative inverse is an infinitesimal negative.
|
Hyperreal.isSt_refl_real
theorem Hyperreal.isSt_refl_real : ∀ (r : ℝ), (↑r).IsSt r
This theorem states that for every real number `r`, `r` is the standard part of its hyperreal extension. In the context of hyperreal numbers, the standard part of a hyperreal number is the real number that is infinitesimally close to it. The `Hyperreal.IsSt` function captures this concept, and the theorem `Hyperreal.isSt_refl_real` asserts that the standard part of the hyperreal extension of a real number `r` is `r` itself. In other words, every real number is infinitesimally close to its hyperreal counterpart.
More concisely: Every real number is equal to its standard part in its hyperreal extension.
|
Hyperreal.isSt_ofSeq_iff_tendsto
theorem Hyperreal.isSt_ofSeq_iff_tendsto :
∀ {f : ℕ → ℝ} {r : ℝ}, (Hyperreal.ofSeq f).IsSt r ↔ Filter.Tendsto f (↑(Filter.hyperfilter ℕ)) (nhds r)
This theorem establishes an equivalence between two properties of a sequence `f` of real numbers and a real number `r`. On one hand, it states that `r` is the standard part of the hyperreal number constructed from the sequence `f`, denoted as `Hyperreal.IsSt (Hyperreal.ofSeq f) r`. On the other hand, it asserts that the sequence `f` converges to `r` under the ultrafilter extending the cofinite filter (in other words, almost all elements of the sequence are close to `r`), denoted as `Filter.Tendsto f (↑(Filter.hyperfilter ℕ)) (nhds r)`. The equivalence between these two conditions implies that the standard part of a hyperreal number is the limit point of the sequence from which the hyperreal number is constructed, when the limit is taken under the hyperfilter, a certain type of ultrafilter.
More concisely: The theorem states that a real number `r` is the standard part of the hyperreal number constructed from a convergent sequence `f` of real numbers if and only if `f` converges to `r` under the ultrafilter extending the cofinite filter.
|
Hyperreal.exists_st_of_not_infinite
theorem Hyperreal.exists_st_of_not_infinite : ∀ {x : ℝ*}, ¬x.Infinite → ∃ r, x.IsSt r
The theorem `Hyperreal.exists_st_of_not_infinite` states that for every hyperreal number `x`, if `x` is not infinite, then there exists a real number `r` such that `r` is the standard part of `x`. In other words, for any real number `δ` greater than zero, `x` lies within the interval from `r - δ` to `r + δ`. This captures the idea that if a hyperreal number is not infinitely large or small, it must be close to some standard real number, within any given margin.
More concisely: For every hyperreal number `x` that is not infinite, there exists a real number `r` such that `x` lies within the interval `(r - δ, r + δ)` for any positive real `δ`. In other words, the standard part `r` of `x` exists and approximates `x` arbitrarily closely.
|
Hyperreal.infinitesimal_def
theorem Hyperreal.infinitesimal_def : ∀ {x : ℝ*}, x.Infinitesimal ↔ ∀ (r : ℝ), 0 < r → -↑r < x ∧ x < ↑r
The theorem `Hyperreal.infinitesimal_def` states that for every hyperreal number 'x', 'x' is infinitesimal if and only if for every real number 'r' greater than zero, 'x' lies in the interval (-r, r). In other words, a hyperreal number is infinitesimal if and only if it is strictly between the negated and the positive representation of every positive real number.
More concisely: A hyperreal number is infinitesimal if and only if it lies strictly between the negated and positive representations of every positive real number.
|
Hyperreal.IsSt.not_infinite
theorem Hyperreal.IsSt.not_infinite : ∀ {x : ℝ*} {r : ℝ}, x.IsSt r → ¬x.Infinite
The theorem `Hyperreal.IsSt.not_infinite` states that for any hyperreal number `x` and any real number `r`, if `x` is the standard part of `r` (denoted as `Hyperreal.IsSt x r`, meaning that `x` is within any infinitesimal distance from `r`), then `x` cannot be an infinite hyperreal number. In other words, a standard part of a real number cannot be infinitely large or infinitely small.
More concisely: A real number's standard part is finite in the hyperreal numbers.
|
Hyperreal.Infinite.st_eq
theorem Hyperreal.Infinite.st_eq : ∀ {x : ℝ*}, x.Infinite → x.st = 0
This theorem states that for any hyperreal number `x`, if `x` is infinite (either infinitely positive or infinitely negative), then the standard part of `x` is equal to zero. The standard part of a hyperreal number, denoted `Hyperreal.st x`, is similar to rounding, but rounds to the nearest real number rather than the nearest integer. In the context of this theorem, it means that an infinitely large or small hyperreal number is rounded to zero.
More concisely: For any hyperreal number `x`, if `x` is infinite then its standard part is equal to zero.
|
Hyperreal.eq_of_isSt_real
theorem Hyperreal.eq_of_isSt_real : ∀ {r s : ℝ}, (↑r).IsSt s → r = s
The theorem `Hyperreal.eq_of_isSt_real` states that for any two real numbers `r` and `s`, if the standard part of the hyperreal number corresponding to `r` is `s`, then `r` and `s` must be identical. The standard part of a hyperreal number `x` is a real number `r` such that for all positive real numbers `δ`, `x` lies between `r - δ` and `r + δ`.
More concisely: For any real numbers `r` and `s`, if the standard part of the hyperreal number `r` is equal to `s`, then `r` and `s` are identical.
|
Hyperreal.ofSeq_lt_ofSeq
theorem Hyperreal.ofSeq_lt_ofSeq :
∀ {f g : ℕ → ℝ}, Hyperreal.ofSeq f < Hyperreal.ofSeq g ↔ ∀ᶠ (n : ℕ) in ↑(Filter.hyperfilter ℕ), f n < g n := by
sorry
This theorem, `Hyperreal.ofSeq_lt_ofSeq`, states that for any two sequences of real numbers `f` and `g`, the hyperreal number constructed from sequence `f` is less than the hyperreal number constructed from sequence `g` if and only if for "almost all" natural numbers `n` (in the sense of the ultrafilter extending the cofinite filter), the `n`-th term of sequence `f` is less than the `n`-th term of sequence `g`.
More concisely: For any sequences of real numbers `f` and `g`, their corresponding hyperreal numbers satisfy the relationship `Hyperreal.ofSeq f < Hyperreal.ofSeq g` if and only if `f(n) < g(n)` for all but finitely many natural numbers `n`.
|
Hyperreal.infinitePos_mul_of_infiniteNeg_not_infinitesimal_neg
theorem Hyperreal.infinitePos_mul_of_infiniteNeg_not_infinitesimal_neg :
∀ {x y : ℝ*}, x.InfiniteNeg → ¬y.Infinitesimal → y < 0 → (x * y).InfinitePos
The theorem states that for any two hyperreal numbers `x` and `y`, if `x` is negative infinite (meaning it is less than all real numbers), `y` is not infinitesimal (meaning its standard part is not zero), and `y` is less than zero, then the product of `x` and `y` is positive infinite (meaning it is greater than all real numbers). In other words, a product of a negative infinite hyperreal number and a negative non-infinitesimal hyperreal number is a positive infinite hyperreal number.
More concisely: For any hyperreal numbers `x` and `y`, if `x` is negative infinite and `y` is a non-infinitesimal negative number, then `x * y` is positive infinite.
|
Hyperreal.infiniteNeg_mul_of_infinitePos_not_infinitesimal_neg
theorem Hyperreal.infiniteNeg_mul_of_infinitePos_not_infinitesimal_neg :
∀ {x y : ℝ*}, x.InfinitePos → ¬y.Infinitesimal → y < 0 → (x * y).InfiniteNeg
The theorem states that given any two hyperreal numbers 'x' and 'y', if 'x' is positively infinite (meaning it is larger than any real number) and 'y' is not infinitesimal (meaning its standard part is not zero) and 'y' is less than zero, then the product of 'x' and 'y' is negatively infinite (meaning it is smaller than any real number).
More concisely: If x is a positively infinite hyperreal number and y is a finite negative non-zero hyperreal number, then x * y is negatively infinite.
|
Hyperreal.isSt_sSup
theorem Hyperreal.isSt_sSup : ∀ {x : ℝ*}, ¬x.Infinite → x.IsSt (sSup {y | ↑y < x})
This theorem states that for every hyperreal number `x` that is not infinite, the standard part of `x` is the supremum of the set of all real numbers `y` that are strictly less than `x`. In other words, if `x` is a hyperreal number that is not infinitely large or infinitely small, then the closest real number to `x` (in a sense made precise by the `IsSt` predicate) is the least upper bound (or supremum, denoted by `sSup`) of all the real numbers that are less than `x`.
More concisely: For every finite hyperreal number `x`, the real number `sSup { y | y < x }` is the standard part of `x`.
|
Hyperreal.IsSt.st_eq
theorem Hyperreal.IsSt.st_eq : ∀ {x : ℝ*} {r : ℝ}, x.IsSt r → x.st = r
The theorem `Hyperreal.IsSt.st_eq` states that for any hyperreal number `x` and any real number `r`, if `r` is the standard part of `x` (i.e., `r` is as close to `x` as possible, but still a standard real number), then the standard part function `Hyperreal.st` applied to `x` equals `r`. This is a formalization of the idea that the standard part of a hyperreal number is the real number that is closest to it while remaining within any infinitesimal distance.
More concisely: For any hyperreal number `x` and its standard part `r`, `Hyperreal.st x = r`.
|
Hyperreal.infiniteNeg_add_not_infinitePos
theorem Hyperreal.infiniteNeg_add_not_infinitePos :
∀ {x y : ℝ*}, x.InfiniteNeg → ¬y.InfinitePos → (x + y).InfiniteNeg
This theorem states that for any pair of hyperreal numbers `x` and `y`, if `x` is negative infinite (meaning that it is smaller than any real number) and `y` is not positive infinite (meaning it's not the case that `y` is larger than any real number), then the sum of `x` and `y` is also negative infinite. In other words, adding a non-positive-infinite hyperreal number to a negative-infinite hyperreal number still results in a negative-infinite hyperreal number.
More concisely: For any hyperreal numbers `x` and `y`, if `x` is negative infinite and `y` is not positive infinite, then `x + y` is negative infinite.
|
Hyperreal.infinitesimal_neg
theorem Hyperreal.infinitesimal_neg : ∀ {x : ℝ*}, (-x).Infinitesimal ↔ x.Infinitesimal
The theorem `Hyperreal.infinitesimal_neg` states that for any hyperreal number 'x', 'x' is infinitesimal if and only if '-x' is infinitesimal. In other words, a hyperreal number is infinitesimal if its negation is also infinitesimal, and if a hyperreal number is infinitesimal, then its negation must also be infinitesimal. This mirrors the concept in mathematics where a real number is close to zero if and only if its negation is close to zero.
More concisely: For any hyperreal number x, x is infinitesimal if and only if -x is infinitesimal.
|
Hyperreal.infinitePos_iff_infinitesimal_inv_pos
theorem Hyperreal.infinitePos_iff_infinitesimal_inv_pos : ∀ {x : ℝ*}, x.InfinitePos ↔ x⁻¹.Infinitesimal ∧ 0 < x⁻¹ := by
sorry
This theorem states that for any hyperreal number 'x', 'x' is infinitely positive if and only if the inverse of 'x' is infinitesimal and is greater than zero. In simpler terms, a hyperreal number is larger than all real numbers if only its reciprocal is infinitesimally small (closer to zero) and is positive.
More concisely: A hyperreal number is infinitely positive if and only if its reciprocal is an infinitesimal and is positive.
|
Hyperreal.isSt_st'
theorem Hyperreal.isSt_st' : ∀ {x : ℝ*}, ¬x.Infinite → x.IsSt x.st
The theorem `Hyperreal.isSt_st'` asserts that for every hyperreal number `x` which is not infinite, the real number `Hyperreal.st x` returned by the standard part function `Hyperreal.st` satisfies the standard part predicate with respect to `x`. In other words, given any real number `δ` greater than zero, `x` lies strictly between `Hyperreal.st x` minus `δ` and `Hyperreal.st x` plus `δ`. This essentially states that `Hyperreal.st x` is the best real number approximation of the hyperreal number `x` within any given positive precision `δ`.
More concisely: For every non-infinite hyperreal number x, the real number Hyperreal.st x is a real number approximation of x such that x lies between Hyperreal.st x - δ and Hyperreal.st x + δ for any positive real number δ.
|
Hyperreal.IsSt.unique
theorem Hyperreal.IsSt.unique : ∀ {x : ℝ*} {r s : ℝ}, x.IsSt r → x.IsSt s → r = s
The theorem `Hyperreal.IsSt.unique` states that for any hyperreal number `x` and any two real numbers `r` and `s`, if `r` and `s` both satisfy the condition of being the standard part (the real part) of `x`, then `r` and `s` must be equal. In other words, the standard part of a hyperreal number is unique.
More concisely: The standard part of a hyperreal number is unique. That is, for all hyperreal numbers x and real numbers r and s, if r and s are the standard parts of x, then r = s.
|
Hyperreal.coe_lt_coe
theorem Hyperreal.coe_lt_coe : ∀ {x y : ℝ}, ↑x < ↑y ↔ x < y
This theorem states that for every pair of real numbers `x` and `y`, the proposition that the hyperreal representation of `x` is less than the hyperreal representation of `y` is equivalent to the proposition that `x` is less than `y`. In other words, the ordering of real numbers is preserved when they are embedded into the hyperreal numbers.
More concisely: The hyperreal representation of real number `x` is less than the hyperreal representation of real number `y` if and only if `x` is less than `y`.
|
Hyperreal.infinitePos_add_not_infiniteNeg
theorem Hyperreal.infinitePos_add_not_infiniteNeg :
∀ {x y : ℝ*}, x.InfinitePos → ¬y.InfiniteNeg → (x + y).InfinitePos
This theorem states that for any two hyperreal numbers `x` and `y`, if `x` is positively infinite (meaning it is greater than all real numbers) and `y` is not negatively infinite (meaning there exists some real number `r` such that `y` is not less than `r`), then the sum of `x` and `y` is also positively infinite (it's greater than all real numbers).
More concisely: If `x` is a positively infinite hyperreal number and `y` is not negatively infinite, then `x + y` is positively infinite.
|
Hyperreal.Infinite.not_infinitesimal
theorem Hyperreal.Infinite.not_infinitesimal : ∀ {x : ℝ*}, x.Infinite → ¬x.Infinitesimal
The theorem `Hyperreal.Infinite.not_infinitesimal` states that for any hyperreal number `x`, if `x` is infinite (either infinitely positive or infinitely negative), then `x` cannot be infinitesimal. In other words, a hyperreal number cannot be both infinite and have a standard part of 0.
More concisely: A hyperreal number is not infinitesimal if it is infinite.
|
Hyperreal.infinitePos_neg
theorem Hyperreal.infinitePos_neg : ∀ {x : ℝ*}, (-x).InfinitePos ↔ x.InfiniteNeg
The theorem `Hyperreal.infinitePos_neg` states that for any hyperreal number `x`, `-x` is positively infinite if and only if `x` is negatively infinite. In other words, a hyperreal number `x` is negatively infinite (meaning it is less than all real numbers) if its negation `-x` is positively infinite (meaning `-x` is greater than all real numbers), and vice versa.
More concisely: For any hyperreal number `x`, `-x` is positively infinite if and only if `x` is negatively infinite.
|
Hyperreal.IsSt.mul
theorem Hyperreal.IsSt.mul : ∀ {x y : ℝ*} {r s : ℝ}, x.IsSt r → y.IsSt s → (x * y).IsSt (r * s)
The theorem `Hyperreal.IsSt.mul` states that for all hyperreal numbers `x` and `y` and for all real numbers `r` and `s`, if `x` is infinitesimally close to `r` and `y` is infinitesimally close to `s` (i.e., `Hyperreal.IsSt x r` and `Hyperreal.IsSt y s`), then the product of `x` and `y` is infinitesimally close to the product of `r` and `s` (i.e., `Hyperreal.IsSt (x * y) (r * s)`).
In other words, this theorem states that the concept of being infinitesimally close is preserved under multiplication in the hyperreal numbers. It is essentially a formalization of the intuition that the product of two numbers close to two other numbers should be close to the product of those two other numbers.
More concisely: The theorem `Hyperreal.IsSt.mul` asserts that the product of two infinitesimally close hyperreal numbers is infinitesimally close to the product of their real approximations.
|
Hyperreal.infinitePos_mul_of_infinitePos_not_infinitesimal_pos
theorem Hyperreal.infinitePos_mul_of_infinitePos_not_infinitesimal_pos :
∀ {x y : ℝ*}, x.InfinitePos → ¬y.Infinitesimal → 0 < y → (x * y).InfinitePos
The theorem `Hyperreal.infinitePos_mul_of_infinitePos_not_infinitesimal_pos` states that for any two hyperreal numbers `x` and `y`, if `x` is positively infinite (meaning it is larger than all real numbers), and `y` is not infinitesimal (meaning its standard part is not zero) and `y` is greater than zero, then the product `x * y` is also positively infinite.
More concisely: If `x` is positively infinite and `y` is a non-infinitesimal positive hyperreal number, then `x * y` is also positively infinite.
|
Hyperreal.isSt_real_iff_eq
theorem Hyperreal.isSt_real_iff_eq : ∀ {r s : ℝ}, (↑r).IsSt s ↔ r = s
The theorem `Hyperreal.isSt_real_iff_eq` establishes an equivalence between two conditions for any two real numbers `r` and `s`. The first condition is that `s` is the standard part of the hyperreal number `r` (denoted as `Hyperreal.IsSt (↑r) s` in Lean 4, where `Hyperreal.IsSt` is a function that takes a hyperreal number and a real number and returns true if the real number is within any infinitesimal distance of the hyperreal number). The second condition is that `r` and `s` are equal. In other words, for any two real numbers, `s` is the standard part of the hyperreal number `r` if and only if `r` is equal to `s`.
More concisely: For any real numbers r and s, r is the hyperreal extension of s if and only if r equals s.
|