OAI/NumberTheory/DirichletL/Mellin/CompactWeights.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.CompactScaleBridge.outsideCoeff_baseChange_zero line 56
  2. theorem OAI.CompactScaleBridge.outsideCoeff_compact_hasSum line 76
  3. theorem OAI.CompactScaleBridge.realCompactOutsideSum_eq_outsideCompactSum line 118
  4. theorem OAI.CompactScaleBridge.zero_free_of_fixedTestPrimeMSConstants line 128
  5. def OAI.ConcreteCompactWeight.bumpData line 169
  6. def OAI.ConcreteCompactWeight.bump line 172
  7. theorem OAI.ConcreteCompactWeight.bump_smooth line 174
  8. theorem OAI.ConcreteCompactWeight.bump_nonneg line 178
  9. theorem OAI.ConcreteCompactWeight.bump_one line 180
  10. theorem OAI.ConcreteCompactWeight.bump_support line 186
  11. theorem OAI.ConcreteCompactWeight.bump_compact line 197
  12. def OAI.ConcreteCompactWeight.positiveExtension line 199
  13. theorem OAI.ConcreteCompactWeight.positiveExtension_smooth line 202
  14. theorem OAI.ConcreteCompactWeight.positiveExtension_pos line 209
  15. theorem OAI.ConcreteCompactWeight.positiveExtension_eq line 225
  16. def OAI.ConcreteCompactWeight.weight line 231
  17. theorem OAI.ConcreteCompactWeight.weight_smooth line 234
  18. theorem OAI.ConcreteCompactWeight.weight_support line 249
  19. theorem OAI.ConcreteCompactWeight.weight_eq_cpow line 253
  20. theorem OAI.ConcreteCompactWeight.weight_mellin_eq_bump line 264
  21. def OAI.ConcreteCompactWeight.weightedBump line 283
  22. theorem OAI.ConcreteCompactWeight.weightedBump_continuous line 286
  23. theorem OAI.ConcreteCompactWeight.weightedBump_compact line 290
  24. theorem OAI.ConcreteCompactWeight.weightedBump_nonneg line 294
  25. theorem OAI.ConcreteCompactWeight.weightedBump_nonzero line 297
  26. theorem OAI.ConcreteCompactWeight.weightedBump_integral_pos line 300
  27. theorem OAI.ConcreteCompactWeight.weightedBump_eq_zero_of_nonpos line 306
  28. theorem OAI.ConcreteCompactWeight.mellin_bump_zero_eq_integral_weightedBump line 310
  29. theorem OAI.ConcreteCompactWeight.weight_mellin_ne_zero line 330
  30. theorem OAI.ConcreteCompactWeight.weight_norm_le_one line 334
  31. theorem OAI.CompactScaleBridge.zero_free_of_fixedTestPrimeMSConstants_concrete line 361
  32. theorem OAI.CompactScaleBridge.dirichletTarget_of_fixedTestPrimeMSConstants_concrete line 385
  33. theorem OAI.ActualEisensteinCubic.A3_unramified_fixed_denominator_local_character line 415
  34. theorem OAI.TwoPassProfiles.first_poisson_profile line 433
  35. theorem OAI.TwoPassProfiles.second_poisson_profile line 443
  36. theorem OAI.TwoPassProfiles.child_column_profile line 451
  37. theorem OAI.TwoPassProfiles.first_profile_logshape line 457
  38. theorem OAI.TwoPassProfiles.second_profile_logshape line 478
  39. def OAI.TwoPassProfiles.firstCoeff line 497
  40. def OAI.TwoPassProfiles.firstLogs line 501
  41. theorem OAI.TwoPassProfiles.first_logsum line 506
  42. def OAI.TwoPassProfiles.secondCoeff line 515
  43. def OAI.TwoPassProfiles.secondLogs line 519
  44. theorem OAI.TwoPassProfiles.second_logsum line 524
  45. theorem OAI.TwoPassProfiles.first_profile_exp line 533
  46. theorem OAI.TwoPassProfiles.second_profile_exp line 545
  47. theorem OAI.TwoPassProfiles.first_dyadic_profile line 557
  48. theorem OAI.TwoPassProfiles.second_dyadic_profile line 577