OAI/NumberTheory/DirichletL/CubicSieve/FrequencyCutoffs.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SecondPassArithmetic.columnLog_norm_upper line 81
  2. def OAI.SecondPassArithmetic.secondFrequencyCutoff line 88
  3. theorem OAI.SecondPassArithmetic.mem_secondFrequencyCutoff line 91
  4. theorem OAI.SecondPassArithmetic.secondFrequencyCutoff_zero line 97
  5. theorem OAI.SecondPassArithmetic.outside_secondFrequencyCutoff line 101
  6. theorem OAI.SecondPassArithmetic.active_norm_sq_disjoint line 107
  7. theorem OAI.SecondPassArithmetic.secondFrequencyCutoff_uniform line 117
  8. def OAI.SecondPassArithmetic.truncatedSecondZero line 155
  9. theorem OAI.SecondPassArithmetic.truncatedSecondSource_eq_nonzero_add_zero line 166
  10. theorem OAI.SecondPassArithmetic.secondExpansionSector_frequency_ne_zero line 188
  11. theorem OAI.SecondPassArithmetic.normalized_second_sector_transfer line 207
  12. def OAI.CubicEisenstein.ramifiedIdeal line 330
  13. lemma OAI.CubicEisenstein.ramifiedIdeal_prime line 332
  14. lemma OAI.CubicEisenstein.goodIdeal_iff_not_ramified line 336
  15. lemma OAI.CubicEisenstein.ramifiedIdeal_absNorm line 342
  16. lemma OAI.CubicEisenstein.prime_power_remainder_multiplicity line 344
  17. abbrev OAI.CubicEisenstein.NonzeroIdeal line 352
  18. def OAI.CubicEisenstein.lambdaFactorMap line 354
  19. lemma OAI.CubicEisenstein.lambdaFactorMap_bijective line 358
  20. def OAI.CubicEisenstein.lambdaFactorEquiv line 378
  21. lemma OAI.CubicEisenstein.ideal_pow_injective line 381
  22. lemma OAI.CubicEisenstein.lambdaFactor_generator_span line 393
  23. lemma OAI.CubicEisenstein.three_dvd_lambda_sq line 399
  24. lemma OAI.CubicEisenstein.unit_cube_eq_sign line 403
  25. def OAI.CubicEisenstein.cubeSign line 426
  26. lemma OAI.CubicEisenstein.cubeSign_isUnit line 430
  27. lemma OAI.CubicEisenstein.cubeSign_cube line 433
  28. lemma OAI.CubicEisenstein.cubeSign_injective line 436
  29. def OAI.CubicEisenstein.cubeBase line 441
  30. def OAI.CubicEisenstein.cubeColumn line 443
  31. lemma OAI.CubicEisenstein.cubeBase_ne_zero line 445
  32. lemma OAI.CubicEisenstein.cubeColumn_ne_zero line 448
  33. lemma OAI.CubicEisenstein.cubeColumn_cube line 451
  34. lemma OAI.CubicEisenstein.cubeColumn_level line 456
  35. lemma OAI.CubicEisenstein.cubeColumn_span line 465
  36. abbrev OAI.CubicEisenstein.CubeLower line 472
  37. def OAI.CubicEisenstein.cubeColumnMap line 474
  38. lemma OAI.CubicEisenstein.cubeColumnMap_injective line 479
  39. lemma OAI.CubicEisenstein.cubeColumnMap_surjective line 495
  40. def OAI.CubicEisenstein.cubeColumnEquiv line 529
  41. lemma OAI.CubicEisenstein.cubeColumn_expanded line 532
  42. lemma OAI.CubicEisenstein.cubeColumn_arithmetic_sum line 538
  43. lemma OAI.CubicEisenstein.cubeColumn_norm line 553
  44. def OAI.CubicEisenstein.ramifiedRatio line 558
  45. lemma OAI.CubicEisenstein.cube_norm_weight_algebra line 560
  46. lemma OAI.CubicEisenstein.cubeColumn_dirichletTerm line 591