OAI/NumberTheory/Catalan/Estimates/BlaschkeUniformInterpolation.lean

GitHub source file

79 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InternalCatalan.imaginary_path_dist line 14
2. theorem OAI.InternalCatalan.upper_circle_crossing_location line 19
3. theorem OAI.InternalCatalan.upper_crossing_far_separation line 35
4. theorem OAI.InternalCatalan.upper_crossing_local_path line 44
5. theorem OAI.InternalCatalan.upper_crossing_endpoint_distances line 53
6. theorem OAI.InternalCatalan.imaginary_path_neg_distance line 77
7. theorem OAI.InternalCatalan.lower_circle_crossing_location line 84
8. theorem OAI.InternalCatalan.lower_crossing_far_separation line 96
9. theorem OAI.InternalCatalan.lower_crossing_local_path line 103
10. theorem OAI.InternalCatalan.lower_crossing_endpoint_distances line 111
11. def OAI.InternalCatalan.circleRightPerturb line 132
12. theorem OAI.InternalCatalan.circleRightPerturb_zero line 135
13. theorem OAI.InternalCatalan.circleRightPerturb_continuousAt_zero line 138
14. theorem OAI.InternalCatalan.circleRightPerturb_norm_and_re line 146
15. def OAI.InternalCatalan.polynomialDividedDifference line 177
16. theorem OAI.InternalCatalan.sub_mul_polynomialDividedDifference line 180
17. theorem OAI.InternalCatalan.polynomialDividedDifference_analyticAt_left line 193
18. theorem OAI.InternalCatalan.polynomialDividedDifference_analyticAt_right line 203
19. theorem OAI.InternalCatalan.polynomialEval_analyticAt line 213
20. def OAI.InternalCatalan.blaschkeDensityRemainder line 220
21. theorem OAI.InternalCatalan.blaschkeDensity_eq_add_remainder line 228
22. theorem OAI.InternalCatalan.blaschkeDensityRemainder_analyticAt_left line 253
23. theorem OAI.InternalCatalan.blaschkeDensityRemainder_analyticAt_right line 265
24. def OAI.InternalCatalan.blaschkeCauchyMoment line 286
25. def OAI.InternalCatalan.blaschkeIntegratedDividedDifference line 291
26. theorem OAI.InternalCatalan.continuous_nodePolynomial_imaginary line 296
27. theorem OAI.InternalCatalan.continuous_blaschkeCauchyMoment_integrand line 303
28. theorem OAI.InternalCatalan.intervalIntegrable_blaschkeCauchyMoment_integrand line 311
29. theorem OAI.InternalCatalan.intervalIntegrable_blaschkeDividedDifference_quotient line 317
30. theorem OAI.InternalCatalan.integral_blaschkeDividedDifference_quotient line 336
31. theorem OAI.InternalCatalan.blaschkeIntegratedDividedDifference_analyticAt line 365
32. def OAI.InternalCatalan.blaschkeCauchyRemainder line 387
33. theorem OAI.InternalCatalan.blaschkeDensityRemainder_eq_sub line 393
34. theorem OAI.InternalCatalan.remainder_path_eq line 406
35. theorem OAI.InternalCatalan.intervalIntegrable_blaschkeDensityRemainder line 420
36. theorem OAI.InternalCatalan.integral_blaschkeDensityRemainder line 429
37. theorem OAI.InternalCatalan.blaschkeCauchyRemainder_analyticAt line 443
38. theorem OAI.InternalCatalan.integral_blaschkeCauchyKernel_eq_scalar_add_remainder line 452
39. theorem OAI.InternalCatalan.complexLog_analyticAt line 483
40. theorem OAI.InternalCatalan.cauchyLogLeft_analyticAt line 489
41. theorem OAI.InternalCatalan.cauchyLogRight_analyticAt line 508
42. theorem OAI.InternalCatalan.blaschkeDensity_analyticAt_of_nodePolynomial_ne_zero line 528
43. def OAI.InternalCatalan.blaschkeCauchyLeft line 538
44. def OAI.InternalCatalan.blaschkeCauchyRight line 543
45. theorem OAI.InternalCatalan.blaschkeCauchyTransform_eq_left line 548
46. theorem OAI.InternalCatalan.blaschkeCauchyTransform_eq_right line 557
47. theorem OAI.InternalCatalan.blaschkeCauchyLeft_analyticAt line 566
48. theorem OAI.InternalCatalan.blaschkeCauchyRight_analyticAt line 576
49. theorem OAI.InternalCatalan.blaschkeCauchyLeft_sub_right line 586
50. theorem OAI.InternalCatalan.blaschkeDensity_endpoint_difference_norm_le line 614
51. theorem OAI.InternalCatalan.blaschkeDensity_endpoint_difference_quotient_norm_le line 644
52. def OAI.InternalCatalan.blaschkeInterpolant line 667
53. theorem OAI.InternalCatalan.blaschkeNodePolynomial_eval_node line 674
54. theorem OAI.InternalCatalan.blaschkeIntegratedNodeDifference_eq_scalarIntegral line 679
55. theorem OAI.InternalCatalan.blaschkeInterpolant_analyticAt line 694
56. theorem OAI.InternalCatalan.blaschkeInterpolant_analyticOnNhd_closedDisk line 705
57. theorem OAI.InternalCatalan.blaschkeInterpolant_eval_negative_node line 720
58. theorem OAI.InternalCatalan.cauchy_coefficient_mul_two_pi line 732
59. theorem OAI.InternalCatalan.blaschkeInterpolant_eval_positive_node line 741
60. theorem OAI.InternalCatalan.blaschkeInterpolant_eq_left_continuation line 759
61. theorem OAI.InternalCatalan.blaschkeInterpolant_eq_right_continuation line 777
62. theorem OAI.InternalCatalan.blaschkeNodePolynomial_ne_zero_on_circle line 803
63. theorem OAI.InternalCatalan.blaschkeDensity_norm_eq_one_on_circle line 812
64. theorem OAI.InternalCatalan.circle_inside_cauchy_strip line 818
65. theorem OAI.InternalCatalan.blaschkeInterpolant_circle_eq_left line 825
66. theorem OAI.InternalCatalan.blaschkeInterpolant_circle_eq_right line 834
67. theorem OAI.InternalCatalan.blaschkeInterpolant_circle_norm_le_five_add line 844
68. theorem OAI.InternalCatalan.interpolant_far_axis_numerical line 858
69. theorem OAI.InternalCatalan.interpolant_near_axis_numerical line 872
70. theorem OAI.InternalCatalan.blaschkeCauchyKernel_local_norm_le line 893
71. theorem OAI.InternalCatalan.blaschkeCauchyKernel_far_piece_norm_le line 946
72. theorem OAI.InternalCatalan.blaschkeCauchyTransform_norm_le_split line 988
73. theorem OAI.InternalCatalan.blaschkeCauchyTransform_upper_crossing_bound line 1018
74. theorem OAI.InternalCatalan.blaschkeCauchyTransform_lower_crossing_bound line 1076
75. theorem OAI.InternalCatalan.blaschkeCauchyTransform_near_axis_bound line 1135
76. theorem OAI.InternalCatalan.blaschkeInterpolant_boundary_norm_le_off_axis line 1157
77. theorem OAI.InternalCatalan.blaschkeInterpolant_boundary_norm_le line 1189
78. theorem OAI.InternalCatalan.blaschkeInterpolant_closedDisk_norm_le line 1218
79. theorem OAI.InternalCatalan.real_uniform_interpolation_actual line 1236