OAI/NumberTheory/Ostmann/Preliminaries/MoebiusSquareRemoval.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exact Möbius removal of the square-part coprimality condition

  1. theorem OAI.Ostmann.sum_moebius_complex line 12
  2. theorem OAI.Ostmann.coprime_moebius_sum line 21
  3. theorem OAI.Ostmann.sum_coprime_moebius line 36

    Source documentation

    This form allows the summation index to carry all the other frequency parameters while w extracts only the square part.

    theorem sum_coprime_moebius {ι : Type*} (S : Finset ι) (w : ι → ℕ) (a : ι → ℂ)
    {M : ℕ} (hM : 0 < M) :
    (∑ i ∈ S, a i * (if (w i).Coprime M then 1 else 0)) =
      ∑ P ∈ M.divisors, (ArithmeticFunction.moebius P : ℂ) *
        ∑ i ∈ S with P ∣ w i, a i := by
…
  4. theorem OAI.Ostmann.quadratic_square_removal line 51
  5. theorem OAI.Ostmann.squarefree_frequency_moebius_expansion line 59