OAI/NumberTheory/DirichletL/CubicSieve/RowCaps.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SecondPassArithmetic.globalFirstRowCap line 82
  2. theorem OAI.SecondPassArithmetic.globalFirstRowCap_pos line 85
  3. theorem OAI.SecondPassArithmetic.globalFirstPooledRow_le_cap line 95
  4. theorem OAI.SecondPassArithmetic.globalTwoPassage_original_ranges line 145
  5. abbrev OAI.CompletedGauss.actualSextic line 204
  6. def OAI.CompletedGauss.exceptionalPiece line 206
  7. theorem OAI.CompletedGauss.bracket_four_eq_sum_exceptionalPiece line 211
  8. def OAI.CompletedGauss.exceptionalBranch line 219
  9. theorem OAI.CompletedGauss.prod_bracket_four_eq_branches line 223
  10. def OAI.CompletedGauss.exceptionalDivisor line 232
  11. theorem OAI.CompletedGauss.exceptionalBranch_support line 235
  12. theorem OAI.CompletedGauss.exceptionalBranch_divisibility line 249
  13. theorem OAI.CompletedGauss.rootCard_eq_sqrt_absNorm line 279
  14. def OAI.CompletedGauss.exceptionalSize line 284
  15. theorem OAI.CompletedGauss.exceptionalPiece_norm_le line 288
  16. theorem OAI.CompletedGauss.exceptionalBranch_norm_le line 297
  17. theorem OAI.CompletedGauss.exceptionalDivisor_ne_zero line 303
  18. theorem OAI.CompletedGauss.sqrt_norm_exceptionalDivisor line 313
  19. theorem OAI.CompletedGauss.exceptionalSize_eq line 326
  20. theorem OAI.CompletedGauss.exceptional_normalized_bound line 339
  21. theorem OAI.CanonicalQuadraticSieve.product_quadratic_norm_scaled line 363
  22. theorem OAI.CanonicalQuadraticSieve.completed_quadratic_dyad line 413
  23. def OAI.CubicEisenstein.spatialHorizontal line 445
  24. def OAI.CubicEisenstein.mobiusSpatialDenominator line 447
  25. def OAI.CubicEisenstein.mobiusSpatialHorizontal line 450
  26. def OAI.CubicEisenstein.mobiusSpatial line 454
  27. lemma OAI.CubicEisenstein.mobiusSpatialDenominator_pos line 458
  28. lemma OAI.CubicEisenstein.mobiusSpatial_positive line 463
  29. lemma OAI.CubicEisenstein.mobiusSpatial_coordinates line 466
  30. lemma OAI.CubicEisenstein.spatialHorizontal_contDiff line 472
  31. lemma OAI.CubicEisenstein.mobiusSpatialDenominator_contDiff line 477
  32. lemma OAI.CubicEisenstein.mobiusSpatial_contDiffAt line 489
  33. abbrev OAI.CubicEisenstein.PositiveSpatial line 518
  34. def OAI.CubicEisenstein.positiveSpatialToUpper line 520
  35. def OAI.CubicEisenstein.upperToPositiveSpatial line 522
  36. lemma OAI.CubicEisenstein.positiveSpatialToUpper_continuous line 525
  37. lemma OAI.CubicEisenstein.upperToPositiveSpatial_continuous line 529
  38. def OAI.CubicEisenstein.positiveSpatialUpperHomeomorph line 535
  39. def OAI.CubicEisenstein.positiveSpatialHomeomorph line 550
  40. lemma OAI.CubicEisenstein.hyperbolicSpatial_isOpenEmbedding line 553
  41. abbrev OAI.CubicEisenstein.KernelQuotient line 565
  42. def OAI.CubicEisenstein.hyperbolicSpatialChart line 567
  43. lemma OAI.CubicEisenstein.hyperbolicSpatialChart_apply line 570
  44. lemma OAI.CubicEisenstein.hyperbolicSpatialChart_source line 573
  45. lemma OAI.CubicEisenstein.hyperbolicSpatialChart_target_positive line 575
  46. def OAI.CubicEisenstein.kernelLocalLift line 581
  47. lemma OAI.CubicEisenstein.kernelLocalLift_symm line 584
  48. lemma OAI.CubicEisenstein.kernelLocalLift_project line 588
  49. lemma OAI.CubicEisenstein.kernel_lifts_eventually_eq line 593
  50. lemma OAI.CubicEisenstein.kernel_lifts_eventually_deck line 604
  51. lemma OAI.CubicEisenstein.mobiusSpatial_coordinates_global line 617
  52. def OAI.CubicEisenstein.kernelCoordinateTransition line 624
  53. lemma OAI.CubicEisenstein.kernelCoordinateTransition_eventually line 628
  54. lemma OAI.CubicEisenstein.kernelCoordinateTransition_contDiffAt line 659
  55. def OAI.CubicEisenstein.kernelQuotientChart line 666
  56. lemma OAI.CubicEisenstein.kernelQuotientChart_symm line 669
  57. lemma OAI.CubicEisenstein.kernelQuotientChart_contDiffOn line 675