OAI/NumberTheory/CubicMoment/Estimates/CubeSummation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Three-to-one summation of cube frequencies

This is the exact multiplicity correction before estimating the cube lattice. Summability is stated explicitly so that regrouping is valid.

  1. lemma OAI.CubicFirstMoment.cube_fiber_sum line 17
  2. theorem OAI.CubicFirstMoment.tsum_nonzero_cubes line 61

    Source documentation

    Regrouping the nonzero cubes divides their lattice parametrization by exactly three. No asymptotic estimate enters this identity.

    theorem tsum_nonzero_cubes (F : Eisenstein → ℂ)
    (hF : Summable (fun j : Eisenstein => if j = 0 then 0 else F (j^3))) :
    (∑' j : Eisenstein, if j = 0 then 0 else F (j^3)) =
      3*(∑' h : Eisenstein, if h ≠ 0 ∧ (∃ j : Eisenstein, j^3 = h) then F h else 0) := by
…

    Mentions: OAI.CubicFirstMoment.Eisenstein