OAI/NumberTheory/Ostmann/Characters/RepeatedCharacterCancellation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Ostmann.periodic_poisson_complete_mean line 13
2. def OAI.Ostmann.groupedSlotValue line 34
3. theorem OAI.Ostmann.groupedSlotValue_product line 39
4. theorem OAI.Ostmann.groupedSlotValue_singleton line 55
5. theorem OAI.Ostmann.grouped_singleton_fourier_zero line 66
6. theorem OAI.Ostmann.grouped_singleton_poisson_zero line 87

   Source documentation

   Once the repeated tuple's actual period is below the Fourier cutoff, one singly occurring nonprincipal character annihilates its entire sum.

   theorem grouped_singleton_poisson_zero {I : Type*} [Fintype I] (P : Finset ℕ)
       (hP : ∀ q ∈ P, q.Prime) (p : I → P)
       (χ : I → ∀ q : ℕ, DirichletCharacter ℂ q) (t : ∀ q : ℕ, ZMod q)
       (i : I) (hi : ∀ j, p j = p i → j = i) (hχ : χ i (p i) ≠ 1)
       (ψ : 𝓢(ℝ, ℂ)) (X H : ℝ) (hX : 0 < X)
       (hperiod : H < X / (∏ q : P, (q : ℕ)))
       (hsupp : ∀ x : ℝ, H < |x| → 𝓕 ψ x = 0) :
       (∑' n : ℤ, (∏ j, χ j (p j) ((n : ZMod (p j : ℕ)) - t (p j))) *
         ψ ((n : ℝ) / X)) = 0 := by
   …

7. theorem OAI.Ostmann.bounded_complete_mean_norm line 111
8. theorem OAI.Ostmann.short_period_character_sum_bound line 127