OAI/LinearAlgebra/MatrixFields/Certificates/CertificatesReplay.lean

GitHub source file

118 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLogCertificate.sumPower line 14
2. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLogCertificate.rationalSumPower line 17
3. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLogCertificate.realApprox line 20
4. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLogCertificate.rationalApprox line 23
5. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLogCertificate.rationalSumPower_cast line 27
6. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLogCertificate.rationalApprox_cast line 31
7. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLogCertificate.symmetric_expansion_error line 35
8. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLogCertificate.normalized_variable_bounds line 53
9. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLogCertificate.normalized_log_error line 61
10. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLogCertificate.normalized_log_error_80 line 82
11. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLogCertificate.rational_log_error_80 line 90
12. structure OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLogCertificate.ReducedArgument line 95
13. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLogCertificate.reducedApprox line 102
14. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLogCertificate.ReducedArgument.positive line 105
15. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLogCertificate.reduced_log_error line 109
16. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLogCertificate.reduced_entropy_error line 142
17. def OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLogCertificate.finiteEntropyApprox line 151
18. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLogCertificate.finite_entropy_error line 155
19. theorem OAI.MatrixAllFields.MatrixMultiplication.Foundation.RationalLogCertificate.finite_entropy_error_of_exponent_bound line 169
20. structure OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Ball line 201
21. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Ball.Encloses line 208
22. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Ball.exact line 210
23. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Ball.add line 211
24. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Ball.neg line 212
25. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Ball.mul line 213
26. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Ball.lower line 217
27. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Ball.upper line 218
28. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Ball.ofBounds line 220
29. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Ball.nonnegative_radius line 222
30. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Ball.bounds line 226
31. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Ball.ofBounds_sound line 232
32. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Ball.exact_sound line 239
33. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Ball.add_sound line 242
34. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Ball.neg_sound line 251
35. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Ball.mul_sound line 255
36. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Ball.widen_sound line 277
37. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Ball.inv line 288
38. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Ball.inv_sound line 290
39. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.reductionError line 303
40. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.reduction_error_cast line 306
41. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.logBall line 310
42. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.logBall_sound line 313
43. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.log_center_lipschitz line 329
44. inductive OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Expression line 362
45. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Expression.value line 370
46. inductive OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Certificate line 378
47. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Certificate.sound line 389
48. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.published_endpoint_below_target line 400
49. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.value_below_target_of_certificate line 404
50. inductive OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.Op line 435
51. instance OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.(instance at line 444) line 444
52. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.Program line 453
53. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.Op.value line 455
54. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.Program.eval line 463
55. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.contains line 466
56. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.contains_sound line 469
57. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.polynomial line 473
58. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.traceHead line 477
59. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.checkPolynomial line 479
60. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.checkPolynomial_sound line 486
61. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.logCoefficients line 503
62. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.realApprox_eq_polynomial line 506
63. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.normalized_log_error_48 line 515
64. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.pad line 523
65. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.pad_sound line 525
66. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.logVariable line 536
67. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.normalizedLogBall line 538
68. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.normalizedLogBall_sound line 541
69. structure OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.NInterval line 563
70. def OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.NInterval.Encloses line 570
71. def OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.NInterval.zero line 573
72. def OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.NInterval.add line 574
73. def OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.NInterval.mul line 575
74. def OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.NInterval.frac line 577
75. lemma OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.NInterval.div_floor_bounds line 579
76. lemma OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.NInterval.zero_sound line 590
77. lemma OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.NInterval.nonneg line 592
78. lemma OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.NInterval.add_sound line 595
79. lemma OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.NInterval.mul_sound line 600
80. lemma OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.NInterval.frac_sound line 620
81. def OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.NInterval.oddHorner line 635
82. def OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.NInterval.oddPolynomial line 640
83. lemma OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.NInterval.oddHorner_sound line 644
84. lemma OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.oddPolynomial_eq line 662
85. def OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.scale line 666
86. lemma OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.scale_pos line 667
87. def OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.logApprox line 669
88. lemma OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.logApprox_sound line 674
89. def OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.NInterval.ball line 688
90. lemma OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.NInterval.ball_sound line 691
91. def OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.normalized line 697
92. lemma OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.normalized_sound line 699
93. structure OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.LogData line 708
94. def OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.logResult line 714
95. def OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.checkLog line 718
96. lemma OAI.MatrixAllFields.MatrixMultiplication.CompactCertificate.checkLog_sound line 724
97. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.LogWitness line 748
98. abbrev OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.logResult line 749
99. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.checkLog line 751
100. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.checkLog_sound line 757
101. structure OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.Witness line 762
102. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.ballAt line 767
103. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.checkStep line 769
104. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.Related line 780
105. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.checkStep_sound line 783
106. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.Related.push line 802
107. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.Related.empty line 812
108. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.evalFrom line 818
109. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.ballsFrom line 821
110. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.checkFrom line 824
111. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.checkFrom_sound line 830
112. def OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.checkProgram line 846
113. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.checkProgram_sound line 849
114. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.evalFrom_append line 855
115. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.ballsFrom_append line 859
116. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.checkFrom_append line 863
117. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.checked_upper_bound line 881
118. theorem OAI.MatrixAllFields.MatrixMultiplication.AllFieldCertificates.Replay.checked_below_target line 888