OAI/NumberTheory/DirichletL/Eisenstein/CuspIntegration.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicEisenstein.spatialTriple line 77
  2. lemma OAI.CubicEisenstein.spatialTriple_zero line 78
  3. lemma OAI.CubicEisenstein.spatialTriple_one line 79
  4. lemma OAI.CubicEisenstein.spatialTriple_two line 80
  5. def OAI.CubicEisenstein.cuspCylinderMeasure line 82
  6. def OAI.CubicEisenstein.cuspBoxIntegral line 87
  7. lemma OAI.CubicEisenstein.continuous_spatialTriple line 90
  8. lemma OAI.CubicEisenstein.continuous_cuspBox_integrand line 97
  9. lemma OAI.CubicEisenstein.integrable_cuspBox line 101
  10. lemma OAI.CubicEisenstein.cuspBoxIntegral_add line 110
  11. lemma OAI.CubicEisenstein.cuspBoxIntegral_sub line 113
  12. lemma OAI.CubicEisenstein.cuspBoxIntegral_const_mul line 116
  13. lemma OAI.CubicEisenstein.cuspBoxIntegral_eq_iterated line 119
  14. lemma OAI.CubicEisenstein.cuspBoxIntegral_eq_vertical line 140
  15. lemma OAI.CubicEisenstein.rectangle_interval_swap line 161
  16. def OAI.CubicEisenstein.greenSecondField line 169
  17. def OAI.CubicEisenstein.greenWronskianField line 172
  18. def OAI.CubicEisenstein.greenAxisDensity line 175
  19. def OAI.CubicEisenstein.greenVerticalDensity line 177
  20. def OAI.CubicEisenstein.greenBoundaryFlux line 179
  21. def OAI.CubicEisenstein.clampHeight line 182
  22. lemma OAI.CubicEisenstein.clampHeight_continuous line 184
  23. lemma OAI.CubicEisenstein.clampHeight_eq line 187
  24. def OAI.CubicEisenstein.extendAboveHeight line 191
  25. lemma OAI.CubicEisenstein.extendAboveHeight_continuous line 193
  26. lemma OAI.CubicEisenstein.extendAboveHeight_eq line 199
  27. lemma OAI.CubicEisenstein.greenSecondField_update line 203
  28. lemma OAI.CubicEisenstein.greenWronskianField_update line 208
  29. lemma OAI.CubicEisenstein.greenFields_continuousAt line 214
  30. lemma OAI.CubicEisenstein.actual_green_fields_density line 234
  31. lemma OAI.CubicEisenstein.spatialTriple_update_zero line 246
  32. lemma OAI.CubicEisenstein.spatialTriple_update_one line 249
  33. lemma OAI.CubicEisenstein.spatialTriple_update_two line 252
  34. lemma OAI.CubicEisenstein.actual_green_axis_zero_integral line 256
  35. lemma OAI.CubicEisenstein.actual_green_axis_one_integral line 270
  36. lemma OAI.CubicEisenstein.actual_green_vertical_integral line 284
  37. lemma OAI.CubicEisenstein.cuspCylinder_ae_height line 299
  38. lemma OAI.CubicEisenstein.cuspBoxIntegral_congr line 303
  39. lemma OAI.CubicEisenstein.cuspBoxIntegral_extendAboveHeight line 310
  40. lemma OAI.CubicEisenstein.integrable_cuspBox_of_positive_continuity line 314
  41. lemma OAI.CubicEisenstein.cuspBox_green_axis_zero line 323
  42. lemma OAI.CubicEisenstein.cuspBox_green_axis_one line 340
  43. lemma OAI.CubicEisenstein.cuspBox_green_vertical line 359
  44. def OAI.CubicEisenstein.eisensteinHermitianDensity line 378
  45. lemma OAI.CubicEisenstein.integrable_eisensteinHermitianDensity line 381
  46. theorem OAI.CubicEisenstein.actual_eisenstein_cylinder_green line 393
  47. lemma OAI.CubicEisenstein.cuspBoxIntegral_eq_iterated_positive line 422
  48. lemma OAI.CubicEisenstein.eisensteinHermitianDensity_continuousAt line 437
  49. theorem OAI.CubicEisenstein.actual_eisenstein_cylinder_green_iterated line 445
  50. theorem OAI.CanonicalQuadraticSieve.sum_subtype_powerset_products line 466
  51. theorem OAI.CanonicalQuadraticSieve.primePool_singleton_eq_primeSupport line 483
  52. theorem OAI.CanonicalQuadraticSieve.primePool_subset_sum_eq_divisors line 487
  53. theorem OAI.CanonicalQuadraticSieve.middleTruncation_eq_ideal_divisors line 493
  54. theorem OAI.CanonicalQuadraticSieve.middleTruncation_eq_ideal_frequencies line 522
  55. theorem OAI.CanonicalQuadraticSieve.principalTruncation_eq_ideal_divisors line 547
  56. theorem OAI.CanonicalQuadraticSieve.finite_middle_triangle line 570
  57. theorem OAI.CanonicalQuadraticSieve.finite_nonzero_frequency_sum_le line 597
  58. theorem OAI.CanonicalQuadraticSieve.sum_two_finite_subtypes line 616
  59. def OAI.CanonicalQuadraticSieve.originalTruncatedMiddle line 625
  60. theorem OAI.CanonicalQuadraticSieve.original_truncated_pair_expansion line 633
  61. theorem OAI.CanonicalQuadraticSieve.originalTruncatedMiddle_le_product_divisors line 673
  62. theorem OAI.CanonicalQuadraticSieve.HasSieveExponent.original_truncated_middle line 722