OAI/NumberTheory/CubicMoment/Angular/AngularPrimaryLattice.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Cancellation on the actual primary congruence class. The annulus has zero area, and scaled coset Poisson summation controls every length.

  1. def OAI.CubicFirstMoment.primaryAngularLattice line 13
  2. lemma OAI.CubicFirstMoment.angularPlanePhase_pos_mul line 16
  3. lemma OAI.CubicFirstMoment.angularAnnulus_scaled line 23
  4. lemma OAI.CubicFirstMoment.primary_scaled_coset line 35
  5. theorem OAI.CubicFirstMoment.primaryAngularLattice_decay line 47

    Source documentation

    A strong smooth-coset estimate, sufficient for the elementary square-divisor inversion in the angular model.

    theorem primaryAngularLattice_decay {ℓ : ℤ} (hℓ : ℓ ≠ 0)
    (W : ℝ → ℂ) (hW : HasCompactSupport W) (hpos : tsupport W ⊆ Ioi 0)
    (hsm : ContDiff ℝ ∞ W) :
    ∃ K : ℝ, 0 < K ∧ ∀ Y : ℝ, 0 < Y → ‖primaryAngularLattice ℓ W Y‖ ≤ K/Y := by
…

    Mentions: OAI.CubicFirstMoment.primaryAngularLattice

  6. theorem OAI.CubicFirstMoment.primaryAngularLattice_bounded line 73

    Source documentation

    Uniform over the length parameter, including the empty short range.

    theorem primaryAngularLattice_bounded {ℓ : ℤ} (hℓ : ℓ ≠ 0)
    (W : ℝ → ℂ) (hW : HasCompactSupport W) (hpos : tsupport W ⊆ Ioi 0)
    (hsm : ContDiff ℝ ∞ W) :
    ∃ K : ℝ, 0 < K ∧ ∀ Y : ℝ, 0 < Y → ‖primaryAngularLattice ℓ W Y‖ ≤ K := by
…

    Mentions: OAI.CubicFirstMoment.primaryAngularLattice