OAI/Combinatorics/HoneycombChords/Resolvents.lean

GitHub source file

97 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jacobiA line 15
2. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jacobiB line 16
3. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jacobiA_pos line 17
4. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jacobi_zero line 18
5. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jacobi_succ line 24
6. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jacobi_poly_zero line 37
7. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jacobi_poly_succ line 42
8. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.negativeEval line 48
9. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.negativeEval_pos line 49
10. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.negativeEval_zero line 51
11. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.negativeEval_jacobi_zero line 52
12. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.negativeEval_jacobi_succ line 60
13. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rational_sech_integrable line 78
14. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rationalSechMoment line 91
15. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rationalSechMoment_add line 93
16. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rationalSechMoment_smul line 98
17. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rationalSechMoment_neg line 103
18. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rationalSechMoment_sub line 106
19. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rationalSechMoment_sum line 109
20. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rationalSechMoment_den line 114
21. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rationalSechMoment_sq_nonneg line 123
22. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rationalSechMoment_zero_mul line 131
23. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rationalSechMoment_residual line 134
24. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.resolventCoeff line 144
25. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.resolventCoeff_bessel line 146
26. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.square_prefix_monotone line 166
27. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.antitone_ratio_nonneg line 171
28. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.antitone_ratio_zero line 200
29. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.wronskian_ratio_step line 234
30. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.wronskian_ratio_antitone line 243
31. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rationalSechMoment_X line 259
32. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rationalSechMoment_basis_zero line 265
33. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.resolventCoeff_jacobi_zero line 270
34. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.resolventCoeff_jacobi_succ line 278
35. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.signedResolventCoeff line 288
36. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.signedResolventCoeff_jacobi_zero line 289
37. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.signedResolventCoeff_jacobi_succ line 294
38. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.resolvent_wronskian line 300
39. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.signedResolventCoeff_sq line 313
40. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.signedResolventCoeff_bessel line 317
41. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.negativeEval_square_diverges line 324
42. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.signedResolventCoeff_ratio_zero line 334
43. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.signedResolventCoeff_pos line 339
44. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.poch_ratio_factor_tendsto line 357
45. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pochRatio_same_normalized_tendsto line 363
46. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.pochRatio_power_bounds line 373
47. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.reciprocalPoch line 382
48. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.reciprocalPoch_pos line 383
49. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.reciprocalPoch_step line 385
50. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.reciprocalPoch_normalized_tendsto line 395
51. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.reciprocalPoch_bounds line 403
52. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.reciprocalPoch_zero line 412
53. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.reciprocalPoch_difference_bounds line 420
54. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.difference_comparison line 443
55. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.negativeEval_power_bounds line 469
56. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.nat_power_shift_bounds line 483
57. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.jacobiA_power_bounds line 495
58. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.resolvent_denominator_bounds line 499
59. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.resolvent_ratio_difference_bounds line 527
60. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.resolvent_ratio_power_bounds line 539
61. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.signedResolventCoeff_power_bounds line 565
62. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.mixedWronskian line 592
63. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.mixedWronskian_sum line 594
64. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.mixedWronskian_power_bound line 608
65. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.mixedWronskian_zero line 642
66. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.resolventEvalResidual line 651
67. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.resolventEvalResidual_zero line 653
68. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.resolventEvalResidual_step line 664
69. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.resolventEvalResidual_power_bounds line 668
70. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.difference_lower_of_nonneg line 716
71. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.resolventNormResidual line 731
72. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.resolventNormResidual_nonneg line 733
73. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.resolventNormResidual_step line 738
74. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.resolventNormResidual_lower line 743
75. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.resolventNormResidual_pos line 764
76. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.resolventEvalResidual_normalized_bound line 768
77. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rationalSechMoment_den_twice line 786
78. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rationalSechMoment_combination line 790
79. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rational_combination_eval line 812
80. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.polynomial_linear_decomposition line 830
81. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rational_polynomial_evaluation_bound line 846
82. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rationalPolynomialChristoffel line 883
83. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rational_polynomial_ratio_bound line 885
84. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rationalPolynomialChristoffel_upper line 893
85. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rationalPolynomialChristoffel_bounds line 903
86. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sechWeight line 956
87. def OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rationalSechWeight line 957
88. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sechWeight_pos line 958
89. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rationalSechWeight_pos line 960
90. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.sechWeight_moments line 962
91. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rationalSechWeight_moments line 968
92. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weightedNorm_sech line 978
93. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weightedKernel_sech line 985
94. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weightedNorm_rationalSech line 988
95. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weightedNorm_rationalSech_scale line 996
96. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.rationalSechWeight_evaluation_bound line 1010
97. lemma OAI.CriticalHoneycomb.FiniteFunctional.StripAsymptotic.weightedKernel_rationalSech_upper line 1024