OAI/NumberTheory/Catalan/FirstBarrier/BarrierCaseOneGlobalBounds.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InternalCatalan.barrierCase1AX_transform1_signVariations line 14
2. theorem OAI.InternalCatalan.barrierCase1AX_transform1_positive_roots_le line 25
3. theorem OAI.InternalCatalan.barrierCase1AX_transform2_signVariations line 40
4. theorem OAI.InternalCatalan.barrierCase1AX_transform2_positive_roots_le line 51
5. theorem OAI.InternalCatalan.barrierCase1AX_transform3_signVariations line 66
6. theorem OAI.InternalCatalan.barrierCase1AX_transform3_positive_roots_le line 77
7. theorem OAI.InternalCatalan.barrierCase1AX_mapped_natDegree_le line 95
8. theorem OAI.InternalCatalan.barrierCase1AX_interval0_roots_card_le line 101
9. theorem OAI.InternalCatalan.barrierCase1AX_interval1_roots_card_le line 116
10. theorem OAI.InternalCatalan.barrierCase1AX_interval2_roots_card_le line 131
11. theorem OAI.InternalCatalan.barrierCase1AX_interval3_roots_card_le line 146
12. theorem OAI.InternalCatalan.barrierCase1AX_map_eval_rat_ne_zero line 161
13. theorem OAI.InternalCatalan.barrierCase1AX_root_subdivision line 172
14. theorem OAI.InternalCatalan.barrierCase1AX_domain_roots_card_le line 197
15. theorem OAI.InternalCatalan.barrierCase1X_bracket_subset_domain line 245
16. theorem OAI.InternalCatalan.barrierCase1X_brackets_disjoint line 258
17. def OAI.InternalCatalan.barrierCase1XChosenRoot line 273
18. theorem OAI.InternalCatalan.barrierCase1XChosenRoot_spec line 278
19. def OAI.InternalCatalan.barrierCase1XChosenRoots line 286
20. theorem OAI.InternalCatalan.barrierCase1XChosenRoots_card line 290
21. theorem OAI.InternalCatalan.barrierCase1XChosenRoots_spec line 305
22. theorem OAI.InternalCatalan.barrierCase1AX_root_mem_chosen line 315
23. theorem OAI.InternalCatalan.barrierCase1AX_roots_exhausted line 330
24. theorem OAI.InternalCatalan.barrierCase1AX_unique_root_in_bracket line 342
25. theorem OAI.InternalCatalan.barrierCase1X_le_of_bracket_bounds line 368
26. theorem OAI.InternalCatalan.barrierCase1Y_le_of_bracket_bounds line 394
27. theorem OAI.InternalCatalan.rootSimplicity_case1AX_degree_le line 421
28. theorem OAI.InternalCatalan.rootSimplicity_case1AX_interval0 line 425
29. theorem OAI.InternalCatalan.rootSimplicity_case1AX_interval1 line 451
30. theorem OAI.InternalCatalan.rootSimplicity_case1AX_interval2 line 477
31. theorem OAI.InternalCatalan.rootSimplicity_case1AX_interval3 line 503
32. theorem OAI.InternalCatalan.barrierCase1AX_rootMultiplicity_one line 529
33. theorem OAI.InternalCatalan.barrierCase1AY_rootMultiplicity_one line 552
34. theorem OAI.InternalCatalan.rootSimplicity_case1X_bracket_domain line 577
35. theorem OAI.InternalCatalan.rootSimplicity_case1Y_bracket_domain line 590
36. theorem OAI.InternalCatalan.barrierCase1AX_unique_simple_root_in_bracket line 599
37. theorem OAI.InternalCatalan.barrierCase1AY_unique_simple_root_in_bracket line 610
38. theorem OAI.InternalCatalan.barrierCase1AX_derivative_eval_ne_zero line 621
39. theorem OAI.InternalCatalan.barrierCase1X_stationary_numerator_simple line 634
40. theorem OAI.InternalCatalan.barrierCase1AY_derivative_eval_ne_zero line 648
41. theorem OAI.InternalCatalan.barrierCase1Y_stationary_numerator_simple line 661
42. theorem OAI.InternalCatalan.barrierCase1Y2_approx_upper line 678
43. theorem OAI.InternalCatalan.barrierCase1Y2_lt line 686
44. theorem OAI.InternalCatalan.barrierCase1Y3_approx_upper line 703
45. theorem OAI.InternalCatalan.barrierCase1Y3_lt line 711
46. theorem OAI.InternalCatalan.barrierCase1Y4_approx_upper line 728
47. theorem OAI.InternalCatalan.barrierCase1Y4_lt line 736
48. theorem OAI.InternalCatalan.barrierCase1X_bracket_left_lt line 752
49. theorem OAI.InternalCatalan.barrierCase1Y_bracket_left_lt line 767
50. theorem OAI.InternalCatalan.barrierCase1X_neg_one_lt line 783
51. theorem OAI.InternalCatalan.barrierCase1X_global_upper line 791
52. theorem OAI.InternalCatalan.barrierCase1Y_global_upper line 808