mellin_convergent_of_isBigO_scalar
theorem mellin_convergent_of_isBigO_scalar :
∀ {a b : ℝ} {f : ℝ → ℝ} {s : ℝ},
MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
(f =O[Filter.atTop] fun x => x ^ (-a)) →
s < a →
(f =O[nhdsWithin 0 (Set.Ioi 0)] fun x => x ^ (-b)) →
b < s → MeasureTheory.IntegrableOn (fun t => t ^ (s - 1) * f t) (Set.Ioi 0) MeasureTheory.volume
The theorem `mellin_convergent_of_isBigO_scalar` states that if you have a real-valued function `f` that is locally integrable over the interval (0, ∞) and is "big O" of `x ^ (-a)` as `x` approaches infinity and "big O" of `x ^ (-b)` as `x` approaches 0, then the Mellin transform integral of `f` converges for real numbers `s` such that `b < s < a`. In the context of big O notation, `f =O[...] g` signifies that `f` is asymptotically upper bounded by `g` up to a constant factor. The Mellin transform integral is a particular kind of integral that involves a function multiplied by a power of its argument, in this case `t ^ (s - 1) * f t`, over the interval (0, ∞).
More concisely: If a locally integrable real-valued function `f` on (0, ∞) is big O of `x ^ (-a)` as `x` approaches infinity and big O of `x ^ (-b)` as `x` approaches 0, then the Mellin transform of `f`, defined as the integral of `t ^ (s - 1) * f(t) dt` over (0, ∞), converges for `s` with `b < s < a`.
|
mellin_convergent_top_of_isBigO
theorem mellin_convergent_top_of_isBigO :
∀ {f : ℝ → ℝ},
MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ioi 0)) →
∀ {a s : ℝ},
(f =O[Filter.atTop] fun x => x ^ (-a)) →
s < a →
∃ c, 0 < c ∧ MeasureTheory.IntegrableOn (fun t => t ^ (s - 1) * f t) (Set.Ioi c) MeasureTheory.volume
This theorem states that if we have a locally integrable real-valued function `f`, which is big O of `x` to the power of negative `a` as `x` tends towards infinity, then for any real number `s` that is less than `a`, the Mellin transform of `f` converges on some neighborhood of positive infinity. Here, the Mellin transform is represented by the function `t` to the power of `s - 1` multiplied by `f(t)`. The existence of such a neighborhood is indicated by the existence of a positive real number `c` such that the Mellin transform is integrable (finite integral) on the interval from `c` to infinity.
More concisely: If `f` is a locally integrable real-valued function that is big O of `x^(-a)` as `x` approaches infinity for `a > s > 0`, then the Mellin transform of `f` converges on some neighborhood of positive infinity, i.e., the integral of `t^(s-1)*f(t) dt` is finite on some interval `(c, ∞)`.
|
hasMellin_cpow_Ioc
theorem hasMellin_cpow_Ioc :
∀ (a : ℂ) {s : ℂ}, 0 < s.re + a.re → HasMellin ((Set.Ioc 0 1).indicator fun t => ↑t ^ a) s (1 / (s + a))
This theorem states that for any complex number 'a' and a complex number 's' with its real part plus the real part of 'a' greater than zero, the Mellin transform of a power function, when restricted to the interval between 0 (excluded) and 1 (included), is defined at 's' and equals to 1/(s+a). The power function is defined as t to the power of 'a' for any real number 't' inside the interval, and zero outside of this interval.
More concisely: For complex numbers 'a' and 's' with Re(s) + Re(a) > 0, the Mellin transform of the power function t^a with domain [0, 1) equals 1/(s+a).
|
mellin_convergent_iff_norm
theorem mellin_convergent_iff_norm :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℝ → E} {T : Set ℝ},
T ⊆ Set.Ioi 0 →
MeasurableSet T →
MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ioi 0)) →
∀ {s : ℂ},
MeasureTheory.IntegrableOn (fun t => ↑t ^ (s - 1) • f t) T MeasureTheory.volume ↔
MeasureTheory.IntegrableOn (fun t => t ^ (s.re - 1) * ‖f t‖) T MeasureTheory.volume
This theorem, `mellin_convergent_iff_norm`, establishes an equivalence for integrability conditions on complex vector-valued and real scalar-valued functions in the context of a Mellin transform. Specifically, for a given normed additive commutative group `E` and a normed space over the complex numbers `ℂ` with `E` as the underlying set, a function `f` from the real numbers `ℝ` to `E`, and a set `T` of real numbers that is a subset of the interval `(0, ∞)`. If `T` is measurable and the function `f` is almost everywhere strongly measurable on the interval `(0, ∞)`, then for any complex number `s`, the theorem states that the function `t ↦ t^(s-1) • f(t)` is integrable over the set `T` with respect to the Lebesgue measure if and only if the function `t ↦ t^(Re(s)-1) * ||f(t)||` is integrable over the same set `T` with respect to the Lebesgue measure. Here, `||f(t)||` represents the norm of `f(t)`, `Re(s)` is the real part of `s`, and `t^(s-1) • f(t)` denotes scalar multiplication of the function value `f(t)` by the complex number `t^(s-1)`.
More concisely: For a measurable set T of positive real numbers and an almost everywhere strongly measurable complex vector-valued function f from the reals to a normed space over the complex numbers, the Mellin transform t => t^(s-1) * f(t) is integrable over T with respect to Lebesgue measure if and only if the function t => t^(Re(s)-1) * ||f(t)|| is integrable over T with respect to Lebesgue measure.
|
mellinConvergent_of_isBigO_rpow_exp
theorem mellinConvergent_of_isBigO_rpow_exp :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b : ℝ},
0 < a →
∀ {f : ℝ → E} {s : ℂ},
MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
(f =O[Filter.atTop] fun t => (-a * t).exp) →
(f =O[nhdsWithin 0 (Set.Ioi 0)] fun x => x ^ (-b)) → b < s.re → MellinConvergent f s
This theorem states that for a function `f` from real numbers to a normed space `E`, and given two real numbers `a` and `b` where `a` is greater than 0, if `f` is locally integrable over the interval (0, +∞), decays exponentially at infinity (i.e., `f` is big O of the exponential of `-a * t` as `t` approaches infinity), and `f` is asymptotic to `x ^ (-b)` as `x` approaches 0 from the right (in other words, `f` is big O of `x ^ (-b)` in the neighborhood of 0 within the right-open interval (0, +∞)), then the Mellin transform of `f` converges for complex numbers `s` whose real part is greater than `b`.
The Mellin transform of `f` is a generalization of the Fourier transform that extends the notion of frequency analysis to include scale analysis. In this case, convergence of the Mellin transform is defined as the integrability of the function `t` to the power of `(s - 1)` times `f(t)` over the interval (0, +∞) with respect to the Lebesgue measure.
More concisely: If a real-valued function `f` on the positive real numbers is locally integrable, decays exponentially at infinity, and is asymptotic to `x ^ (-b)` as `x` approaches 0 from the right, then its Mellin transform converges for complex numbers `s` with real part greater than `b`.
|
hasMellin_one_Ioc
theorem hasMellin_one_Ioc : ∀ {s : ℂ}, 0 < s.re → HasMellin ((Set.Ioc 0 1).indicator fun x => 1) s (1 / s)
The theorem `hasMellin_one_Ioc` states that for any complex number `s` with a positive real part, the Mellin transform of the indicator function of the interval `(0, 1]` (i.e., a function that is equal to 1 on this interval and 0 outside) is defined at `s` and equals to `1/s`.
More concisely: For complex numbers `s` with positive real part, the Mellin transform of the indicator function of the interval `(0, 1]` equals `1/s`.
|
mellin_differentiableAt_of_isBigO_rpow_exp
theorem mellin_differentiableAt_of_isBigO_rpow_exp :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b : ℝ},
0 < a →
∀ {f : ℝ → E} {s : ℂ},
MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
(f =O[Filter.atTop] fun t => (-a * t).exp) →
(f =O[nhdsWithin 0 (Set.Ioi 0)] fun x => x ^ (-b)) → b < s.re → DifferentiableAt ℂ (mellin f) s
The theorem `mellin_differentiableAt_of_isBigO_rpow_exp` states that if a function `f` is locally integrable over the interval `(0, ∞)`, decays exponentially as it approaches infinity, and is of order `O(x^(-b))` near 0, then the Mellin transform of `f` is holomorphic (i.e., complex differentiable) at any complex number `s` whose real part is greater than `b`. Here, `a` is a positive real number which controls the rate of the exponential decay at infinity, and `b` is a real number that controls the rate of decay near 0. The theorem provides conditions under which we can claim the complex differentiability of the Mellin transform of a function.
More concisely: If a locally integrable function `f` over `(0, ∞)` decays exponentially at infinity and is of order `O(x^(-b))` near 0, then its Mellin transform is holomorphic for complex numbers `s` with real part greater than `b`.
|
isBigO_rpow_zero_log_smul
theorem isBigO_rpow_zero_log_smul :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E},
a < b →
(f =O[nhdsWithin 0 (Set.Ioi 0)] fun x => x ^ (-a)) →
(fun t => t.log • f t) =O[nhdsWithin 0 (Set.Ioi 0)] fun x => x ^ (-b)
The theorem `isBigO_rpow_zero_log_smul` states that if a function `f` is big O of `x` raised to the power of negative `a` as `x` approaches zero from the positive side, then the function that is the natural logarithm of `t` multiplied by `f(t)` is big O of `x` raised to the power of negative `b` as `x` approaches zero from the positive side, for every `a` less than `b`. In other words, if `f` grows at most as fast as a certain decreasing power function near zero, then the function where we multiply `f` by the log of its argument grows at most as fast as a power function with a higher exponent near zero. This gives us an idea about how fast our function grows in comparison to a power function.
More concisely: If `f(x)` is big O of `x^a` as `x` approaches 0 from the right, then `log(x) * f(x)` is big O of `x^b` for `b > a`.
|
mellin_hasDerivAt_of_isBigO_rpow
theorem mellin_hasDerivAt_of_isBigO_rpow :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b : ℝ} {f : ℝ → E} {s : ℂ},
MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
(f =O[Filter.atTop] fun x => x ^ (-a)) →
s.re < a →
(f =O[nhdsWithin 0 (Set.Ioi 0)] fun x => x ^ (-b)) →
b < s.re →
MellinConvergent (fun t => t.log • f t) s ∧ HasDerivAt (mellin f) (mellin (fun t => t.log • f t) s) s
This theorem states that given a function `f` which is locally integrable on the open interval `(0, ∞)`, behaves as `O(x ^ (-a))` as `x` tends to infinity, and as `O(x ^ (-b))` as `x` tends to 0, then its Mellin transform is differentiable on the domain where the real part of `s` lies strictly between `b` and `a`. Furthermore, the derivative is equal to the Mellin transform of the function `log • f`, where `log` is the natural logarithm and `•` denotes function multiplication.
More concisely: Given a locally integrable function `f` on `(0, ∞)` with `O(x ^ (-a))` behavior as `x` approaches infinity and `O(x ^ (-b))` behavior as `x` approaches 0, its Mellin transform is differentiable on the real `s` such that `b < s < a`, and the derivative equals the Mellin transform of `log • f`.
|
mellin_convergent_zero_of_isBigO
theorem mellin_convergent_zero_of_isBigO :
∀ {b : ℝ} {f : ℝ → ℝ},
MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ioi 0)) →
(f =O[nhdsWithin 0 (Set.Ioi 0)] fun x => x ^ (-b)) →
∀ {s : ℝ},
b < s →
∃ c, 0 < c ∧ MeasureTheory.IntegrableOn (fun t => t ^ (s - 1) * f t) (Set.Ioc 0 c) MeasureTheory.volume
The theorem `mellin_convergent_zero_of_isBigO` states that for a locally integrable real-valued function `f`, which behaves asymptotically like `O(x ^ (-b))` as `x` approaches `0` from the right, the Mellin transform of `f` will converge in some right neighbourhood of `0` for any real number `s` that is greater than `b`.
Here, `MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (Set.Ioi 0))` indicates that `f` is almost everywhere strongly measurable on the set of real numbers greater than `0`, and `(f =O[nhdsWithin 0 (Set.Ioi 0)] fun x => x ^ (-b))` signifies that `f` is asymptotically bounded above by the function `x ^ (-b)` as `x` approaches `0` from the right. The notation `MeasureTheory.IntegrableOn (fun t => t ^ (s - 1) * f t) (Set.Ioc 0 c) MeasureTheory.volume` is used to express that the function `t ^ (s - 1) * f t`, multiplied pointwise by `f` and elevated to the `s - 1` power, is integrable over the interval `(0, c]` for some positive `c`.
More concisely: If a locally integrable real-valued function `f` is almost everywhere strongly measurable and asymptotically bounded above by `x ^ (-b)` as `x` approaches `0` from the right, then its Mellin transform converges in some right neighborhood of `s = b`.
|
isBigO_rpow_top_log_smul
theorem isBigO_rpow_top_log_smul :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E},
b < a → (f =O[Filter.atTop] fun x => x ^ (-a)) → (fun t => t.log • f t) =O[Filter.atTop] fun x => x ^ (-b)
This theorem states that for any type `E` that is a normed commutative additive group and a normed space over the real numbers, and for any real numbers `a` and `b`, if a function `f` from the real numbers to `E` is Big O of `x ^ (-a)` as `x` approaches infinity (denoted `f =O[Filter.atTop] fun x => x ^ (-a)`), and if `b` is less than `a`, then the function that maps each real number `t` to the log of `t` times `f(t)` (denoted `fun t => t.log • f t`) is Big O of `x ^ (-b)` as `x` approaches infinity (denoted `(fun t => t.log • f t) =O[Filter.atTop] fun x => x ^ (-b)`). In simpler terms, if `f` grows no faster than `x ^ (-a)` as `x` goes to infinity, then the function `log(x) * f(x)` grows no faster than `x ^ (-b)` as `x` goes to infinity, for any `b` less than `a`.
More concisely: If `f : ℝ → E` is a function from the real numbers to a normed commutative additive group and normed space over the reals, such that `f = O(x ^ (-a))` as `x → ∞`, then `x → log(x) * f(x) = O(x ^ (-b))` for any `b < a`.
|
mellin_differentiableAt_of_isBigO_rpow
theorem mellin_differentiableAt_of_isBigO_rpow :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b : ℝ} {f : ℝ → E} {s : ℂ},
MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume →
(f =O[Filter.atTop] fun x => x ^ (-a)) →
s.re < a → (f =O[nhdsWithin 0 (Set.Ioi 0)] fun x => x ^ (-b)) → b < s.re → DifferentiableAt ℂ (mellin f) s
The theorem `mellin_differentiableAt_of_isBigO_rpow` states that given a locally integrable function `f` on the interval `(0, ∞)`, which behaves asymptotically as `O(x ^ (-a))` as `x` approaches infinity and `O(x ^ (-b))` as `x` approaches 0, then the Mellin transform of `f` is differentiable at a point `s` in the complex plane such that `b` is less than the real part of `s` which is less than `a`. This is to say, the Mellin transform of `f` has a derivative at such a point `s`.
More concisely: Given a locally integrable function `f` on `(0, ∞)` with asymptotic behaviors `O(x ^ (-a))` as `x` approaches infinity and `O(x ^ (-b))` as `x` approaches 0, if `b < Re(s) < a`, then the Mellin transform of `f` is differentiable at `s`.
|