OAI/NumberTheory/DirichletL/Eisenstein/SmoothSummands.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicEisenstein.smoothEisenstein line 78
  2. lemma OAI.CubicEisenstein.smoothEisenstein_eq_actual line 80
  3. lemma OAI.CubicEisenstein.summable_smoothSummand line 85
  4. theorem OAI.CubicEisenstein.eisenstein_axis_termwise line 90
  5. def OAI.CubicEisenstein.axisLaplacian line 119
  6. lemma OAI.CubicEisenstein.axisSlice_zero line 123
  7. lemma OAI.CubicEisenstein.axisSlice_one line 127
  8. lemma OAI.CubicEisenstein.axisSlice_two line 131
  9. lemma OAI.CubicEisenstein.axisLaplacian_eq_hyperbolicLaplacian line 136
  10. lemma OAI.CubicEisenstein.smoothSummand_axisLaplacian line 142
  11. theorem OAI.CubicEisenstein.smoothEisenstein_eigenfunction line 157
  12. lemma OAI.CubicEisenstein.axisSlice_eventuallyEq_of_positive line 180
  13. lemma OAI.CubicEisenstein.axisLaplacian_congr_positive line 190
  14. def OAI.CubicEisenstein.upperEisensteinField line 201
  15. lemma OAI.CubicEisenstein.upperEisensteinField_eq_smooth line 204
  16. theorem OAI.CubicEisenstein.upperEisenstein_eigenfunction line 209
  17. lemma OAI.SecondPassArithmetic.firstCoreModeHeight_norm line 229
  18. theorem OAI.SecondPassArithmetic.firstCoreInputRow_finite_second_transfer line 233
  19. lemma OAI.SecondPassArithmetic.residualPairWeight_test_ne_zero line 371
  20. theorem OAI.SecondPassArithmetic.residualTailCost_frequencyTwist line 383
  21. theorem OAI.SecondPassArithmetic.firstCoreSecondCutoff_tail_bound line 397
  22. lemma OAI.CanonicalQuadraticSieve.divisorPool_filter line 452
  23. lemma OAI.CanonicalQuadraticSieve.divisor_product_delta line 459
  24. lemma OAI.CanonicalQuadraticSieve.four_sums_exchange line 475
  25. lemma OAI.CanonicalQuadraticSieve.three_sums_exchange line 484
  26. theorem OAI.CanonicalQuadraticSieve.originalTerm_product_divisor line 496
  27. theorem OAI.CanonicalQuadraticSieve.originalColumnSum_product_divisor line 530
  28. theorem OAI.CanonicalQuadraticSieve.originalColumnSum_divisor_rectangles line 559
  29. lemma OAI.CanonicalQuadraticSieve.positive_ideal_dyadic_exists line 609
  30. def OAI.CanonicalQuadraticSieve.divisorDyadicLabel line 617
  31. def OAI.CanonicalQuadraticSieve.divisorDyadicBin line 623
  32. def OAI.CanonicalQuadraticSieve.divisorDyadicScale line 627
  33. lemma OAI.CanonicalQuadraticSieve.divisorDyadicLabel_bounds line 629
  34. lemma OAI.CanonicalQuadraticSieve.divisorDyadicScale_ge_one line 637
  35. theorem OAI.CanonicalQuadraticSieve.divisorDyadicBin_bounds line 639
  36. theorem OAI.CanonicalQuadraticSieve.divisorDyadicBin_scale_le line 652
  37. theorem OAI.CanonicalQuadraticSieve.sum_divisorDyadicBins line 659
  38. theorem OAI.CanonicalQuadraticSieve.sum_divisorDyadicRectangles line 668
  39. def OAI.CanonicalQuadraticSieve.columnDivisorPool line 688
  40. theorem OAI.CanonicalQuadraticSieve.mem_columnDivisorPool_of_dvd line 691
  41. theorem OAI.CanonicalQuadraticSieve.columnDivisorPool_norm_bounds line 697