CubePoisson.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The actual principal frequencies in the dispersion Poisson formula

At h = d²*j³, the additive phase is one and the character factors are precisely the coprimality indicator. The radial argument loses its d scale exactly, before any lattice estimate is applied.

lemma OAI.CubicFirstMoment.cubicSymbol_cube_value line 18
lemma OAI.CubicFirstMoment.cube_character_phase line 26
lemma OAI.CubicFirstMoment.cube_mixed_character_phase line 40

theorem OAI.CubicFirstMoment.cube_gramDualTerm line 56

Source documentation

This is the literal principal-frequency summand of the sieved Poisson expansion. It retains the exclusion of common prime factors.

theorem cube_gramDualTerm {a b d : Eisenstein}
    (ha : primary a) (hb : primary b) (hd : primary d)
    (had : IsCoprime a d) (hbd : IsCoprime b d)
    (W : ℝ → ℂ) {A : ℝ} (hA : 0 ≤ A) (j : Eisenstein) :
    mixedSymbol b a (d^2)*gramDualTerm b a W (A/(norm d)^2) (d^2*j^3) =
      if IsCoprime a j ∧ IsCoprime b j then
        radialDualProfile W (A*(norm j)^3/(27*norm (b*a))) else 0 := by
…

Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.mixedSymbol, OAI.CubicFirstMoment.gramDualTerm, OAI.CubicFirstMoment.norm, OAI.CubicFirstMoment.radialDualProfile