CubeFrequencies.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The exact cube frequencies after square-divisor sieving

For a squarefree divisor d, the frequencies with d*h a cube are precisely d²*j³. Every nonzero such frequency has three preimages.

theorem OAI.CubicFirstMoment.squarefree_mul_cube_iff line 18
Source documentation
Squarefreeness forces the full d² factor in a principal frequency.
```
theorem squarefree_mul_cube_iff {d h : Eisenstein} (hd : d ≠ 0) (hs : Squarefree d) :
    (∃ j : Eisenstein, d*h = j^3) ↔ ∃ j : Eisenstein, h = d^2*j^3 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
lemma OAI.CubicFirstMoment.cube_eq_iff line 32
theorem OAI.CubicFirstMoment.cube_fiber_eq line 51
Source documentation
The three roots differ exactly by the cube roots of unity.
```
theorem cube_fiber_eq {y : Eisenstein} :
    {x : Eisenstein | x^3 = y^3} = {y,omegaE*y,omegaE^2*y} := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.omegaE
theorem OAI.CubicFirstMoment.cube_eq_integer_mod_three line 57
Source documentation
Every Eisenstein cube is a rational integer modulo three.
```
theorem cube_eq_integer_mod_three (j : Eisenstein) :
    ∃ n : ℤ, (3 : Eisenstein) ∣ j^3-(n : Eisenstein) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein
lemma OAI.CubicFirstMoment.tracePhase_rational_mod_three line 67
theorem OAI.CubicFirstMoment.squarefree_cube_frequency_phase line 91
Source documentation
The additive phase in the Poisson formula is one on every principal frequency produced by the squarefree majorant.
```
theorem squarefree_cube_frequency_phase {d : Eisenstein} (hd : primary d)
    (j : Eisenstein) :
    (Real.fourierChar (tracePair ((d^2*j^3 : Eisenstein) : ℂ)
      (1/(3*traceLambda))) : ℂ) = 1 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.tracePair, OAI.CubicFirstMoment.traceLambda
lemma OAI.CubicFirstMoment.omegaE_mul_injective line 105
theorem OAI.CubicFirstMoment.cube_fiber_card line 113
Source documentation
The factor 1/3 in the cube-lattice sum is the exact fiber size, including all three units whose cubes are one.
```
theorem cube_fiber_card {y : Eisenstein} (hy : y ≠ 0) :
    {x : Eisenstein | x^3 = y^3}.ncard = 3 := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein