OAI/NumberTheory/DirichletL/Moments/FirstAmplificationChoice.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.ballProfile line 25
  2. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.ballProfile_nonneg line 27
  3. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.ballProfile_le_one line 31
  4. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.ballProfile_one line 35
  5. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.ballProfile_majorizes line 39
  6. def OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.primeTest line 47
  7. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.primeTest_support line 53
  8. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.primeTest_tsupport line 60
  9. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.primeTest_ne_zero line 68
  10. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.eventually_log_card_power line 76
  11. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.eventually_actual_pool_card line 105
  12. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.eventually_actual_pool line 117
  13. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.reciprocal_pool_bound line 156
  14. def OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.dyadRows line 166
  15. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.mem_dyadRows line 170
  16. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.dyadRows_ne_zero line 181
  17. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.dyadRows_norm_lt line 187
  18. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.dyadRows_log_nonneg line 191
  19. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.dyadic_energy_eq_sum line 197
  20. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.dyadic_energy_le_sum line 207
  21. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.dyadic_energy_empty line 214
  22. def OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.mainGain line 218
  23. def OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.errorRemoval line 220
  24. def OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.errorMoving line 223
  25. def OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.errorGain line 226
  26. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.mainGain_bounds line 229
  27. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.errorGain_bounds line 236
  28. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.error_lengths line 248
  29. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.dyadRows_norm_power line 259
  30. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.dyad_ball_majorant line 265
  31. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.amplified_ball_majorant line 272
  32. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.gaussEnergy_ball_nonneg line 284
  33. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.errorEnergy_nonneg line 291
  34. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.eligible_error_sum line 297
  35. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.dyadic_to_ball line 306
  36. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.dyadic_amplification_to_ball line 318
  37. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.eventually_dyadic_amplification line 376
  38. structure OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.OriginalData line 419
  39. def OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.OriginalData.profile line 438
  40. def OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.OriginalData.columns line 442
  41. def OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.OriginalData.beta line 445
  42. def OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.OriginalData.coefficient line 448
  43. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.OriginalData.coefficient_eq line 452
  44. def OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.OriginalData.childEnergy line 456
  45. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.OriginalData.childEnergy_nonneg line 470
  46. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.exists_original_error_ball_family line 480
  47. def OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.errorIndex line 522
  48. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.errorIndex_cases line 524
  49. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.exists_pool_error_families line 527
  50. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.original_slot_coprime line 562
  51. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.eventually_original_source_amplification line 578
  52. def OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.OriginalData.active line 631
  53. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.OriginalData.active_subset line 636
  54. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.OriginalData.active_profile line 641
  55. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.OriginalData.active_slot line 643
  56. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.OriginalData.active_profile_zero line 647
  57. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.OriginalData.active_beta line 664
  58. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.OriginalData.active_columns_subset line 676
  59. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.OriginalData.active_gaussPolynomial line 679
  60. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.OriginalData.active_gaussEnergy line 701
  61. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.eventually_original_amplification line 712
  62. def OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.nominalLog line 759
  63. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.retained_nominal_choice line 762
  64. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.canonical_active_log_le line 779
  65. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.retained_main_first_saving line 796
  66. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.pool_prime_log_range line 826
  67. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.errorRemoval_power line 842
  68. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.errorMoving_power line 848
  69. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.shortened_raw_exact line 862
  70. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.eventually_frequency_loss line 867
  71. theorem OAI.SevenEighths.CenteredMomentFirstAmplificationChoice.retained_error_first_saving line 879