OAI/NumberTheory/CubicMoment/Estimates/ShortFactorMoments.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The actual short Möbius, zeta and logarithmic factors occurring in the finite ideal convolution identity.

  1. def OAI.CubicFirstMoment.ShortArithmeticFactor line 12
  2. lemma OAI.CubicFirstMoment.shortArithmeticFactor_norm line 15
  3. lemma OAI.CubicFirstMoment.shortArithmeticFactor_twisted_norm line 32
  4. lemma OAI.CubicFirstMoment.primaryElementBall_card_le line 40
  5. lemma OAI.CubicFirstMoment.shortArithmeticFactor_energy line 44
  6. theorem OAI.CubicFirstMoment.shortFactor_multiplicity_moment line 62

    Source documentation

    The fixed-multiplicity sharp cubic moment for the exact ideal polynomials supplied by the short Möbius identity.

    theorem shortFactor_multiplicity_moment (k : ι → ℕ)
    {ε δ : ℝ} (hε : 0 < ε) (hδ : 0 < δ) :
    ∃ C : ℝ, 0 < C ∧ ∀ (F : ℝ) (X : ι → ℝ)
      (A : ι → EisensteinArithmeticFunction) (u : ι → Eisenstein → ℂ),
      (∀ i, ShortArithmeticFactor F (A i)) → (∀ i, 1 ≤ X i) →
      (∀ i, ∀ a ∈ primaryElementBall (X i), ‖u i a‖ ≤ 1) →
      ∀ (P : Finset Eisenstein) (N : ℝ), 1 ≤ N →
      (∀ a ∈ P, primary a ∧ Squarefree a ∧ norm a ≤ N) →
      (∑ a ∈ P, ‖∏ i,
        (primaryIdealPolynomial (X i) (A i) (fun n => u i n*cubicSymbol a n))^(k i)‖^2) ≤
        C*(N*(∏ i, (X i)^(k i)))^ε*(∏ i, (X i)^(k i))*
          (N+(∏ i, (X i)^(k i))+(N*(∏ i, (X i)^(k i)))^(2/3:ℝ))*
…

    Mentions: OAI.CubicFirstMoment.EisensteinArithmeticFunction, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.ShortArithmeticFactor, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.primaryIdealPolynomial, OAI.CubicFirstMoment.cubicSymbol

  7. theorem OAI.CubicFirstMoment.shortFactor_mixed_multiplicity_moment line 89

    Source documentation

    Actual short-factor mixed moments, with all individual coefficient energies bounded explicitly. Huxley's additive sieve is the sole input.

    theorem shortFactor_mixed_multiplicity_moment
    (hHuxley : HuxleyAdditiveLargeSieve) (k : ι → ℕ)
    {ε δ : ℝ} (hε : 0 < ε) (hδ : 0 < δ) :
    ∃ C : ℝ, 0 < C ∧ ∀ (F : ℝ) (X : ι → ℝ)
      (A : ι → EisensteinArithmeticFunction) (u : ι → Eisenstein → ℂ),
      (∀ i, ShortArithmeticFactor F (A i)) → (∀ i, 1 ≤ X i) →
      (∀ i, ∀ a ∈ primaryElementBall (X i), ‖u i a‖ ≤ 1) →
      ∀ (P : Finset (Eisenstein × Eisenstein)) (Q : ℝ), 1 ≤ Q →
      (∀ p ∈ P, PrimarySquarefreePair p ∧ norm (pairConductor p) ≤ Q) →
      (∑ p ∈ P, ‖∏ i, (primaryIdealPolynomial (X i) (A i)
        (fun n => u i n*mixedCubic p.1 p.2 n))^(k i)‖^2) ≤
        C*Q^ε*(Q^2+(∏ i, (X i)^(k i)))*
…

    Mentions: OAI.CubicFirstMoment.HuxleyAdditiveLargeSieve, OAI.CubicFirstMoment.EisensteinArithmeticFunction, OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.ShortArithmeticFactor, OAI.CubicFirstMoment.primaryElementBall, OAI.CubicFirstMoment.PrimarySquarefreePair, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.pairConductor, OAI.CubicFirstMoment.primaryIdealPolynomial, OAI.CubicFirstMoment.mixedCubic