summable_pow_mul_cexp — Mathlib

English

For given integers and complex exponentials, a certain power-weighted exponential sum is summable uniformly on a local neighborhood in the upper half-plane.

Русский

Для заданных целых чисел и экспонент, сумма вида n^k e^{2πi n z} суммируема локально в верхней полуплоскости.

LaTeX

$$Summable fun c ↦ c^k * exp(2π i e z)^c$$

Lean4

theorem summable_pow_mul_cexp (k : ℕ) (e : ℕ+) (z : ℍ) :
    Summable fun c : ℕ ↦ (c : ℂ) ^ k * cexp (2 * π * I * e * z) ^ c :=
  by
  have he : 0 < (e * (z : ℂ)).im := by simpa using z.2
  apply
    ((summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp 0 k (p := 1) (f := fun n ↦ (n ^ k : ℂ)) (by norm_num)
            (by simp [← Complex.isBigO_ofReal_right, Asymptotics.isBigO_refl])).summable
        he).congr
  grind [ofReal_one, iteratedDerivWithin_zero, Pi.smul_apply, smul_eq_mul]

Похожие утверждения