OAI/NumberTheory/DirichletL/Eisenstein/GreenIdentity.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicEisenstein.greenWronskian line 77
  2. def OAI.CubicEisenstein.greenSecondTerm line 80
  3. lemma OAI.CubicEisenstein.hasDerivAt_greenWronskian line 83
  4. lemma OAI.CubicEisenstein.weighted_vertical_green line 93
  5. theorem OAI.CubicEisenstein.actual_eisenstein_vertical_green line 130
  6. lemma OAI.CubicEisenstein.axisSlice_self line 155
  7. theorem OAI.CubicEisenstein.actual_eisenstein_green_density line 159
  8. theorem OAI.CanonicalQuadraticSieve.symmetric_truncation_scales line 185
  9. theorem OAI.CanonicalQuadraticSieve.symmetric_truncation_scalar_bound line 195
  10. def OAI.SecondPassArithmetic.SecondSourceSupport line 268
  11. theorem OAI.SecondPassArithmetic.secondExpansionSource_singleton_zero_of_not_support line 280
  12. theorem OAI.SecondPassArithmetic.secondExpansionSource_eq_supported line 329
  13. def OAI.SecondPassArithmetic.normLogBin line 361
  14. def OAI.SecondPassArithmetic.normLogScale line 362
  15. lemma OAI.SecondPassArithmetic.normLogScale_pos line 364
  16. lemma OAI.SecondPassArithmetic.normLogScale_ge_one line 365
  17. lemma OAI.SecondPassArithmetic.normLogBin_error line 368
  18. lemma OAI.SecondPassArithmetic.normLogBin_scale_bounds line 375
  19. lemma OAI.SecondPassArithmetic.normLogBin_mono line 385
  20. abbrev OAI.SecondPassArithmetic.SecondLogIndex line 388
  21. def OAI.SecondPassArithmetic.secondLogE line 390
  22. def OAI.SecondPassArithmetic.secondLogV line 391
  23. def OAI.SecondPassArithmetic.secondLogK line 392
  24. def OAI.SecondPassArithmetic.secondLogIndex line 397
  25. def OAI.SecondPassArithmetic.secondLogX line 401
  26. lemma OAI.SecondPassArithmetic.secondLogX_pos line 406
  27. lemma OAI.SecondPassArithmetic.actualSecondRow_ne_zero line 412
  28. lemma OAI.SecondPassArithmetic.element_norm_ge_one line 416
  29. theorem OAI.SecondPassArithmetic.secondLogIndex_coordinates line 425
  30. theorem OAI.SecondPassArithmetic.secondLogX_radial_scale line 478
  31. def OAI.SecondPassArithmetic.secondBaseLabel line 495
  32. lemma OAI.SecondPassArithmetic.secondBaseLabel_ne_zero line 500
  33. theorem OAI.SecondPassArithmetic.secondSupportNewLabel_norm line 508
  34. lemma OAI.SecondPassArithmetic.secondSupportNewLabel_ne_bot line 519
  35. def OAI.SecondPassArithmetic.secondLogLabelBound line 526
  36. lemma OAI.SecondPassArithmetic.secondLogLabelBound_ge_one line 532
  37. theorem OAI.SecondPassArithmetic.secondLogIndex_target_bounds line 544
  38. theorem OAI.SecondPassArithmetic.secondLogX_label_cost line 569
  39. def OAI.SecondPassArithmetic.secondLogBinBox line 583
  40. lemma OAI.SecondPassArithmetic.secondLogBinBox_card line 587
  41. theorem OAI.SecondPassArithmetic.secondSourceSupport_bounds line 597
  42. lemma OAI.SecondPassArithmetic.secondLogIndex_mem_box line 609
  43. def OAI.SecondPassArithmetic.secondSupportedSector line 621
  44. def OAI.SecondPassArithmetic.secondLogSector line 625
  45. lemma OAI.SecondPassArithmetic.secondSupportedSector_mem line 630
  46. lemma OAI.SecondPassArithmetic.secondLogSector_subset line 643
  47. theorem OAI.SecondPassArithmetic.sum_secondLogSector line 650
  48. theorem OAI.SecondPassArithmetic.secondLogX_lower line 672