OAI/Analysis/Triangular/Certificate/Inverse.lean

GitHub source file

154 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AtomicTriangular.FiniteCertificate.minusBlockBox line 10
  2. lemma OAI.AtomicTriangular.FiniteCertificate.minusBlockBox_mem line 11
  3. def OAI.AtomicTriangular.FiniteCertificate.minusApproxNum line 13
  4. def OAI.AtomicTriangular.FiniteCertificate.minusApprox line 34
  5. def OAI.AtomicTriangular.FiniteCertificate.minusApproxBox line 35
  6. lemma OAI.AtomicTriangular.FiniteCertificate.minusApproxBox_mem line 36
  7. lemma OAI.AtomicTriangular.FiniteCertificate.minusApprox_bound line 37
  8. def OAI.AtomicTriangular.FiniteCertificate.minusResidualBox line 45
  9. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualBox_mem line 47
  10. def OAI.AtomicTriangular.FiniteCertificate.minusResidualRow0 line 50
  11. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow0_calc line 71
  12. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow0_mem line 74
  13. def OAI.AtomicTriangular.FiniteCertificate.minusResidualRow1 line 78
  14. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow1_calc line 99
  15. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow1_mem line 102
  16. def OAI.AtomicTriangular.FiniteCertificate.minusResidualRow2 line 106
  17. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow2_calc line 127
  18. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow2_mem line 130
  19. def OAI.AtomicTriangular.FiniteCertificate.minusResidualRow3 line 134
  20. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow3_calc line 155
  21. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow3_mem line 158
  22. def OAI.AtomicTriangular.FiniteCertificate.minusResidualRow4 line 162
  23. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow4_calc line 183
  24. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow4_mem line 186
  25. def OAI.AtomicTriangular.FiniteCertificate.minusResidualRow5 line 190
  26. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow5_calc line 211
  27. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow5_mem line 214
  28. def OAI.AtomicTriangular.FiniteCertificate.minusResidualRow6 line 218
  29. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow6_calc line 239
  30. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow6_mem line 242
  31. def OAI.AtomicTriangular.FiniteCertificate.minusResidualRow7 line 246
  32. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow7_calc line 267
  33. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow7_mem line 270
  34. def OAI.AtomicTriangular.FiniteCertificate.minusResidualRow8 line 274
  35. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow8_calc line 295
  36. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow8_mem line 298
  37. def OAI.AtomicTriangular.FiniteCertificate.minusResidualRow9 line 302
  38. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow9_calc line 323
  39. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow9_mem line 326
  40. def OAI.AtomicTriangular.FiniteCertificate.minusResidualRow10 line 330
  41. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow10_calc line 351
  42. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow10_mem line 354
  43. def OAI.AtomicTriangular.FiniteCertificate.minusResidualRow11 line 358
  44. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow11_calc line 379
  45. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow11_mem line 382
  46. def OAI.AtomicTriangular.FiniteCertificate.minusResidualRow12 line 386
  47. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow12_calc line 407
  48. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow12_mem line 410
  49. def OAI.AtomicTriangular.FiniteCertificate.minusResidualRow13 line 414
  50. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow13_calc line 435
  51. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow13_mem line 438
  52. def OAI.AtomicTriangular.FiniteCertificate.minusResidualRow14 line 442
  53. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow14_calc line 463
  54. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow14_mem line 466
  55. def OAI.AtomicTriangular.FiniteCertificate.minusResidualRow15 line 470
  56. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow15_calc line 491
  57. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow15_mem line 494
  58. def OAI.AtomicTriangular.FiniteCertificate.minusResidualRow16 line 498
  59. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow16_calc line 519
  60. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow16_mem line 522
  61. def OAI.AtomicTriangular.FiniteCertificate.minusResidualRow17 line 526
  62. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow17_calc line 547
  63. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow17_mem line 550
  64. def OAI.AtomicTriangular.FiniteCertificate.minusResidualRow18 line 554
  65. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow18_calc line 575
  66. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow18_mem line 578
  67. def OAI.AtomicTriangular.FiniteCertificate.minusResidualRow19 line 582
  68. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow19_calc line 603
  69. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualRow19_mem line 606
  70. def OAI.AtomicTriangular.FiniteCertificate.minusResidualTable line 610
  71. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidualTable_mem line 611
  72. lemma OAI.AtomicTriangular.FiniteCertificate.minusResidual_bound line 634
  73. lemma OAI.AtomicTriangular.FiniteCertificate.minusBlock_isUnit line 641
  74. lemma OAI.AtomicTriangular.FiniteCertificate.minusInverse_bound line 643
  75. lemma OAI.AtomicTriangular.FiniteCertificate.minusInverse_error line 646
  76. def OAI.AtomicTriangular.FiniteCertificate.minusInverseBox line 649
  77. lemma OAI.AtomicTriangular.FiniteCertificate.minusInverseBox_mem line 650
  78. def OAI.AtomicTriangular.FiniteCertificate.plusBlockBox line 657
  79. lemma OAI.AtomicTriangular.FiniteCertificate.plusBlockBox_mem line 658
  80. def OAI.AtomicTriangular.FiniteCertificate.plusApproxNum line 660
  81. def OAI.AtomicTriangular.FiniteCertificate.plusApprox line 681
  82. def OAI.AtomicTriangular.FiniteCertificate.plusApproxBox line 682
  83. lemma OAI.AtomicTriangular.FiniteCertificate.plusApproxBox_mem line 683
  84. lemma OAI.AtomicTriangular.FiniteCertificate.plusApprox_bound line 684
  85. def OAI.AtomicTriangular.FiniteCertificate.plusResidualBox line 692
  86. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualBox_mem line 694
  87. def OAI.AtomicTriangular.FiniteCertificate.plusResidualRow0 line 697
  88. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow0_calc line 718
  89. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow0_mem line 721
  90. def OAI.AtomicTriangular.FiniteCertificate.plusResidualRow1 line 725
  91. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow1_calc line 746
  92. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow1_mem line 749
  93. def OAI.AtomicTriangular.FiniteCertificate.plusResidualRow2 line 753
  94. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow2_calc line 774
  95. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow2_mem line 777
  96. def OAI.AtomicTriangular.FiniteCertificate.plusResidualRow3 line 781
  97. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow3_calc line 802
  98. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow3_mem line 805
  99. def OAI.AtomicTriangular.FiniteCertificate.plusResidualRow4 line 809
  100. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow4_calc line 830
  101. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow4_mem line 833
  102. def OAI.AtomicTriangular.FiniteCertificate.plusResidualRow5 line 837
  103. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow5_calc line 858
  104. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow5_mem line 861
  105. def OAI.AtomicTriangular.FiniteCertificate.plusResidualRow6 line 865
  106. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow6_calc line 886
  107. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow6_mem line 889
  108. def OAI.AtomicTriangular.FiniteCertificate.plusResidualRow7 line 893
  109. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow7_calc line 914
  110. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow7_mem line 917
  111. def OAI.AtomicTriangular.FiniteCertificate.plusResidualRow8 line 921
  112. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow8_calc line 942
  113. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow8_mem line 945
  114. def OAI.AtomicTriangular.FiniteCertificate.plusResidualRow9 line 949
  115. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow9_calc line 970
  116. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow9_mem line 973
  117. def OAI.AtomicTriangular.FiniteCertificate.plusResidualRow10 line 977
  118. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow10_calc line 998
  119. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow10_mem line 1001
  120. def OAI.AtomicTriangular.FiniteCertificate.plusResidualRow11 line 1005
  121. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow11_calc line 1026
  122. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow11_mem line 1029
  123. def OAI.AtomicTriangular.FiniteCertificate.plusResidualRow12 line 1033
  124. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow12_calc line 1054
  125. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow12_mem line 1057
  126. def OAI.AtomicTriangular.FiniteCertificate.plusResidualRow13 line 1061
  127. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow13_calc line 1082
  128. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow13_mem line 1085
  129. def OAI.AtomicTriangular.FiniteCertificate.plusResidualRow14 line 1089
  130. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow14_calc line 1110
  131. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow14_mem line 1113
  132. def OAI.AtomicTriangular.FiniteCertificate.plusResidualRow15 line 1117
  133. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow15_calc line 1138
  134. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow15_mem line 1141
  135. def OAI.AtomicTriangular.FiniteCertificate.plusResidualRow16 line 1145
  136. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow16_calc line 1166
  137. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow16_mem line 1169
  138. def OAI.AtomicTriangular.FiniteCertificate.plusResidualRow17 line 1173
  139. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow17_calc line 1194
  140. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow17_mem line 1197
  141. def OAI.AtomicTriangular.FiniteCertificate.plusResidualRow18 line 1201
  142. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow18_calc line 1222
  143. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow18_mem line 1225
  144. def OAI.AtomicTriangular.FiniteCertificate.plusResidualRow19 line 1229
  145. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow19_calc line 1250
  146. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualRow19_mem line 1253
  147. def OAI.AtomicTriangular.FiniteCertificate.plusResidualTable line 1257
  148. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidualTable_mem line 1258
  149. lemma OAI.AtomicTriangular.FiniteCertificate.plusResidual_bound line 1281
  150. lemma OAI.AtomicTriangular.FiniteCertificate.plusBlock_isUnit line 1288
  151. lemma OAI.AtomicTriangular.FiniteCertificate.plusInverse_bound line 1290
  152. lemma OAI.AtomicTriangular.FiniteCertificate.plusInverse_error line 1293
  153. def OAI.AtomicTriangular.FiniteCertificate.plusInverseBox line 1296
  154. lemma OAI.AtomicTriangular.FiniteCertificate.plusInverseBox_mem line 1297