OAI/NumberTheory/DirichletL/CubicSieve/TwistedProfiles.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SecondPassArithmetic.actualSecondRawVariableSector_twisted_profiles line 87
  2. theorem OAI.SecondPassArithmetic.actual_raw_twisted_sector_transfer line 139
  3. def OAI.SecondPassArithmetic.firstCoreBaseProfile line 212
  4. def OAI.SecondPassArithmetic.firstCoreModeHeight line 215
  5. def OAI.SecondPassArithmetic.firstCoreModeProfile line 217
  6. theorem OAI.SecondPassArithmetic.firstCoreBaseProfile_apply line 220
  7. lemma OAI.SecondPassArithmetic.logPhase_neg_argument line 227
  8. theorem OAI.SecondPassArithmetic.firstCoreModeProfile_apply line 233
  9. theorem OAI.SecondPassArithmetic.firstCoreModeProfile_norm line 241
  10. theorem OAI.SecondPassArithmetic.firstCoreModeProfile_support line 246
  11. theorem OAI.SecondPassArithmetic.firstCoreTest_eq_normalized_mode line 260
  12. theorem OAI.SecondPassArithmetic.firstCoreInputRow_eq_mode_row line 273
  13. theorem OAI.SecondPassArithmetic.firstCoreInputRow_mode_norm_sq line 294
  14. abbrev OAI.CubicEisenstein.UpperCoordinates line 318
  15. def OAI.CubicEisenstein.coordinateSection line 320
  16. lemma OAI.CubicEisenstein.continuous_coordinate_inverse_operator line 323
  17. lemma OAI.CubicEisenstein.continuous_coordinate_rowBound line 348
  18. lemma OAI.CubicEisenstein.continuous_coordinate_summand line 352
  19. lemma OAI.CubicEisenstein.coordinate_summable_majorant line 373
  20. theorem OAI.CubicEisenstein.coordinate_eisenstein_continuousAt line 399
  21. theorem OAI.CubicEisenstein.coordinate_eisenstein_tendstoUniformlyOn line 426
  22. theorem OAI.CubicEisenstein.coordinate_eisenstein_continuousOn line 436
  23. theorem OAI.CubicEisenstein.upperEisenstein_joint_continuousAt line 441
  24. def OAI.CubicEisenstein.logRatioPower line 454
  25. lemma OAI.CubicEisenstein.logRatioPower_eq_cpow line 457
  26. lemma OAI.CubicEisenstein.hasDerivAt_logRatioPower line 465
  27. lemma OAI.CubicEisenstein.hasDerivAt_deriv_logRatioPower line 473
  28. def OAI.CubicEisenstein.quadraticHeightDenominator line 494
  29. lemma OAI.CubicEisenstein.quadraticHeightDenominator_hasDerivAt_x line 497
  30. lemma OAI.CubicEisenstein.quadraticHeightDenominator_hasDerivAt_y line 504
  31. lemma OAI.CubicEisenstein.quadraticHeightDenominator_hasDerivAt_v line 511
  32. def OAI.CubicEisenstein.spatialHeightPower line 517
  33. def OAI.CubicEisenstein.heightLogDx line 520
  34. def OAI.CubicEisenstein.heightLogDy line 522
  35. def OAI.CubicEisenstein.heightLogDv line 524
  36. def OAI.CubicEisenstein.heightLogDxx line 527
  37. def OAI.CubicEisenstein.heightLogDyy line 530
  38. def OAI.CubicEisenstein.heightLogDvv line 533
  39. lemma OAI.CubicEisenstein.deriv_spatialHeightPower_v line 537
  40. lemma OAI.CubicEisenstein.deriv2_spatialHeightPower_x line 544
  41. lemma OAI.CubicEisenstein.deriv2_spatialHeightPower_y line 559
  42. lemma OAI.CubicEisenstein.deriv2_spatialHeightPower_v line 574
  43. lemma OAI.CubicEisenstein.quadraticHeight_gradient_square line 591
  44. lemma OAI.CubicEisenstein.heightLog_eikonal line 598
  45. lemma OAI.CubicEisenstein.heightLog_laplacian line 611
  46. def OAI.CubicEisenstein.hyperbolicLaplacian line 625
  47. theorem OAI.CubicEisenstein.spatialHeightPower_eigenfunction line 630
  48. lemma OAI.CubicEisenstein.complex_row_quadratic_relation line 656
  49. lemma OAI.CubicEisenstein.heightDenominator_eq_quadratic line 662
  50. def OAI.CubicEisenstein.actualHeightPower line 672
  51. lemma OAI.CubicEisenstein.actualHeightPower_eq_spatial line 675
  52. theorem OAI.CubicEisenstein.actualHeightPower_eigenfunction line 685
  53. lemma OAI.CubicEisenstein.hyperbolicLaplacian_const_mul line 712
  54. theorem OAI.CubicEisenstein.eisenstein_summand_eigenfunction line 719
  55. lemma OAI.CubicEisenstein.eigenfunction_summand_eq_actual_series line 727