OAI/NumberTheory/Ostmann/QuadraticCenter/SquarefreeFrequencyRectangle.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.squarefreeKernelSupport line 11
2. theorem OAI.Ostmann.mem_squarefreeKernelSupport line 14
3. theorem OAI.Ostmann.frequencyTriples_rectangle line 19
4. theorem OAI.Ostmann.sum_frequencyTriples_rectangle line 38
5. theorem OAI.Ostmann.rectangular_frequency_moebius_expansion line 56

   Source documentation

   Inclusion-exclusion and unique squarefree decomposition give the three nested sums defining C_s^(P), with a common finite support.

   theorem rectangular_frequency_moebius_expansion (L N : ℕ) (hL : Squarefree L)
       {M : ℕ} (hM : 0 < M) (χ : DirichletCharacter ℂ M) (hχ : χ.IsQuadratic)
       (F : ℕ → ℂ) (hF : ∀ u, N < u → F u = 0) :
       (∑ u ∈ Finset.Icc 1 N, χ (u : ZMod M) * F u) =
         ∑ P ∈ M.divisors, (ArithmeticFunction.moebius P : ℂ) *
           ∑ s ∈ squarefreeKernelSupport L N, χ (s : ZMod M) *
             ∑ v ∈ L.divisors, χ (v : ZMod M) *
               ∑ w ∈ (Finset.Icc 1 N).filter (fun w => P ∣ w), F (s * v * w ^ 2) := by
   …

   Mentions: OAI.Ostmann.squarefreeKernelSupport