OAI/NumberTheory/Catalan/SecondBarrier/BarrierCaseTwoYRootSimplicity.lean

GitHub source file

68 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InternalCatalan.barrier_case2_AY_transform3_coeff_rat_20 line 21
2. theorem OAI.InternalCatalan.barrier_case2_AY_transform3_coeff_rat_21 line 25
3. theorem OAI.InternalCatalan.barrier_case2_AY_transform3_coeff_rat_22 line 29
4. theorem OAI.InternalCatalan.barrier_case2_AY_transform3_coeff_rat_23 line 33
5. theorem OAI.InternalCatalan.barrier_case2_AY_transform3_coeff_rat_24 line 37
6. theorem OAI.InternalCatalan.barrier_case2_AY_transform3_explicit_coeff_20 line 41
7. theorem OAI.InternalCatalan.barrier_case2_AY_transform3_explicit_coeff_21 line 49
8. theorem OAI.InternalCatalan.barrier_case2_AY_transform3_explicit_coeff_22 line 57
9. theorem OAI.InternalCatalan.barrier_case2_AY_transform3_explicit_coeff_23 line 65
10. theorem OAI.InternalCatalan.barrier_case2_AY_transform3_explicit_coeff_24 line 73
11. theorem OAI.InternalCatalan.barrierCase2AY_transform3_all_coeff_rat line 81
12. theorem OAI.InternalCatalan.barrierCase2AYTransform3Explicit_coeff line 114
13. theorem OAI.InternalCatalan.barrierCase2AY_transform3_eq_explicit line 144
14. theorem OAI.InternalCatalan.barrierCase2AY_transform3_signVariations line 166
15. theorem OAI.InternalCatalan.barrierCase2AY_transform3_positive_roots_le line 178
16. theorem OAI.InternalCatalan.barrierCase2AY_bracket_sign_03 line 189
17. theorem OAI.InternalCatalan.barrierCase2AY_bracket_sign_04 line 196
18. theorem OAI.InternalCatalan.barrierCase2AY_bracket_sign_05 line 203
19. theorem OAI.InternalCatalan.barrierCase2AY_bracket_sign_06 line 210
20. theorem OAI.InternalCatalan.barrierCase2AY_bracket_sign_07 line 217
21. theorem OAI.InternalCatalan.barrierCase2AY_bracket_sign_08 line 224
22. theorem OAI.InternalCatalan.barrierCase2AY_bracket_sign_09 line 231
23. theorem OAI.InternalCatalan.barrierCase2AY_bracket_sign_10 line 238
24. theorem OAI.InternalCatalan.barrierCase2AY_bracket_sign_11 line 245
25. theorem OAI.InternalCatalan.barrierCase2AY_bracket_sign_12 line 252
26. theorem OAI.InternalCatalan.barrierCase2AY_bracket_sign_13 line 259
27. theorem OAI.InternalCatalan.barrierCase2AY_bracket_sign_14 line 266
28. def OAI.InternalCatalan.barrierCase2XBrackets line 275
29. theorem OAI.InternalCatalan.barrierCase2AX_bracket_signs line 283
30. theorem OAI.InternalCatalan.barrierCase2X_bracket_domain line 308
31. def OAI.InternalCatalan.barrierCase2YBrackets line 318
32. theorem OAI.InternalCatalan.barrierCase2AY_bracket_signs line 325
33. theorem OAI.InternalCatalan.barrierCase2Y_bracket_domain line 347
34. theorem OAI.InternalCatalan.barrierCase2AX_bracket_root line 358
35. theorem OAI.InternalCatalan.barrierCase2AY_bracket_root line 365
36. theorem OAI.InternalCatalan.barrierCase2AY_mapped_natDegree_le line 374
37. theorem OAI.InternalCatalan.barrierCase2AY_interval0_roots_card_le line 380
38. theorem OAI.InternalCatalan.barrierCase2AY_interval1_roots_card_le line 395
39. theorem OAI.InternalCatalan.barrierCase2AY_interval2_roots_card_le line 410
40. theorem OAI.InternalCatalan.barrierCase2AY_interval3_roots_card_le line 425
41. theorem OAI.InternalCatalan.barrierCase2AY_map_eval_rat_ne_zero line 440
42. theorem OAI.InternalCatalan.barrierCase2AY_root_subdivision line 451
43. theorem OAI.InternalCatalan.barrierCase2AY_interval_roots_card_le line 482
44. theorem OAI.InternalCatalan.barrierCase2Y_bracket_subset_interval line 530
45. theorem OAI.InternalCatalan.barrierCase2Y_bracket_separation line 539
46. theorem OAI.InternalCatalan.barrierBracketRight_le_left_of_separated line 543
47. theorem OAI.InternalCatalan.barrierCase2Y_brackets_disjoint line 552
48. def OAI.InternalCatalan.barrierCase2YChosenRoot line 564
49. theorem OAI.InternalCatalan.barrierCase2YChosenRoot_spec line 569
50. def OAI.InternalCatalan.barrierCase2YChosenRoots line 577
51. theorem OAI.InternalCatalan.barrierCase2YChosenRoots_card line 581
52. theorem OAI.InternalCatalan.barrierCase2YChosenRoots_spec line 596
53. theorem OAI.InternalCatalan.barrierCase2AY_root_mem_chosen line 606
54. theorem OAI.InternalCatalan.barrierCase2AY_roots_exhausted line 621
55. theorem OAI.InternalCatalan.barrierCase2AY_unique_root_in_bracket line 633
56. theorem OAI.InternalCatalan.barrierCase2AY_simple_mapped_natDegree_le line 653
57. theorem OAI.InternalCatalan.barrierCase2AY_simple_interval line 659
58. theorem OAI.InternalCatalan.barrierCase2AY_simple_interval0 line 682
59. theorem OAI.InternalCatalan.barrierCase2AY_simple_interval1 line 693
60. theorem OAI.InternalCatalan.barrierCase2AY_simple_interval2 line 704
61. theorem OAI.InternalCatalan.barrierCase2AY_simple_interval3 line 715
62. theorem OAI.InternalCatalan.barrierCase2AY_simple_map_eval_rat_ne_zero line 726
63. theorem OAI.InternalCatalan.barrierCase2AY_simple_root_subdivision line 737
64. theorem OAI.InternalCatalan.barrierCase2AY_rootMultiplicity_eq_one line 768
65. theorem OAI.InternalCatalan.barrierCase2AY_derivative_ne_zero_at_root line 778
66. theorem OAI.InternalCatalan.barrierCase2Y_simple_bracket_subset_interval line 790
67. theorem OAI.InternalCatalan.barrierCase2AY_simple_root_in_bracket line 799
68. theorem OAI.InternalCatalan.barrierCase2AY_unique_simple_root_in_bracket line 809