OAI/NumberTheory/CubicMoment/Theta/CubicThetaSieveSupport.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CubicFirstMoment.cubicThetaPrimarySupport line 10
2. lemma OAI.CubicFirstMoment.cubicThetaPrimarySupport_coordinates line 13
3. lemma OAI.CubicFirstMoment.cubicThetaPrimarySupport_iff line 22

   Source documentation

   This is the source set S, written on the common numerator lattice.

   lemma cubicThetaPrimarySupport_iff (n : Eisenstein) :
       cubicThetaPrimarySupport n ↔ ∃ c d : Eisenstein,
         primary c ∧ primary d ∧ Squarefree c ∧ n = lambdaE*c*d^3 := by
   …

   Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.cubicThetaPrimarySupport, OAI.CubicFirstMoment.primary, OAI.CubicFirstMoment.lambdaE

4. def OAI.CubicFirstMoment.cubicThetaRootProjector line 43
5. lemma OAI.CubicFirstMoment.cubicThetaRootProjector_one line 45
6. lemma OAI.CubicFirstMoment.cubicThetaRootProjector_omega line 49
7. lemma OAI.CubicFirstMoment.cubicThetaRootProjector_omega_sq line 59
8. lemma OAI.CubicFirstMoment.CubicThetaCoordinates.primary_product line 69
9. lemma OAI.CubicFirstMoment.cubicThetaRootProjector_coefficient line 76
10. theorem OAI.CubicFirstMoment.cubicThetaRootProjector_arithmetic line 116

    Source documentation

    Multiplying the actual conjugate theta coefficient by the finite third-root projector cuts it down to precisely the source set S.

    theorem cubicThetaRootProjector_arithmetic (n : Eisenstein) :
        cubicThetaRootProjector (cubicThetaSievePhase n)*star (cubicThetaArithmeticCoefficient n) =
          if cubicThetaPrimarySupport n then star (cubicThetaArithmeticCoefficient n) else 0 := by
    …

    Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.cubicThetaRootProjector, OAI.CubicFirstMoment.cubicThetaSievePhase, OAI.CubicFirstMoment.cubicThetaArithmeticCoefficient, OAI.CubicFirstMoment.cubicThetaPrimarySupport