OAI/NumberTheory/Catalan/Estimates/RealEnergyDampedDual.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.InternalCatalan.realEnergyCosineMoment line 16
  2. def OAI.InternalCatalan.realEnergyPowerMoment line 19
  3. def OAI.InternalCatalan.realEnergyColumnMoment line 22
  4. theorem OAI.InternalCatalan.energy_sum_sum_mul_div line 26
  5. theorem OAI.InternalCatalan.energy_cosineMoment_square_div_eq line 38
  6. theorem OAI.InternalCatalan.energy_hasSum_first_square line 51
  7. theorem OAI.InternalCatalan.energy_summable_abs_first_square line 88
  8. theorem OAI.InternalCatalan.energy_abs_average_le_one line 101
  9. theorem OAI.InternalCatalan.energy_cosineMoment_abs_le_one line 112
  10. theorem OAI.InternalCatalan.energy_powerMoment_abs_le_one line 125
  11. theorem OAI.InternalCatalan.energy_columnMoment_abs_le_one line 138
  12. theorem OAI.InternalCatalan.energy_secondMoment_abs_le_three line 151
  13. theorem OAI.InternalCatalan.energy_trial_norm_summable line 165
  14. theorem OAI.InternalCatalan.energy_trial_product_summable line 180
  15. theorem OAI.InternalCatalan.realEnergy_damped_node_mem line 203
  16. theorem OAI.InternalCatalan.energy_hasSum_power_square line 209
  17. theorem OAI.InternalCatalan.energy_hasSum_column_square line 240
  18. theorem OAI.InternalCatalan.energy_hasSum_mixed_moments line 288
  19. theorem OAI.InternalCatalan.energy_hasSum_second_square line 339
  20. theorem OAI.InternalCatalan.energy_hasSum_trialTau_average line 365
  21. theorem OAI.InternalCatalan.energy_hasSum_trialRho_average line 387
  22. theorem OAI.InternalCatalan.energy_hasSum_trialSigma_average line 409
  23. theorem OAI.InternalCatalan.energy_tsum_trialTau_average line 431
  24. theorem OAI.InternalCatalan.energy_tsum_trialRho_average line 440
  25. theorem OAI.InternalCatalan.energy_tsum_trialSigma_average line 449
  26. theorem OAI.InternalCatalan.energy_tangent_of_hasSum line 463
  27. theorem OAI.InternalCatalan.realEnergy_first_tangent line 478
  28. theorem OAI.InternalCatalan.realEnergy_second_tangent line 500
  29. def OAI.InternalCatalan.realEnergyDampedInteraction line 558
  30. theorem OAI.InternalCatalan.realEnergyDampedInteraction_eq_squares line 572
  31. theorem OAI.InternalCatalan.realEnergyDampedInteraction_le_trials line 585
  32. theorem OAI.InternalCatalan.energy_average_le_of_le_add line 606
  33. theorem OAI.InternalCatalan.realEnergyDampedInteraction_le_trialAverages line 618
  34. theorem OAI.InternalCatalan.realEnergyDampedInteraction_le_canonicalTrials line 635