OAI/NumberTheory/DirichletL/QuadraticSieve/HighKernelGeometry.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CanonicalQuadraticSieve.finite_inverse_norm_square_sum line 77
  2. theorem OAI.CanonicalQuadraticSieve.highSquareParts_card_le line 123
  3. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.high_kernel line 136
  4. def OAI.CubicEisenstein.bottomRowUnitary line 189
  5. lemma OAI.CubicEisenstein.bottomRowUnitary_mem line 192
  6. lemma OAI.CubicEisenstein.iwasawa_z_row_identities line 206
  7. def OAI.CubicEisenstein.matrixHorizontal line 219
  8. lemma OAI.CubicEisenstein.matrix_iwasawa_factor line 222
  9. theorem OAI.CubicEisenstein.upperPoint_surjective line 286
  10. lemma OAI.CubicEisenstein.eisEmbedding_range_closed line 313
  11. lemma OAI.CubicEisenstein.exists_nearest_eisenstein line 330
  12. lemma OAI.CubicEisenstein.hexagon_norm_sq_bound line 339
  13. theorem OAI.CubicEisenstein.exists_eisenstein_distance_sq_le_third line 360
  14. def OAI.CubicEisenstein.integralBottomRow line 402
  15. def OAI.CubicEisenstein.integralRowEnergy line 403
  16. lemma OAI.CubicEisenstein.integralRowEnergy_sublevel_finite line 406
  17. lemma OAI.CubicEisenstein.integral_height_action_matrix line 417
  18. lemma OAI.CubicEisenstein.integralRowEnergy_bottom_pos line 424
  19. theorem OAI.CubicEisenstein.exists_maximal_integral_height line 430
  20. def OAI.CubicEisenstein.integralTranslation line 462
  21. def OAI.CubicEisenstein.integralInversion line 464
  22. lemma OAI.CubicEisenstein.integralTranslation_action line 467
  23. lemma OAI.CubicEisenstein.integralInversion_height line 483
  24. theorem OAI.CubicEisenstein.bianchi_ford_cover line 495
  25. theorem OAI.CubicEisenstein.bianchi_reduction_height_floor line 526
  26. def OAI.CubicEisenstein.truncatedFordBox line 535
  27. lemma OAI.CubicEisenstein.truncatedFordBox_isCompact line 537
  28. lemma OAI.CubicEisenstein.mem_truncatedFordBox line 540
  29. lemma OAI.CubicEisenstein.levelThree_finiteIndex line 557
  30. def OAI.CubicEisenstein.finiteCubicMultiplier line 562
  31. def OAI.CubicEisenstein.globalKubotaKernel line 573
  32. lemma OAI.CubicEisenstein.globalKubotaKernel_finiteIndex line 575
  33. lemma OAI.CubicEisenstein.finiteCubicMultiplier_coe line 583
  34. lemma OAI.CubicEisenstein.finiteCubicMultiplier_eq_one line 586
  35. lemma OAI.CubicEisenstein.globalKubotaKernel_mem line 597
  36. lemma OAI.CubicEisenstein.finite_right_representatives line 606
  37. theorem OAI.CubicEisenstein.finiteIndex_ford_cover line 616
  38. theorem OAI.CubicEisenstein.levelThree_ford_cover line 630
  39. theorem OAI.CubicEisenstein.globalKubotaKernel_ford_cover line 638