OAI/NumberTheory/Catalan/Estimates/RealEnergyTrialDamping.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.realEnergyTrialTau line 12
  2. def OAI.InternalCatalan.realEnergyTrialRho line 16
  3. def OAI.InternalCatalan.realEnergyTrialSigma line 20
  4. theorem OAI.InternalCatalan.energy_one_sub_pow_le line 24
  5. theorem OAI.InternalCatalan.energy_trial_term_norm_le line 34
  6. theorem OAI.InternalCatalan.energy_trial_damping_term_norm_le line 47
  7. theorem OAI.InternalCatalan.energy_damped_trial_summable line 68
  8. theorem OAI.InternalCatalan.energy_damped_trial_sub_le line 84
  9. theorem OAI.InternalCatalan.realEnergyTrialTau_summable line 109
  10. theorem OAI.InternalCatalan.realEnergyTrialRho_summable line 119
  11. theorem OAI.InternalCatalan.realEnergyTrialSigma_summable line 129
  12. theorem OAI.InternalCatalan.realEnergyTrialTau_sub_le line 140
  13. theorem OAI.InternalCatalan.realEnergyTrialRho_sub_le line 153
  14. theorem OAI.InternalCatalan.realEnergyTrialSigma_sub_le line 168