OAI/NumberTheory/DirichletL/CubicSieve/Ideal.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CubicSieve.Admissible line 14
  2. def OAI.SevenEighths.CubicSieve.idealKernel line 16
  3. theorem OAI.SevenEighths.CubicSieve.idealKernel_reciprocity line 19
  4. theorem OAI.SevenEighths.CubicSieve.idealKernel_norm_le_one line 24
  5. theorem OAI.SevenEighths.CubicSieve.idealSymbol_fourth line 29
  6. theorem OAI.SevenEighths.CubicSieve.idealSymbol_cube_mask line 57
  7. theorem OAI.SevenEighths.CubicSieve.idealKernel_square_eq_star line 109
  8. def OAI.SevenEighths.CubicSieve.idealNumeratorHom line 113
  9. theorem OAI.SevenEighths.CubicSieve.idealKernel_row_decomposition line 122
  10. def OAI.SevenEighths.CubicSieve.idealRange line 131
  11. theorem OAI.SevenEighths.CubicSieve.mem_idealRange line 134
  12. def OAI.SevenEighths.CubicSieve.idealMatrix line 150
  13. def OAI.SevenEighths.CubicSieve.sieveNorm line 153
  14. theorem OAI.SevenEighths.CubicSieve.sieveNorm_reciprocity line 155
  15. theorem OAI.SevenEighths.CubicSieve.ideal_energy_bound line 161
  16. theorem OAI.SevenEighths.CubicSieve.family_squared_norm_le line 167
  17. theorem OAI.SevenEighths.CubicSieve.ideal_cube_block_energy_le line 181
  18. theorem OAI.SevenEighths.CubicSieve.ideal_cubic_factorization line 209