OAI/NumberTheory/DirichletL/Energy/FirstLiveAdmission.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SevenEighths.CenteredMomentEnergyFirstLiveAdmission.first_block_active_rows_nonempty line 38
  2. theorem OAI.SevenEighths.CenteredMomentEnergyFirstLiveAdmission.original_both_columns line 53
  3. def OAI.SevenEighths.CenteredMomentEnergyFirstLiveAdmission.columnIdeal line 74
  4. def OAI.SevenEighths.CenteredMomentEnergyFirstLiveAdmission.oppositeIdeal line 76
  5. def OAI.SevenEighths.CenteredMomentEnergyFirstLiveAdmission.columnMainRadius line 78
  6. def OAI.SevenEighths.CenteredMomentEnergyFirstLiveAdmission.columnErrorRadius line 85
  7. lemma OAI.SevenEighths.CenteredMomentEnergyFirstLiveAdmission.columnMainRadius_left line 92
  8. lemma OAI.SevenEighths.CenteredMomentEnergyFirstLiveAdmission.columnErrorRadius_left line 96
  9. def OAI.SevenEighths.CenteredMomentEnergyFirstLiveAdmission.readyBudget line 101
  10. lemma OAI.SevenEighths.CenteredMomentEnergyFirstLiveAdmission.readyBudget_nonneg line 103
  11. lemma OAI.SevenEighths.CenteredMomentEnergyFirstLiveAdmission.common_exponent_le line 106
  12. lemma OAI.SevenEighths.CenteredMomentEnergyFirstLiveAdmission.error_exponent_le line 111
  13. lemma OAI.SevenEighths.CenteredMomentEnergyFirstLiveAdmission.ready_mono line 117
  14. lemma OAI.SevenEighths.CenteredMomentEnergyFirstLiveAdmission.lower_profile_zero line 125
  15. theorem OAI.SevenEighths.CenteredMomentEnergyFirstLiveAdmission.main_lower_support line 130
  16. theorem OAI.SevenEighths.CenteredMomentEnergyFirstLiveAdmission.error_lower_support line 141
  17. theorem OAI.SevenEighths.CenteredMomentEnergyFirstLiveAdmission.eventual_parent_radius line 156
  18. theorem OAI.SevenEighths.CenteredMomentEnergyFirstLiveAdmission.eventually_main_packet line 176
  19. theorem OAI.SevenEighths.CenteredMomentEnergyFirstLiveAdmission.eventually_error_packet line 255