OAI/NumberTheory/CubicMoment/Angular/AngularUniformLattice.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform fixed-angular cancellation on the actual primary, coprime, squarefree lattice. Constants precede every weight and length parameter.

  1. theorem OAI.CubicFirstMoment.UniformLogWeights.primaryAngularLattice_bounded line 14
  2. theorem OAI.CubicFirstMoment.UniformLogWeights.primaryCoprimeAngularLattice_bound line 36
  3. theorem OAI.CubicFirstMoment.UniformLogWeights.squarefreeCoprimeAngularLattice_bound line 63

    Source documentation

    The angular lattice model, with one constant for the whole given smooth weight family.

    theorem UniformLogWeights.squarefreeCoprimeAngularLattice_bound {ι : Type*} {W : ι → ℝ → ℂ}
    (h : UniformLogWeights W) {ℓ : ℤ} (hℓ : ℓ ≠ 0) {ε : ℝ} (hε : 0 < ε) :
    ∃ K : ℝ, 0 < K ∧ ∀ i r, primary r → Squarefree r → ∀ Y, 1 ≤ Y →
      ‖squarefreeCoprimeAngularLattice r ℓ (W i) Y‖ ≤ K*norm r^ε*Real.sqrt Y := by
…

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