OAI/NumberTheory/DirichletL/Energy/ZeroReflectionSupport.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SevenEighths.CenteredMomentEnergyZeroReflectionSupport.naturalDualScale line 22
  2. lemma OAI.SevenEighths.CenteredMomentEnergyZeroReflectionSupport.naturalDualScale_pos line 26
  3. theorem OAI.SevenEighths.CenteredMomentEnergyZeroReflectionSupport.eventually_natural_choice_range line 38
  4. theorem OAI.SevenEighths.CenteredMomentEnergyZeroReflectionSupport.eventually_natural_source_zero line 54
  5. lemma OAI.SevenEighths.CenteredMomentEnergyZeroReflectionSupport.deleted_short_length line 120
  6. theorem OAI.SevenEighths.CenteredMomentEnergyZeroReflectionSupport.live_deleted_growth line 137
  7. theorem OAI.SevenEighths.CenteredMomentEnergyZeroReflectionSupport.eventually_endpoint_defect line 151
  8. theorem OAI.SevenEighths.CenteredMomentEnergyZeroReflectionSupport.actual_deleted_growth line 161
  9. theorem OAI.SevenEighths.CenteredMomentEnergyZeroReflectionSupport.eventually_actual_source_zero line 175
  10. theorem OAI.SevenEighths.CenteredMomentEnergyZeroReflectionSupport.eventually_actual_deleted_growth line 199
  11. theorem OAI.SevenEighths.CenteredMomentEnergyZeroReflectionSupport.eventually_actual_retained_deleted_growth line 217