OAI/NumberTheory/CubicMoment/Angular/AngularCoprimeLattice.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Exact coprimality removal for the angular lattice model. The primary congruence class and all divisor phases remain literal.

  1. def OAI.CubicFirstMoment.primaryCoprimeAngularLattice line 15
  2. lemma OAI.CubicFirstMoment.primaryAngularLattice_eq_indicator line 18
  3. lemma OAI.CubicFirstMoment.summable_primary_angular_restricted line 27
  4. lemma OAI.CubicFirstMoment.primaryAngularLattice_divisor line 38
  5. lemma OAI.CubicFirstMoment.primaryCoprimeAngularLattice_expansion line 53
  6. theorem OAI.CubicFirstMoment.primaryCoprimeAngularLattice_bound line 95

    Source documentation

    The actual coprime angular sum is bounded by a fixed small power of the level, uniformly over its length.

    theorem primaryCoprimeAngularLattice_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 : ℝ, 0 < Y → ‖primaryCoprimeAngularLattice r ℓ W Y‖ ≤ K*norm r^ε := by
…

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