OAI/NumberTheory/CubicGauss/CubicFourier.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Composite character primitivity and Fourier transforms of cubic correlations.

  1. lemma OAI.CubicFirstMoment.cubicSymbol_one_upper line 18
  2. def OAI.CubicFirstMoment.compositeCubicChar line 25
  3. lemma OAI.CubicFirstMoment.compositeCubicChar_mk line 45
  4. lemma OAI.CubicFirstMoment.isCoprime_of_residue_isUnit line 49

    Distinct definitions of this name: OAI/NumberTheory/CubicMoment/Estimates/PrimaryHeckeCharacter.lean:15 (different declaration text). Qualify references as OAI.CubicFirstMoment.isCoprime_of_residue_isUnit@path.

  5. lemma OAI.CubicFirstMoment.residue_isUnit_iff_isCoprime line 60
  6. lemma OAI.CubicFirstMoment.lambdaE_coe_lambda line 64
  7. lemma OAI.CubicFirstMoment.primary_isCoprime_three line 68
  8. lemma OAI.CubicFirstMoment.primary_isCoprime_lambda line 73
  9. lemma OAI.CubicFirstMoment.residueTraceChar_lambda_shift line 78
  10. lemma OAI.CubicFirstMoment.composite_gauss_exact line 95
  11. lemma OAI.CubicFirstMoment.composite_gauss_norm line 103
  12. lemma OAI.CubicFirstMoment.composite_gauss_norm_sq line 125
  13. lemma OAI.CubicFirstMoment.composite_fourier line 135
  14. lemma OAI.CubicFirstMoment.composite_fourier_neg line 148
  15. lemma OAI.CubicFirstMoment.tracePhase_neg_left line 154
  16. lemma OAI.CubicFirstMoment.residueFourier_conj line 163
  17. lemma OAI.CubicFirstMoment.composite_fourier_conj line 170
  18. lemma OAI.CubicFirstMoment.cubicSymbol_congr_of_dvd line 182
  19. def OAI.CubicFirstMoment.correlationResidue line 188
  20. lemma OAI.CubicFirstMoment.correlationResidue_mk line 192
  21. lemma OAI.CubicFirstMoment.tracePhase_mix line 199
  22. lemma OAI.CubicFirstMoment.cubic_correlation_mix line 209
  23. lemma OAI.CubicFirstMoment.correlation_fourier_factor line 232
  24. theorem OAI.CubicFirstMoment.cubic_correlation_fourier line 270
  25. theorem OAI.CubicFirstMoment.cubic_correlation_poisson line 280