Complex.IsExpCmpFilter.isLittleO_log_abs_re
theorem Complex.IsExpCmpFilter.isLittleO_log_abs_re :
∀ {l : Filter ℂ}, Complex.IsExpCmpFilter l → (fun z => (Complex.abs z).log) =o[l] Complex.re
This theorem states that for any filter `l` on the complex numbers, if `l` is an "exponential comparison filter", then the logarithm of the absolute value of `z` (`log |z|`) is little `o` of the real part of `z` (ℜz) along `l`. In other words, the logarithm of the absolute value of `z` grows slower than the real part of `z` when `l` is an exponential comparison filter. This theorem is a key step in the proof of `Complex.IsExpCmpFilter.isLittleO_cpow_exp`.
More concisely: For any filter `l` on the complex numbers, if `l` is an exponential comparison filter, then `log |z|` is little o of ℜz along `l`.
|
Complex.IsExpCmpFilter.isLittleO_exp_cpow
theorem Complex.IsExpCmpFilter.isLittleO_exp_cpow :
∀ {l : Filter ℂ},
Complex.IsExpCmpFilter l → ∀ (a : ℂ) {b : ℝ}, b < 0 → (fun z => (↑b * z).exp) =o[l] fun z => z ^ a
This theorem states that if we have a filter `l` on the complex numbers, which is an "exponential comparison filter", then for any complex number `a` and any negative real number `b`, the function that maps `z` to the exponential of `b * z` is little-o of the function that maps `z` to `z` raised to the power `a` with respect to the filter `l`. Here, little-o notation `=o[l]` represents the mathematical notation for describing limiting behavior of functions, and an "exponential comparison filter" is a specific kind of filter related to comparing exponential growth rates in complex analysis.
More concisely: For an exponential comparison filter `l` on the complex numbers, if `a` is a complex number and `b` is a negative real number, then `exp(b * z) = o[l](z ^ a)` for all complex numbers `z`.
|
Complex.IsExpCmpFilter.isLittleO_zpow_mul_exp
theorem Complex.IsExpCmpFilter.isLittleO_zpow_mul_exp :
∀ {l : Filter ℂ} {b₁ b₂ : ℝ},
Complex.IsExpCmpFilter l →
b₁ < b₂ → ∀ (m n : ℤ), (fun z => z ^ m * (↑b₁ * z).exp) =o[l] fun z => z ^ n * (↑b₂ * z).exp
In this theorem, given a filter `l` of complex numbers that satisfies the "exponential comparison filter" property, and for any two distinct real numbers `b₁` and `b₂` with `b₁` less than `b₂`, and any two integers `m` and `n`, the theorem states that the function `(fun z => z ^ m * (↑b₁ * z).exp)` is little-o of the function `(fun z => z ^ n * (↑b₂ * z).exp)` at filter `l`. Here, `little-o` is a way of comparing the growth rates of functions, and saying `f` is little-o of `g` means `f` grows at a lesser rate than `g` as their argument goes to infinity.
More concisely: Given a filter `l` of complex numbers satisfying the exponential comparison property, for any distinct real numbers `b₁ < b₂` and integers `m < n`, the function `z => z ^ m * (b₁ * z).exp` is little-o of the function `z => z ^ n * (b₂ * z).exp` as `z` approaches infinity in the filter `l`.
|
Complex.IsExpCmpFilter.isLittleO_cpow_exp
theorem Complex.IsExpCmpFilter.isLittleO_cpow_exp :
∀ {l : Filter ℂ},
Complex.IsExpCmpFilter l → ∀ (a : ℂ) {b : ℝ}, 0 < b → (fun z => z ^ a) =o[l] fun z => (↑b * z).exp
This theorem states that if we have a filter `l` on complex numbers which is an "exponential comparison filter", then for any complex number `a` and any positive real number `b`, the function `z ↦ z ^ a` (which maps `z` to `z` to the power of `a`) is little-o of the function `z ↦ exp (b * z)` (which maps `z` to the exponential of `b` times `z`) at that filter. In other words, as the values in filter `l` get larger, the growth of `z ↦ z ^ a` is dominated by the growth of `z ↦ exp (b * z)`.
More concisely: For an exponential comparison filter `l` on complex numbers, the function `z ↦ z ^ a` is little-o of `z ↦ exp (b * z)` as `z` approaches infinity in `l`.
|
Complex.IsExpCmpFilter.isLittleO_cpow_mul_exp
theorem Complex.IsExpCmpFilter.isLittleO_cpow_mul_exp :
∀ {l : Filter ℂ} {b₁ b₂ : ℝ},
Complex.IsExpCmpFilter l →
b₁ < b₂ → ∀ (a₁ a₂ : ℂ), (fun z => z ^ a₁ * (↑b₁ * z).exp) =o[l] fun z => z ^ a₂ * (↑b₂ * z).exp
The theorem `Complex.IsExpCmpFilter.isLittleO_cpow_mul_exp` states that if `l` is an exponential comparison filter, for any two complex numbers `a₁` and `a₂`, and any two real numbers `b₁` and `b₂` where `b₁ < b₂`, the function `z ↦ z ^ a₁ * exp(b₁ * z)` is little o of the function `z ↦ z ^ a₂ * exp(b₂ * z)` at the filter `l`. In other words, the growth rate of the first function is significantly smaller than the second one as `z` goes to the limit of the filter `l`.
More concisely: For an exponential comparison filter `l`, if complex numbers `a₁` and `a₂` and real numbers `b₁` and `b₂` satisfy `b₁ < b₂`, then `z ^ a₁ * exp(b₁ * z) = o(z ^ a₂ * exp(b₂ * z))` as `z` approaches the limit of `l`.
|
Complex.IsExpCmpFilter.isLittleO_pow_mul_exp
theorem Complex.IsExpCmpFilter.isLittleO_pow_mul_exp :
∀ {l : Filter ℂ} {b₁ b₂ : ℝ},
Complex.IsExpCmpFilter l →
b₁ < b₂ → ∀ (m n : ℕ), (fun z => z ^ m * (↑b₁ * z).exp) =o[l] fun z => z ^ n * (↑b₂ * z).exp
This theorem in Lean 4 states that, given a complex filter `l` that is an "exponential comparison filter", for any complex numbers `m` and `n`, and any real numbers `b₁` and `b₂` where `b₁` is less than `b₂`, the function `(fun z => z ^ m * (exp (b₁ * z)))` is little-o of the function `(fun z => z ^ n * (exp (b₂ * z)))` with respect to the filter `l`. In other words, as complex numbers `z` drawn from the filter `l` get large, the rate of growth of `z ^ m * (exp (b₁ * z))` is significantly smaller than the rate of growth of `z ^ n * (exp (b₂ * z))`.
More concisely: For any exponential comparison filter `l`, the function `z => z ^ m * exp(b₁*z)` is little-o of the function `z => z ^ n * exp(b₂*z)` as `z` approaches infinity in the filter `l`, where `m` and `n` are complex numbers and `b₁` is strictly less than `b₂`.
|