OAI/NumberTheory/DirichletL/Moments/FirstDiscardedEnergy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.CenteredMomentFirstDiscardedEnergy.tripleRow_norm_le_one line 16
  2. theorem OAI.SevenEighths.CenteredMomentFirstDiscardedEnergy.tripleFourier_norm_le_full line 30
  3. theorem OAI.SevenEighths.CenteredMomentFirstDiscardedEnergy.activeFunction_norm_le_one line 48
  4. theorem OAI.SevenEighths.CenteredMomentFirstDiscardedEnergy.scaled_discarded_triple_bound line 59
  5. def OAI.SevenEighths.CenteredMomentFirstDiscardedEnergy.canonicalDiscardedTerm line 86
  6. theorem OAI.SevenEighths.CenteredMomentFirstDiscardedEnergy.canonical_kernel_scale line 103
  7. theorem OAI.SevenEighths.CenteredMomentFirstDiscardedEnergy.canonical_discarded_term_bound line 117
  8. def OAI.SevenEighths.CenteredMomentFirstDiscardedEnergy.inactiveSubsets line 166
  9. theorem OAI.SevenEighths.CenteredMomentFirstDiscardedEnergy.inactiveSubsets_card line 169
  10. def OAI.SevenEighths.CenteredMomentFirstDiscardedEnergy.canonicalDiscardedPair line 178
  11. theorem OAI.SevenEighths.CenteredMomentFirstDiscardedEnergy.canonical_discarded_pair_bound line 183