OAI/NumberTheory/CubicMoment/Angular/AngularSquarefreeLattice.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Low-height angular cancellation for the literal squarefree, coprime primary lattice sum.

  1. def OAI.CubicFirstMoment.squarefreeCoprimeAngularLattice line 14
  2. lemma OAI.CubicFirstMoment.coprimeAngularLattice_divisor line 19
  3. lemma OAI.CubicFirstMoment.squarefreeAngular_pointwise_inversion line 45
  4. lemma OAI.CubicFirstMoment.squarefreeAngular_summable line 69
  5. theorem OAI.CubicFirstMoment.squarefreeCoprimeAngularLattice_expansion line 82
  6. theorem OAI.CubicFirstMoment.squarefreeCoprimeAngularLattice_bound line 112

    Source documentation

    Cancellation in every fixed nonzero mode, for the literal squarefree primary sum with coprimality to the level.

    theorem squarefreeCoprimeAngularLattice_bound {ℓ : ℤ} (hℓ : ℓ ≠ 0)
    (W : ℝ → ℂ) (hW : HasCompactSupport W) (hpos : tsupport W ⊆ Ioi 0)
    (hsm : ContDiff ℝ ∞ W) {ε : ℝ} (hε : 0 < ε) :
    ∃ K : ℝ, 0 < K ∧ ∀ r : Eisenstein, primary r → Squarefree r →
      ∀ Y : ℝ, 1 ≤ Y →
        ‖squarefreeCoprimeAngularLattice r ℓ W Y‖ ≤ K*norm r^ε*Real.sqrt Y := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.squarefreeCoprimeAngularLattice, OAI.CubicFirstMoment.norm