OAI/NumberTheory/Ostmann/Characters/SparseCoefficientMajorant.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.sparsePatternMellin line 10
2. theorem OAI.Ostmann.sparsePatternMellin_norm_sum line 17
3. def OAI.Ostmann.sparseTruncatedMellinCoefficient line 44
4. theorem OAI.Ostmann.sparseTruncatedMellinCoefficient_norm_le line 53

   Source documentation

   The norm of each full multiplicative coefficient is at most exp(6H), independently of the truncation order and of the number of primes.

   theorem sparseTruncatedMellinCoefficient_norm_le {n : ℕ}
       (p : Fin n → ℕ) [∀ i, Fact (p i).Prime] (E : ∀ i, Finset (ZMod (p i)))
       (hE : ∀ i, 0 ∉ E i) (hsym : ∀ i b, -b ∈ E i ↔ b ∈ E i)
       (t : ℝ) (ht : 0 ≤ t) (ht1 : t ≤ 1) (hp : ∀ i, (36 : ℝ) ≤ p i)
       (K : ℕ) (χ : ∀ i, MulChar (ZMod (p i)) ℂ) :
       ‖sparseTruncatedMellinCoefficient p E t K χ‖ ≤
         Real.exp (6 * ∑ i, (p i : ℝ)⁻¹) := by
   …

   Mentions: OAI.Ostmann.sparseTruncatedMellinCoefficient