Real.tendsto_exp_atTop
theorem Real.tendsto_exp_atTop : Filter.Tendsto Real.exp Filter.atTop Filter.atTop
This theorem states that the real exponential function tends towards positive infinity as its variable tends towards positive infinity. In other words, as we input larger and larger real numbers into the exponential function, the output of the function also grows without bound. In terms of filters, this is formally represented by stating that the map of the exponential function over the filter representing all large real numbers is contained within that same filter, indicating the function's growth towards positive infinity.
More concisely: The real exponential function, when applied to the filter of all positive real numbers, is contained in the filter of all positive numbers tending to infinity.
|
Real.continuous_exp
theorem Real.continuous_exp : Continuous Real.exp
This theorem states that the real exponential function is continuous. In mathematical terms, it asserts that for every real number 'x', for any arbitrarily small positive number 'ε', there exists a positive number 'δ' such that for all real numbers 'y' within 'δ' distance from 'x', the absolute difference between the exponential of 'x' and the exponential of 'y' is less than 'ε'. This is a property of the real exponential function and is fundamental in analysis and calculus.
More concisely: The real exponential function is continuous, i.e., for every real number x and any ε > 0, there exists δ > 0 such that |e^x - e^y| < ε for all y within δ distance from x.
|
Real.tendsto_pow_mul_exp_neg_atTop_nhds_0
theorem Real.tendsto_pow_mul_exp_neg_atTop_nhds_0 :
∀ (n : ℕ), Filter.Tendsto (fun x => x ^ n * (-x).exp) Filter.atTop (nhds 0)
This theorem, named `Real.tendsto_pow_mul_exp_neg_atTop_nhds_0`, states that for any natural number `n`, the function `x^n * exp(-x)` approaches `0` as `x` approaches infinity. Here, `Filter.Tendsto` denotes the limit of a function, `Filter.atTop` denotes the limit going to infinity, and `nhds 0` represents a neighborhood around `0`. Therefore, in simpler terms, as the input `x` gets larger and larger (approaches infinity), the output of the function `x^n * exp(-x)` gets arbitrarily close to zero.
More concisely: For any natural number `n`, the function `x => x^n * exp(-x)` approaches `0` as `x` approaches infinity.
|
Real.isBigO_one_exp_comp
theorem Real.isBigO_one_exp_comp :
∀ {α : Type u_1} {l : Filter α} {f : α → ℝ},
((fun x => 1) =O[l] fun x => (f x).exp) ↔ Filter.IsBoundedUnder (fun x x_1 => x ≥ x_1) l f
The theorem `Real.isBigO_one_exp_comp` states that for any type `α`, filter `l` over `α`, and function `f` from `α` to the real numbers, the function `Real.exp (f x)` is asymptotically bounded away from zero along the filter if and only if the filter `l` is bounded from below under the function `f`.
In other words, the exponential of the function `f` is of the same order of magnitude as the constant function 1 along the filter `l` if and only if there exists a lower bound for the values that `f` takes at the points determined by the filter `l`.
More concisely: The exponential function of a function `f` is asymptotically bounded away from zero along a filter `l` if and only if `f` is bounded from below along `l`.
|
Real.tendsto_exp_nhds_0_nhds_1
theorem Real.tendsto_exp_nhds_0_nhds_1 : Filter.Tendsto Real.exp (nhds 0) (nhds 1)
The theorem `Real.tendsto_exp_nhds_0_nhds_1` states that the real exponential function converges to `1` as its argument approaches `0`. In other words, for every neighborhood of `1`, there exists a neighborhood of `0` such that the exponential function maps all points from the latter into the former. This is a fundamental property of the exponential function in real analysis.
More concisely: For every neighborhood of 1 in the real numbers, there exists a neighborhood of 0 such that the exponential function maps all elements of the smaller neighborhood to elements in the larger neighborhood.
|
Complex.continuous_exp
theorem Complex.continuous_exp : Continuous Complex.exp
The theorem `Complex.continuous_exp` states that the complex exponential function is continuous. In other words, for any given complex number, any small change in the input results in a correspondingly small change in the output of the function. This is a fundamental property of the complex exponential function, which is defined via its Taylor series in Lean 4.
More concisely: The complex exponential function is a continuous mapping from the complex numbers to themselves.
|
Real.coe_comp_expOrderIso
theorem Real.coe_comp_expOrderIso : Subtype.val ∘ ⇑Real.expOrderIso = Real.exp
The theorem `Real.coe_comp_expOrderIso` asserts that the function composition of `Subtype.val` (which extracts the underlying real number of a subtype) and `Real.expOrderIso` (which is an order isomorphism between real numbers, ℝ, and the open interval (0, +∞)) equals the real exponential function (`Real.exp`). In other words, applying the exponential function to a real number, and then taking its underlying value, is the same as directly applying the real exponential function.
More concisely: The theorem `Real.coe_comp_expOrderIso` states that the function `Subtype.val ∘ Real.expOrderIso` equals `Real.exp`, where `Subtype.val` extracts the underlying real number from a subtype and `Real.expOrderIso` is an order isomorphism between `ℝ` and `(0, +∞)`. Thus, `Subtype.val (Real.expOrderIso x) = Real.exp x` for all real numbers `x`.
|
Real.tendsto_exp_neg_atTop_nhds_zero
theorem Real.tendsto_exp_neg_atTop_nhds_zero : Filter.Tendsto (fun x => (-x).exp) Filter.atTop (nhds 0)
The theorem `Real.tendsto_exp_neg_atTop_nhds_zero` states that the real exponential function of the negative of a variable tends to zero as the variable tends to positive infinity. In other words, as we take increasingly large positive values for `x`, the expression `exp(-x)` gets closer and closer to zero. The concept of "tending to" is formalized in Lean 4 as the `Filter.Tendsto` predicate, which captures the idea of a function's values getting arbitrarily close to a target value in a certain limit. Here, the limit being considered is `x -> +∞`, represented by `Filter.atTop`, and the target value is `0`.
More concisely: As x approaches positive infinity, the function exp(-x) tends to zero.
|
Real.tendsto_exp_div_pow_atTop
theorem Real.tendsto_exp_div_pow_atTop : ∀ (n : ℕ), Filter.Tendsto (fun x => x.exp / x ^ n) Filter.atTop Filter.atTop
The theorem `Real.tendsto_exp_div_pow_atTop` states that for any natural number `n`, the function `exp(x)/x^n` tends to positive infinity as `x` tends to positive infinity. In other words, as `x` gets larger and larger, the value of `exp(x)/x^n` also gets larger without bound, regardless of the value of `n`. This is a statement about the rate of growth of the exponential function relative to polynomial functions: the exponential function grows faster than any power of `x`.
More concisely: For any natural number `n`, the function `exp(x) / x^n` approaches positive infinity as `x` approaches positive infinity.
|
Real.isTheta_exp_comp_one
theorem Real.isTheta_exp_comp_one :
∀ {α : Type u_1} {l : Filter α} {f : α → ℝ},
((fun x => (f x).exp) =Θ[l] fun x => 1) ↔ Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun x => |f x|
The theorem `Real.isTheta_exp_comp_one` states that for any type `α`, any filter `l` on `α`, and any function `f` from `α` to the real numbers (ℝ), the exponential of `f(x)` (`exp(f(x))`, where `exp` is the exponential function) is asymptotically equivalent to the constant function `1` along the filter `l` if and only if the absolute value of `f(x)` (`|f(x)|`) is eventually bounded from above along this filter. In simpler terms, as `x` approaches whatever the filter `l` converges to, the growth rate of `exp(f(x))` and the constant function `1` are the same if and only if there is an upper bound to the absolute value of `f(x)`.
More concisely: The exponential function of a real-valued function is asymptotically equivalent to the constant function 1 along a filter if and only if the absolute values of the function are eventually bounded from above in the filter.
|
Real.tendsto_exp_atBot
theorem Real.tendsto_exp_atBot : Filter.Tendsto Real.exp Filter.atBot (nhds 0)
This theorem states that the real exponential function (`Real.exp`) tends to 0 as its argument tends to negative infinity. In other words, as we take the limit of the function `Real.exp` as the input goes to negative infinity (`Filter.atBot`), the output approaches 0 (`nhds 0`). This is formalized in Lean using the `Filter.Tendsto` predicate, which serves as the generic predicate for expressing the limit of a function.
More concisely: The real exponential function `Real.exp` approaches 0 as its argument approaches negative infinity.
|
Mathlib.Analysis.SpecialFunctions.Exp._auxLemma.25
theorem Mathlib.Analysis.SpecialFunctions.Exp._auxLemma.25 : 1 = Real.exp 0
This theorem states that the exponential of 0, when calculated using the real exponential function (defined as the real part of the complex exponential), is equal to 1. In mathematical notation, it is expressed as \(e^{0} = 1\).
More concisely: The real exponential function evaluates to 1 at 0, i.e., \(e^0 = 1\).
|
Real.tendsto_mul_exp_add_div_pow_atTop
theorem Real.tendsto_mul_exp_add_div_pow_atTop :
∀ (b c : ℝ) (n : ℕ), 0 < b → Filter.Tendsto (fun x => (b * x.exp + c) / x ^ n) Filter.atTop Filter.atTop
The theorem `Real.tendsto_mul_exp_add_div_pow_atTop` states that for any natural number `n` and any real numbers `b` and `c` where `b` is positive, the function `(b * exp(x) + c) / (x^n)` tends to positive infinity as `x` tends to positive infinity. In mathematical terms, this means that as x grows larger and larger, the value of the function `(b * e^x + c) / x^n` increases without bound, given that `b` is greater than zero.
More concisely: For any natural number `n` and positive real number `b`, the function `(b * exp x + c) / x^n` approaches positive infinity as `x` approaches infinity.
|
Mathlib.Analysis.SpecialFunctions.Exp._auxLemma.10
theorem Mathlib.Analysis.SpecialFunctions.Exp._auxLemma.10 :
∀ {α : Type u} {β : Type v} {γ : Type w} {f : α → β} {g : β → γ} {a : Filter α} {c : Filter γ},
Filter.Tendsto (g ∘ f) a c = Filter.Tendsto f a (Filter.comap g c)
This theorem states that for any types α, β, γ, and any functions `f : α → β` and `g : β → γ`, and any filters `a` on α and `c` on γ, the "limit of a function" predicate `Filter.Tendsto` for the composition of functions `(g ∘ f)` from `a` to `c` is equivalent to the "limit of a function" predicate `Filter.Tendsto` for `f` from `a` to the comap of `g` on `c`. This essentially means that the limit of the composition of two functions is the same as the limit of the first function composed with the limit of the second function.
More concisely: Given filters `a` on type `α`, `c` on type `γ`, and functions `f : α → β` and `g : β → γ`, the composition `g ∘ f` tends to `c` as `x` tends to `a` if and only if `f` tends to the composite map `g ∘ g^(-1)` as `x` tends to `a`, where `g^(-1)` is the inverse of `g` over its range.
|
Complex.tendsto_exp_comap_re_atTop
theorem Complex.tendsto_exp_comap_re_atTop :
Filter.Tendsto Complex.exp (Filter.comap Complex.re Filter.atTop) (Bornology.cobounded ℂ)
The theorem `Complex.tendsto_exp_comap_re_atTop` states that as the real part of a complex number tends to infinity, the absolute value of the complex exponential of that number also tends to infinity. Here, `Filter.Tendsto` is used to express the limit concept, `Complex.exp` is the complex exponential function, `Filter.comap Complex.re Filter.atTop` represents the filter of the preimages of the sets tending to infinity under the real part function, and `Bornology.cobounded ℂ` is the filter representing the sets whose complements in the complex numbers have a bounded diameter. In simpler terms, as we move towards complex numbers with very large real part, the magnitude of their exponential grows without bound.
More concisely: As the real part of a complex number approaches infinity, the absolute value of its complex exponential tends to infinity.
|
Complex.comap_exp_nhds_zero
theorem Complex.comap_exp_nhds_zero : Filter.comap Complex.exp (nhds 0) = Filter.comap Complex.re Filter.atBot := by
sorry
The theorem states that the preimage filter of the complex exponential function at the neighborhood of zero is equal to the preimage filter of the real part function at negative infinity. In other words, if we look at the set of complex numbers that get arbitrarily close to zero under the complex exponential function, this set corresponds to the set of real numbers that decrease without bound under the real part function.
More concisely: The preimages of the neighborhood of zero under complex exponential function and of negative infinity under real part function are equal.
|
Real.tendsto_exp_nhds_zero_nhds_one
theorem Real.tendsto_exp_nhds_zero_nhds_one : Filter.Tendsto Real.exp (nhds 0) (nhds 1)
The theorem `Real.tendsto_exp_nhds_zero_nhds_one` states that the real exponential function, denoted by `Real.exp`, approaches the value `1` as its input approaches `0`. In other words, for every neighborhood of `1` (in the real numbers), there exists a neighborhood of `0` such that the exponential function applied to any element in this neighborhood of `0` will produce a value within the chosen neighborhood of `1`. This is a formal way of stating that the limit of `Real.exp` as `x` approaches `0` is `1`.
More concisely: For every neighborhood of 1 in the real numbers, there exists a neighborhood of 0 such that the exponential function maps every element in the smaller neighborhood to a value within the larger neighborhood. Equivalently, the limit of the exponential function as x approaches 0 is 1.
|
Real.tendsto_div_pow_mul_exp_add_atTop
theorem Real.tendsto_div_pow_mul_exp_add_atTop :
∀ (b c : ℝ) (n : ℕ), 0 ≠ b → Filter.Tendsto (fun x => x ^ n / (b * x.exp + c)) Filter.atTop (nhds 0)
The theorem `Real.tendsto_div_pow_mul_exp_add_atTop` states that for any non-zero real number `b`, any real number `c`, and any natural number `n`, the function `(x ^ n) / (b * exp(x) + c)` tends to `0` as `x` tends to infinity. Here, `x ^ n` represents `x` raised to the power `n`, `exp(x)` is the exponential function, and `/` denotes division. Essentially, this theorem tells us that regardless of the particular values of `b`, `c`, and `n` (as long as `b` is not zero), the value of our function becomes arbitrarily close to `0` for sufficiently large `x`.
More concisely: For any non-zero real number `b` and real numbers `c` and `n`, the function `x => (x ^ n) / (b * exp(x) + c)` approaches `0` as `x` approaches infinity.
|
Real.tendsto_pow_mul_exp_neg_atTop_nhds_zero
theorem Real.tendsto_pow_mul_exp_neg_atTop_nhds_zero :
∀ (n : ℕ), Filter.Tendsto (fun x => x ^ n * (-x).exp) Filter.atTop (nhds 0)
The theorem `Real.tendsto_pow_mul_exp_neg_atTop_nhds_zero` states that, for any natural number `n`, the function `x^n * exp(-x)` tends to `0` as `x` approaches positive infinity. In other words, as we take larger and larger values of `x`, the value of the function `x^n * exp(-x)` becomes increasingly close to `0`. This is a statement about the behavior of the function at the limit, and does not imply that the function exactly equals `0` for large `x`.
More concisely: For any natural number `n`, the function `x => x^n * exp(-x)` approaches `0` as `x` approaches infinity.
|
Real.isBigO_exp_comp_one
theorem Real.isBigO_exp_comp_one :
∀ {α : Type u_1} {l : Filter α} {f : α → ℝ},
((fun x => (f x).exp) =O[l] fun x => 1) ↔ Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l f
The theorem `Real.isBigO_exp_comp_one` states that for any type `α`, any filter `l` on `α`, and any function `f` from `α` to the real numbers, the exponential of `f` is asymptotically bounded by 1 along the filter `l` if and only if the filter `l` is bounded from below under the function `f`. In other words, the exponential of the function `f` doesn't go to zero faster than a constant speed, if and only if there is some lower limit to the values of `f` as seen along the filter `l`.
More concisely: For any type `α`, filter `l` on `α`, and function `f` from `α` to the real numbers, `exp (f)` is O(1) along `l` if and only if there exists a constant `C` such that `l.below_filter (f ∘ l.cover) C`.
|
Complex.tendsto_exp_comap_re_atBot
theorem Complex.tendsto_exp_comap_re_atBot :
Filter.Tendsto Complex.exp (Filter.comap Complex.re Filter.atBot) (nhds 0)
This theorem states that the complex exponential function tends to 0 as the real part of the complex number tends to negative infinity. In more mathematical terms, for every neighborhood of 0, there is a set of real numbers such that when the real part of a complex number is less than any number from this set, the image of this complex number under the complex exponential function is within the neighborhood of 0. This is a manifestation of the fact that the magnitude of the complex exponential function decreases without bound as the real part of its input goes to negative infinity.
More concisely: For every neighborhood of 0 in the complex plane, there exists a real number such that the complex exponential function evaluates to a complex number within that neighborhood for all complex numbers with real part less than that number.
|
Real.tendsto_exp_neg_atTop_nhds_0
theorem Real.tendsto_exp_neg_atTop_nhds_0 : Filter.Tendsto (fun x => (-x).exp) Filter.atTop (nhds 0)
The theorem `Real.tendsto_exp_neg_atTop_nhds_0` asserts that the real exponential function of the negative of a variable `x` (`exp(-x)`) converges to `0` as `x` approaches positive infinity. In other words, as `x` goes to `+∞`, the value of `exp(-x)` comes arbitrarily close to `0`. This implies that the larger the value of `x`, the closer `exp(-x)` is to `0`. It is also equivalent to saying that the real exponential function tends to `0` at `-∞`.
More concisely: The real exponential function `exp(-x)` approaches 0 as `x` approaches positive infinity.
|