OAI/NumberTheory/Catalan/Energy/BarrierFinitePotentialRat.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.InternalCatalan.barrierTail_norm_le line 24
  2. theorem OAI.InternalCatalan.barrierTrial_abs_le line 50
  3. theorem OAI.InternalCatalan.barrier_trials_abs_le line 72
  4. theorem OAI.InternalCatalan.barrier_trials_abs_summable line 99
  5. def OAI.InternalCatalan.barrierTrialNormSq line 109
  6. theorem OAI.InternalCatalan.summable_barrier_weighted_square line 112
  7. theorem OAI.InternalCatalan.barrier_trials_norm_summable line 133
  8. theorem OAI.InternalCatalan.barrierTrialNormSq_nonneg line 147
  9. def OAI.InternalCatalan.barrierTrialT line 153
  10. def OAI.InternalCatalan.barrierTrialS line 157
  11. theorem OAI.InternalCatalan.barrierTrialT_term_norm_le line 160
  12. theorem OAI.InternalCatalan.barrierTrialS_term_norm_le line 175
  13. theorem OAI.InternalCatalan.barrierTrialT_summable line 189
  14. theorem OAI.InternalCatalan.barrierTrialS_summable line 196
  15. theorem OAI.InternalCatalan.barrierTrialT_tendstoUniformlyOn line 202
  16. theorem OAI.InternalCatalan.barrierTrialS_tendstoUniformlyOn line 213
  17. theorem OAI.InternalCatalan.barrier_trials_potentials_uniform line 224
  18. theorem OAI.InternalCatalan.barrierTrialNormSq_nil_eq_sum line 249
  19. theorem OAI.InternalCatalan.barrier_case1_norm_sharp_upper line 264
  20. theorem OAI.InternalCatalan.barrier_case1_norm_coarse_upper line 272
  21. theorem OAI.InternalCatalan.barrierTrialNormSq_le_prefix_add_geometric_tail line 277
  22. theorem OAI.InternalCatalan.barrierTrialT_nil_eq_sum line 328
  23. theorem OAI.InternalCatalan.barrierTrialS_nil_eq_sum line 344
  24. theorem OAI.InternalCatalan.barrierTrialT_continuousOn line 366
  25. theorem OAI.InternalCatalan.barrierTrialS_continuousOn line 379
  26. theorem OAI.InternalCatalan.barrier_Tseries_term_hasDerivAt line 394
  27. theorem OAI.InternalCatalan.barrier_Sseries_term_hasDerivAt line 410
  28. theorem OAI.InternalCatalan.barrierTrialT_hasDerivAt_series line 420
  29. theorem OAI.InternalCatalan.barrierTrialS_hasDerivAt_series line 442
  30. theorem OAI.InternalCatalan.barrier_weighted_abs_summable_of_decay line 460
  31. theorem OAI.InternalCatalan.barrier_trials_weighted_abs_summable line 475
  32. def OAI.InternalCatalan.barrierFiniteTRat line 488
  33. def OAI.InternalCatalan.barrierFiniteSRat line 492
  34. theorem OAI.InternalCatalan.barrierTrialT_nil_eval_rat line 496
  35. theorem OAI.InternalCatalan.barrierTrialS_nil_eval_rat line 511