tendsto_rpow_mul_exp_neg_mul_atTop_nhds_0
theorem tendsto_rpow_mul_exp_neg_mul_atTop_nhds_0 :
∀ (s b : ℝ), 0 < b → Filter.Tendsto (fun x => x ^ s * (-b * x).exp) Filter.atTop (nhds 0)
The theorem `tendsto_rpow_mul_exp_neg_mul_atTop_nhds_0` states that for any given real numbers `s` and `b` (with `b` being positive), the function `x^s * exp(-b * x)` approaches 0 as `x` approaches infinity. In other words, as the value of `x` continually increases, the output of this function gets closer and closer to zero. This is expressed in the context of filters, where `Filter.atTop` represents the situation where `x` is increasing without bound (i.e., going to infinity), and `Filter.Tendsto` is used to express the limit of the function.
More concisely: For any real numbers `s` and `b` (with `b` positive), the function `x => x^s * exp(-b*x)` approaches 0 as `x` approaches infinity.
|
isLittleO_exp_neg_mul_rpow_atTop
theorem isLittleO_exp_neg_mul_rpow_atTop :
∀ {a : ℝ}, 0 < a → ∀ (b : ℝ), (fun x => (-a * x).exp) =o[Filter.atTop] fun x => x ^ b
This theorem states that for any positive real number `a` and any real number `b`, the function `exp(-a * x)` is little-o of the function `x^b` as `x` approaches infinity. In mathematical notation, this is saying that `exp(-a * x) = o(x^b)` as `x → ∞`. The little-o notation represents the asymptotic behavior of functions, and `exp(-a * x) = o(x^b)` means that the function `exp(-a * x)` grows at a slower rate than the function `x^b` as `x` approaches infinity.
More concisely: As `x` approaches infinity, the function `exp(-a * x)` is asymptotically smaller than `x^b`.
|
isLittleO_rpow_exp_atTop
theorem isLittleO_rpow_exp_atTop : ∀ (s : ℝ), (fun x => x ^ s) =o[Filter.atTop] Real.exp
This theorem states that for any real number `s`, the function `x ^ s` (where `x` is raised to the power `s`) is dominated by the exponential function `exp x` as `x` approaches infinity. This is expressed using the little-o notation (`=o[Filter.atTop]`), which means that the growth rate of `x ^ s` is significantly slower than the growth rate of `exp x` when `x` becomes extremely large. This property holds for any real number `s`.
More concisely: For any real number `s`, the function `x ^ s` is asymptotically dominated by `exp x` (i.e., `x ^ s = o(exp x)`) as `x` approaches infinity.
|
tendsto_rpow_div_mul_add
theorem tendsto_rpow_div_mul_add :
∀ (a b c : ℝ), 0 ≠ b → Filter.Tendsto (fun x => x ^ (a / (b * x + c))) Filter.atTop (nhds 1)
The theorem `tendsto_rpow_div_mul_add` states that given any real numbers `a`, `b`, and `c`, with `b` not being zero, the function `x ^ (a / (b * x + c))` will approach `1` as `x` goes to positive infinity. Here, "approach" means that for any neighborhood of `1`, there is a threshold beyond which all function values lie within this neighborhood. This is a mathematical way to capture the idea of a limit.
More concisely: For any real numbers `a`, `b` not equal to zero, and `c`, the function `x => x ^ (a / (b * x + c))` approaches `1` as `x` goes to positive infinity.
|
tendsto_rpow_neg_div
theorem tendsto_rpow_neg_div : Filter.Tendsto (fun x => x ^ (-1 / x)) Filter.atTop (nhds 1)
The theorem `tendsto_rpow_neg_div` states that the function `x ^ (-1 / x)` converges to `1` as `x` approaches positive infinity. In more formal terms, as `x` grows without bound, the values of the function `x ^ (-1 / x)` get arbitrarily close to `1`, in a topological sense.
More concisely: As `x` approaches positive infinity, `x ^ (-1/x)` converges to 1.
|
tendsto_exp_div_rpow_atTop
theorem tendsto_exp_div_rpow_atTop : ∀ (s : ℝ), Filter.Tendsto (fun x => x.exp / x ^ s) Filter.atTop Filter.atTop := by
sorry
This theorem states that for any real number `s`, the function `exp(x) / x ^ s` tends to positive infinity as `x` approaches positive infinity. In other words, as `x` gets larger and larger, the value of `exp(x) / x ^ s` also gets larger without bound, regardless of the specific value of `s`.
More concisely: For any real number `s`, the limit of `exp(x) / (x ^ s)` as `x` approaches positive infinity is positive infinity.
|
isLittleO_zpow_exp_pos_mul_atTop
theorem isLittleO_zpow_exp_pos_mul_atTop :
∀ (k : ℤ) {b : ℝ}, 0 < b → (fun x => x ^ k) =o[Filter.atTop] fun x => (b * x).exp
This theorem states that for any integer `k` and any positive real number `b`, the function `x` raised to the power `k` is dominated by the function `exp(b * x)` as `x` approaches infinity. In mathematical terms, it is saying that `x^k = o(exp(bx))` as `x → ∞`. This means that the growth rate of `x^k` is strictly less than that of `exp(bx)` when `x` tends towards infinity.
More concisely: For any integer `k` and positive real number `b`, `x^k = o(exp(bx))` as `x → ∞`, or equivalently, `exp(bx) > x^k` for sufficiently large `x`.
|
tendsto_rpow_div
theorem tendsto_rpow_div : Filter.Tendsto (fun x => x ^ (1 / x)) Filter.atTop (nhds 1)
This theorem states that the function `x ^ (1 / x)` converges to `1` as `x` approaches positive infinity. In other words, for any neighborhood around `1`, there exists a threshold value such that when `x` is greater than this threshold, the value of `x ^ (1 / x)` will lie within this neighborhood. This is a way of expressing the mathematical concept of a limit: the limit of `x ^ (1 / x)` as `x` goes to `+∞` is `1`.
More concisely: The limit of `x ^ (1/x)` as `x` approaches positive infinity is equal to 1.
|
isLittleO_pow_exp_pos_mul_atTop
theorem isLittleO_pow_exp_pos_mul_atTop :
∀ (k : ℕ) {b : ℝ}, 0 < b → (fun x => x ^ k) =o[Filter.atTop] fun x => (b * x).exp
The theorem `isLittleO_pow_exp_pos_mul_atTop` states that for any natural number `k` and any positive real number `b`, the function `x^k` is little-o of `exp(bx)` as `x` approaches infinity. In other words, the rate of growth of the function `x^k` is significantly smaller than that of the function `exp(bx)` when `x` becomes arbitrarily large.
More concisely: For any natural number $k$ and positive real number $b$, $x^k = o(e^{bx})$ as $x \to \infty$.
|
tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero
theorem tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero :
∀ (s b : ℝ), 0 < b → Filter.Tendsto (fun x => x ^ s * (-b * x).exp) Filter.atTop (nhds 0)
This theorem states that for any real numbers `s` and `b` with `b` being positive, the function `x ^ s * exp (-b * x)` converges to `0` as `x` approaches infinity. In other words, if you take any positive `b` and any `s`, and you look at the behavior of the function `x ^ s * exp (-b * x)` as `x` gets larger and larger, this function will get closer and closer to `0`.
More concisely: For any real numbers `s` and `b` with `b` positive, the limit of `x => x^s * exp(-b*x)` as `x` approaches infinity is zero.
|
tendsto_rpow_neg_atTop
theorem tendsto_rpow_neg_atTop : ∀ {y : ℝ}, 0 < y → Filter.Tendsto (fun x => x ^ (-y)) Filter.atTop (nhds 0)
This theorem asserts that for any positive real number `y`, the function `x ^ (-y)` tends to `0` as `x` approaches positive infinity. In mathematical terms, it says that the limit as `x` tends to `+∞` of `x^(-y)` is `0` for any `y` greater than `0`. This describes how the function behaves at very large values of `x`: as `x` gets larger and larger, `x^(-y)` gets closer and closer to zero, regardless of what positive real value `y` takes.
More concisely: For any positive real number `y`, the limit as `x` approaches positive infinity of `x^(-y)` is `0`.
|
tendsto_rpow_atTop
theorem tendsto_rpow_atTop : ∀ {y : ℝ}, 0 < y → Filter.Tendsto (fun x => x ^ y) Filter.atTop Filter.atTop
The theorem `tendsto_rpow_atTop` states that for any given positive real number `y`, the function `x ^ y` tends to positive infinity as `x` tends to positive infinity. In other words, as `x` gets larger and larger without bound, so does the value of `x ^ y` when `y` is a positive real number. This is expressed in the context of filters, where `Filter.Tendsto` is a generic limit of a function predicate, and `Filter.atTop` represents the limit towards positive infinity.
More concisely: For any positive real number `y`, the function `x ^ y` tends to positive infinity as `x` approaches positive infinity.
|
isLittleO_rpow_exp_pos_mul_atTop
theorem isLittleO_rpow_exp_pos_mul_atTop :
∀ (s : ℝ) {b : ℝ}, 0 < b → (fun x => x ^ s) =o[Filter.atTop] fun x => (b * x).exp
The theorem `isLittleO_rpow_exp_pos_mul_atTop` states that for any real number `s` and any positive real number `b`, the function `f(x) = x^s` is little-o of the function `g(x) = exp(b * x)` as `x` approaches infinity. In more mathematical terms, as `x` approaches infinity, the rate of growth of `x^s` is significantly smaller than the rate of growth of `exp(b * x)`.
More concisely: For any real number `s` and positive real number `b`, as `x` approaches infinity, `x^s = o(exp(b*x))`.
|
tendsto_exp_mul_div_rpow_atTop
theorem tendsto_exp_mul_div_rpow_atTop :
∀ (s b : ℝ), 0 < b → Filter.Tendsto (fun x => (b * x).exp / x ^ s) Filter.atTop Filter.atTop
The theorem `tendsto_exp_mul_div_rpow_atTop` states that for any real numbers `s` and `b` where `b > 0`, the function `(exp (b * x) / x^s)` tends to positive infinity as `x` tends to positive infinity. In mathematical notation, this can be expressed as: for all real numbers `s` and `b > 0`, the limit as `x` approaches positive infinity of `(exp(b*x) / x^s)` is positive infinity.
More concisely: For any real numbers `s` and `b > 0`, the limit as `x -> +∞` of `(exp(b*x) / x^s)` is +∞.
|