OAI/NumberTheory/DirichletL/Moments/SectorLocalization.lean

GitHub source file

80 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentSectorLocalization.cutoff line 13
  2. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.cutoff_one line 15
  3. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.cutoff_zero line 18
  4. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.cutoff_bounds line 21
  5. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.cutoff_antitone line 24
  6. def OAI.SevenEighths.CenteredMomentSectorLocalization.annulus line 28
  7. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.annulus_zero_low line 30
  8. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.annulus_zero_high line 33
  9. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.annulus_bounds line 36
  10. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.annulus_smooth line 45
  11. def OAI.SevenEighths.CenteredMomentSectorLocalization.dyadicScale line 50
  12. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.dyadicScale_pos line 52
  13. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.dyadicScale_add line 56
  14. def OAI.SevenEighths.CenteredMomentSectorLocalization.dyadicWeight line 60
  15. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.dyadicWeight_smooth line 62
  16. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.dyadicWeight_bounds line 65
  17. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.dyadicWeight_zero_low line 68
  18. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.dyadicWeight_zero_high line 74
  19. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.dyadicWeight_support line 79
  20. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.dyadicWeight_tsupport line 86
  21. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.dyadicWeight_outside_pair line 90
  22. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.dyadicWeight_finite line 107
  23. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.dyadicWeight_summable line 118
  24. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.dyadicWeight_partition line 121
  25. def OAI.SevenEighths.CenteredMomentSectorLocalization.Retained line 141
  26. def OAI.SevenEighths.CenteredMomentSectorLocalization.retainedWeight line 144
  27. def OAI.SevenEighths.CenteredMomentSectorLocalization.discardedWeight line 146
  28. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.retained_summable line 148
  29. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.discarded_summable line 152
  30. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.retained_add_discarded line 159
  31. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.dyadicWeight_zero_nonpos line 167
  32. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.retainedWeight_zero_nonpos line 170
  33. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.discardedWeight_zero_nonpos line 173
  34. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.retainedWeight_nonneg line 176
  35. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.discardedWeight_nonneg line 183
  36. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.retainedWeight_bounds line 190
  37. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.discardedWeight_bounds line 198
  38. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.retained_scale_le line 206
  39. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.retainedWeight_zero_above line 211
  40. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.retainedWeight_enclosure line 221
  41. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.discardedWeight_zero_below line 226
  42. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.discardedWeight_support line 239
  43. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.retainedWeight_one_below line 242
  44. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.finite_retained_integral_dyads line 246
  45. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.annulus_pos line 263
  46. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.dyadicWeight_support_eq line 271
  47. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.dyadicWeight_tsupport_eq line 281
  48. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.retained_iff_scale line 286
  49. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.retained_boundary line 292
  50. def OAI.SevenEighths.CenteredMomentSectorLocalization.normValue line 296
  51. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.normValue_eq_embedding line 298
  52. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.normValue_mul line 301
  53. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.normValue_pos line 304
  54. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.normValue_ge_one line 309
  55. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.retained_pullback line 314
  56. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.retained_norm_enclosure line 318
  57. def OAI.SevenEighths.CenteredMomentSectorLocalization.frequencyRadius line 325
  58. def OAI.SevenEighths.CenteredMomentSectorLocalization.frequencyLoss line 327
  59. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.frequencyLoss_nonneg line 329
  60. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.source_enclosure_power line 335
  61. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.actual_retained_row_enclosure line 346
  62. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.actual_nonempty_width line 358
  63. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.actual_declared_width_drop line 368
  64. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.retained_first_dyad_enclosure line 379
  65. def OAI.SevenEighths.CenteredMomentSectorLocalization.kernelReference line 393
  66. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.kernelReference_pos line 395
  67. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.frequencyLoss_lt line 398
  68. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.discarded_kernel_argument line 405
  69. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.retained_pullback_zero_extension line 426
  70. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.actual_discarded_lattice_tail line 437
  71. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.actual_discarded_second_tail line 471
  72. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.actual_discarded_first_tail line 490
  73. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.retained_product_ne_zero line 528
  74. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.actual_nonempty_width_of_weight line 533
  75. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.actual_second_pullback line 540
  76. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.retained_integral_empty line 545
  77. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.finite_retained_above line 555
  78. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.retainedWeight_finite_formula line 571
  79. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.retainedWeight_smooth_positive line 583
  80. theorem OAI.SevenEighths.CenteredMomentSectorLocalization.discardedWeight_smooth_positive line 596