OAI/NumberTheory/DirichletL/Eisenstein/SourceMellinInversion.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicEisenstein.source_period_of_three_supported line 83
  2. theorem OAI.CubicEisenstein.exists_source_coefficient_not_three line 104
  3. theorem OAI.CubicEisenstein.exists_sourceArithmeticResidue_not_three line 117
  4. lemma OAI.CompletedGauss.compactMellin_vertical_integrable line 133
  5. theorem OAI.CompletedGauss.compactMellin_inversion line 150
  6. lemma OAI.CompletedGauss.positive_cpow_vertical_norm line 166
  7. lemma OAI.CompletedGauss.positive_cpow_negative_vertical_norm line 171
  8. lemma OAI.CompletedGauss.positive_cpow_vertical_continuous line 176
  9. lemma OAI.CompletedGauss.positive_cpow_negative_vertical_continuous line 181
  10. lemma OAI.CompletedGauss.vertical_power_mul_integrable line 186
  11. lemma OAI.CompletedGauss.weighted_vertical_power_integrable line 193
  12. lemma OAI.CompletedGauss.weighted_vertical_power_integral_norm line 201
  13. theorem OAI.CompletedGauss.weighted_vertical_sum_integral line 206
  14. lemma OAI.CompletedGauss.positive_quotient_cpow_neg line 220
  15. theorem OAI.CompletedGauss.weightedMellin_inversion line 225
  16. lemma OAI.CompletedGauss.angularFactor_norm_le_one line 265
  17. lemma OAI.CompletedGauss.cubicRow_norm_le_one line 270
  18. lemma OAI.CompletedGauss.gaussTwo_norm_le_sqrt line 279
  19. lemma OAI.CompletedGauss.columnWeight_div_sqrt_norm_le_one line 307
  20. lemma OAI.CompletedGauss.cubeWeight_norm_le_one line 319
  21. abbrev OAI.CompletedGauss.CompletedMellinIndex line 346
  22. def OAI.CompletedGauss.completedMellinLength line 348
  23. def OAI.CompletedGauss.completedMellinCoefficient line 351
  24. lemma OAI.CompletedGauss.nonzeroIdeal_norm_pos line 354
  25. lemma OAI.CompletedGauss.completedMellinLength_pos line 357
  26. lemma OAI.CompletedGauss.completedMellinCoefficient_norm_le_one line 360
  27. lemma OAI.CompletedGauss.nonzeroIdeal_norm_rpow_summable line 366
  28. lemma OAI.CompletedGauss.completedMellinLength_rpow line 376
  29. theorem OAI.CompletedGauss.completedMellinCoefficient_summable line 385
  30. def OAI.CompletedGauss.completedDirichletSeries line 399
  31. theorem OAI.CompletedGauss.completedT_eq_mellin_index line 403
  32. theorem OAI.CompletedGauss.completedT_initial_mellin line 435
  33. lemma OAI.CompletedGauss.nat_sqrt_cpow_half line 467
  34. lemma OAI.CompletedGauss.nat_half_shift_product line 473
  35. lemma OAI.CompletedGauss.completedDirichletTerm_expanded line 494
  36. theorem OAI.CompletedGauss.completedDirichletSeries_expanded line 510
  37. lemma OAI.CompletedGauss.weighted_vertical_series_continuous line 523
  38. lemma OAI.CompletedGauss.weighted_vertical_series_norm line 533
  39. lemma OAI.CompletedGauss.completedDirichletSeries_initial line 541
  40. theorem OAI.CompletedGauss.completedT_initial_mellin_integrable line 551
  41. def OAI.CompletedGauss.dualIdealDyad line 579
  42. lemma OAI.CompletedGauss.mem_dualIdealDyad line 583
  43. lemma OAI.CompletedGauss.dualIdealDyad_bounds line 593
  44. abbrev OAI.CompletedGauss.NonzeroDualIdeal line 604
  45. def OAI.CompletedGauss.dualDyadicIndexEquiv line 606
  46. theorem OAI.CompletedGauss.tsum_dualIdealDyads line 624