OAI/NumberTheory/DirichletL/Energy/NaturalSourceAdmission.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentEnergyNaturalSourceAdmission.lowerProduct line 25
  2. lemma OAI.SevenEighths.CenteredMomentEnergyNaturalSourceAdmission.lowerProduct_pos line 27
  3. theorem OAI.SevenEighths.CenteredMomentEnergyNaturalSourceAdmission.both_matches line 45
  4. lemma OAI.SevenEighths.CenteredMomentEnergyNaturalSourceAdmission.source_fields line 50
  5. lemma OAI.SevenEighths.CenteredMomentEnergyNaturalSourceAdmission.slot_fields line 59
  6. lemma OAI.SevenEighths.CenteredMomentEnergyNaturalSourceAdmission.slot_coefficient line 67
  7. lemma OAI.SevenEighths.CenteredMomentEnergyNaturalSourceAdmission.rectangles line 72
  8. lemma OAI.SevenEighths.CenteredMomentEnergyNaturalSourceAdmission.raw_volume line 80
  9. lemma OAI.SevenEighths.CenteredMomentEnergyNaturalSourceAdmission.volume_log line 82
  10. theorem OAI.SevenEighths.CenteredMomentEnergyNaturalSourceAdmission.capacity_admission line 91
  11. theorem OAI.SevenEighths.CenteredMomentEnergyNaturalSourceAdmission.low_admission line 102
  12. theorem OAI.SevenEighths.CenteredMomentEnergyNaturalSourceAdmission.lower_product_admission line 112
  13. theorem OAI.SevenEighths.CenteredMomentEnergyNaturalSourceAdmission.profile_control_admission line 120
  14. theorem OAI.SevenEighths.CenteredMomentEnergyNaturalSourceAdmission.normalized_zero_source line 132
  15. theorem OAI.SevenEighths.CenteredMomentEnergyNaturalSourceAdmission.radial_admission line 153
  16. theorem OAI.SevenEighths.CenteredMomentEnergyNaturalSourceAdmission.original_scale_caps line 162
  17. theorem OAI.SevenEighths.CenteredMomentEnergyNaturalSourceAdmission.eventually_scale_admission line 177