Bounding Functions with Polynomially-Growing Fourier Coefficients

This file proves Lemma 7.4 of the blueprint: an upper bound on the ratio between a function whose Fourier coefficients grow polynomially and its discriminant.

noncomputable def MagicFunction.PolyFourierCoeffBound.fouterm (coeff : ℤ → ℂ) (x : ℂ) (i : ℤ) : ℂ

Equations

• MagicFunction.PolyFourierCoeffBound.fouterm coeff x i = coeff i * Complex.exp (↑Real.pi * Complex.I * ↑i * x)

noncomputable def MagicFunction.PolyFourierCoeffBound.DivDiscBound (c : ℤ → ℂ) (n₀ : ℤ) : ℝ

Equations

• MagicFunction.PolyFourierCoeffBound.DivDiscBound c n₀ = (∑' (n : ℕ), ‖c (↑n + n₀)‖ * Real.exp (-Real.pi * ↑n / 2)) / ∏' (n : ℕ+), (1 - Real.exp (-Real.pi * ↑↑n)) ^ 24

theorem MagicFunction.PolyFourierCoeffBound.hpoly' (c : ℤ → ℂ) (n₀ : ℤ) (k : ℕ) (hpoly : c =O[Filter.atTop] fun (n : ℤ) => ↑n ^ k) : (fun (n : ℕ) => c (↑n + n₀)) =O[Filter.atTop] fun (n : ℕ) => ↑n ^ k

theorem MagicFunction.PolyFourierCoeffBound.aux_5 (z : UpperHalfPlane) : ‖∏' (n : ℕ+), (1 - Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)) ^ 24‖ = ∏' (n : ℕ+), ‖1 - Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)‖ ^ 24

theorem MagicFunction.PolyFourierCoeffBound.aux_6 (z : UpperHalfPlane) : 0 ≤ ∏' (n : ℕ+), ‖1 - Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)‖ ^ 24

theorem MagicFunction.PolyFourierCoeffBound.aux_7 (z : UpperHalfPlane) (a : ℤ) : ‖Complex.exp (↑Real.pi * Complex.I * ↑a * ↑z)‖ ≤ Real.exp (-Real.pi * ↑a * z.im)

theorem MagicFunction.PolyFourierCoeffBound.aux_8 (z : UpperHalfPlane) : 0 < ∏' (n : ℕ+), (1 - Real.exp (-2 * Real.pi * ↑↑n * z.im)) ^ 24

theorem MagicFunction.PolyFourierCoeffBound.aux_ring (z : UpperHalfPlane) (i : ℕ) : Complex.I * ↑Real.pi * ↑i * ↑z = Complex.I * (↑Real.pi * ↑i * ↑z)

theorem MagicFunction.PolyFourierCoeffBound.aux_9 (z : UpperHalfPlane) (c : ℤ → ℂ) (n₀ : ℤ) (i : ℕ) : ‖c (↑i + n₀) * Complex.exp (↑Real.pi * Complex.I * ↑i * ↑z)‖ = ‖c (↑i + n₀)‖ * Real.exp (-Real.pi * ↑i * z.im)

theorem MagicFunction.PolyFourierCoeffBound.aux_10 (z : UpperHalfPlane) (c : ℤ → ℂ) (n₀ : ℤ) (hcsum : Summable fun (i : ℕ) => fouterm c (↑z) (↑i + n₀)) : Summable fun (n : ℕ) => ‖c (↑n + n₀)‖ * Real.exp (-Real.pi * ↑n * z.im)

theorem MagicFunction.PolyFourierCoeffBound.aux_11 : 0 < ∏' (n : ℕ+), (1 - Real.exp (-Real.pi * ↑↑n)) ^ 24

theorem MagicFunction.PolyFourierCoeffBound.aux_misc (x : UpperHalfPlane) : ‖Complex.exp (Complex.I * ↑x)‖ ≤ Real.exp x.im

theorem MagicFunction.PolyFourierCoeffBound.DivDiscBoundOfPolyFourierCoeff (z : UpperHalfPlane) (hz : 1 / 2 < z.im) (c : ℤ → ℂ) (n₀ : ℤ) (hcsum : Summable fun (i : ℕ) => fouterm c (↑z) (↑i + n₀)) (k : ℕ) (hpoly : c =O[Filter.atTop] fun (n : ℤ) => ↑n ^ k) (f : UpperHalfPlane → ℂ) (hf : ∀ (x : UpperHalfPlane), f x = ∑' (n : ℕ), fouterm c (↑x) (↑n + n₀)) : ‖f z / Δ z‖ ≤ DivDiscBound c n₀ * Real.exp (-Real.pi * (↑n₀ - 2) * z.im)

theorem MagicFunction.PolyFourierCoeffBound.DivDiscBound_pos (c : ℤ → ℂ) (n₀ : ℤ) (hcn₀ : c n₀ ≠ 0) (k : ℕ) (hpoly : c =O[Filter.atTop] fun (n : ℤ) => ↑n ^ k) : 0 < DivDiscBound c n₀

theorem MagicFunction.PolyFourierCoeffBound.ArithmeticFunction.sigma_asymptotic (k : ℕ) : (fun (n : ℕ) => ↑((ArithmeticFunction.sigma k) n)) =O[Filter.atTop] fun (n : ℕ) => ↑n ^ (k + 1)

theorem MagicFunction.PolyFourierCoeffBound.ArithmeticFunction.sigma_asymptotic' (k : ℕ) : (fun (n : ℕ) => ↑((ArithmeticFunction.sigma k) n)) =O[Filter.atTop] fun (n : ℕ) => ↑n ^ (k + 1)

theorem MagicFunction.PolyFourierCoeffBound.norm_φ₀_le : ∃ C₀ > 0, ∀ (z : UpperHalfPlane), 1 / 2 < z.im → ‖φ₀ z‖ ≤ C₀ * Real.exp (-2 * Real.pi * z.im)