OAI/NumberTheory/DirichletL/Energy/NaturalInputMatches.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentEnergyNaturalInputMatches.profile line 16
  2. lemma OAI.SevenEighths.CenteredMomentEnergyNaturalInputMatches.profile_support line 19
  3. lemma OAI.SevenEighths.CenteredMomentEnergyNaturalInputMatches.profile_zero line 27
  4. lemma OAI.SevenEighths.CenteredMomentEnergyNaturalInputMatches.profile_norm line 33
  5. theorem OAI.SevenEighths.CenteredMomentEnergyNaturalInputMatches.exists_profile_bound line 42
  6. def OAI.SevenEighths.CenteredMomentEnergyNaturalInputMatches.profileBound line 56
  7. lemma OAI.SevenEighths.CenteredMomentEnergyNaturalInputMatches.profileBound_ge_one line 61
  8. lemma OAI.SevenEighths.CenteredMomentEnergyNaturalInputMatches.norm_profile_le line 67
  9. def OAI.SevenEighths.CenteredMomentEnergyNaturalInputMatches.input line 89
  10. theorem OAI.SevenEighths.CenteredMomentEnergyNaturalInputMatches.input_matches line 105
  11. lemma OAI.SevenEighths.CenteredMomentEnergyNaturalInputMatches.lower_eq line 109
  12. lemma OAI.SevenEighths.CenteredMomentEnergyNaturalInputMatches.upper_eq line 110
  13. lemma OAI.SevenEighths.CenteredMomentEnergyNaturalInputMatches.slot_control_eq line 111
  14. lemma OAI.SevenEighths.CenteredMomentEnergyNaturalInputMatches.character_eq line 113
  15. lemma OAI.SevenEighths.CenteredMomentEnergyNaturalInputMatches.mask_eq line 114
  16. lemma OAI.SevenEighths.CenteredMomentEnergyNaturalInputMatches.height_eq line 115
  17. lemma OAI.SevenEighths.CenteredMomentEnergyNaturalInputMatches.first_rectangle_eq line 116
  18. lemma OAI.SevenEighths.CenteredMomentEnergyNaturalInputMatches.second_rectangle_eq line 117
  19. theorem OAI.SevenEighths.CenteredMomentEnergyNaturalInputMatches.coefficient_eq line 119
  20. theorem OAI.SevenEighths.CenteredMomentEnergyNaturalInputMatches.positive_row_eq line 124
  21. theorem OAI.SevenEighths.CenteredMomentEnergyNaturalInputMatches.energy_eq line 133
  22. theorem OAI.SevenEighths.CenteredMomentEnergyNaturalInputMatches.reference_energy_eq line 144