OAI/NumberTheory/TwoPointCorrelations/MRTPrimeProducts.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The factorial multiplicity of a product of primes. Sorting gives an injective permutation code on each product fiber, including tuples with repeated primes. This is the arithmetic input for high moments of prime Dirichlet polynomials.

  1. lemma OAI.TwoPointCorrelations.mrt_prime_tuples_perm line 20

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPrimeProducts.lean:20 (same declaration text).

  2. lemma OAI.TwoPointCorrelations.mrt_prime_tuples_sorted_eq line 34

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPrimeProducts.lean:34 (same declaration text).

  3. theorem OAI.TwoPointCorrelations.mrt_prime_product_fiber_card line 44

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPrimeProducts.lean:44 (same declaration text).

  4. lemma OAI.TwoPointCorrelations.mrt_norm_sum_sq_le_card line 61

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPrimeProducts.lean:61 (same declaration text).

  5. theorem OAI.TwoPointCorrelations.mrt_prime_product_coefficient_sq line 71

    Source documentation

    Equal products of r primes contribute at most the factorial loss to the square of a grouped Dirichlet coefficient.

    Also declared: OAI/NumberTheory/TwoPoint/ShortIntervals/MRTPrimeProducts.lean:71 (same declaration text).

    theorem mrt_prime_product_coefficient_sq {r : ℕ} (S : Finset (Fin r → ℕ))
    (hS : ∀ v ∈ S, ∀ i, (v i).Prime) (a : (Fin r → ℕ) → ℂ) (n : ℕ) :
    ‖∑ v ∈ S.filter (fun v => (∏ i, v i) = n), a v‖ ^ 2 ≤
      (r.factorial : ℝ) * ∑ v ∈ S.filter (fun v => (∏ i, v i) = n), ‖a v‖ ^ 2 := by
…