OAI/NumberTheory/Ostmann/ZeroDensity/ProgressionCharacterCancellation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.complex_periodic_blocks line 13
2. theorem OAI.Ostmann.complex_periodic_zero_sum_bound line 23
3. theorem OAI.Ostmann.sum_range_residues line 34
4. def OAI.Ostmann.characterPairValue line 46
5. theorem OAI.Ostmann.characterPairValue_nat line 50
6. theorem OAI.Ostmann.characterPairValue_sum_zero line 55
7. theorem OAI.Ostmann.characterPairValue_norm_le_one line 64
8. theorem OAI.Ostmann.character_progression_sum_bound line 72

   Source documentation

   A step coprime to the two short moduli permutes the complete period. This remains exact after fixing any residue class of the frequency modulus.

   theorem character_progression_sum_bound {q r : ℕ} [NeZero q] [NeZero r]
       (hqr : q.Coprime r) (χ : DirichletCharacter ℂ q) (ψ : DirichletCharacter ℂ r)
       (hχ : χ ≠ 1) (a M N : ℕ) (hM : M.Coprime (q * r)) :
       ‖∑ j ∈ Finset.range N, χ ((a + M * j : ℕ) : ZMod q) *
         conj (ψ ((a + M * j : ℕ) : ZMod r))‖ ≤ q * r := by
   …

9. theorem OAI.Ostmann.weighted_character_progression_bound line 103
10. theorem OAI.Ostmann.character_interval_pieces_bound line 114

    Source documentation

    Sum the exact progression bounds over all interval/residue pieces. The total variation budget includes the reciprocal-integer weight.

    theorem character_interval_pieces_bound {I : Type*} [Fintype I]
        {q r : ℕ} [NeZero q] [NeZero r] (hqr : q.Coprime r)
        (χ : DirichletCharacter ℂ q) (ψ : DirichletCharacter ℂ r) (hχ : χ ≠ 1)
        (a M N : I → ℕ) (hM : ∀ i, (M i).Coprime (q * r))
        (w : I → ℕ → ℂ) (V : ℝ) (hvar : ∑ i, discreteVariation (w i) (N i) ≤ V) :
        ‖∑ i, ∑ j ∈ Finset.range (N i), w i j *
          (χ ((a i + M i * j : ℕ) : ZMod q) * conj (ψ ((a i + M i * j : ℕ) : ZMod r)))‖ ≤
          V * (q * r) := by
    …

    Mentions: OAI.Ostmann.discreteVariation