OAI/Analysis/Triangular/Certificate/TargetInterval.lean

GitHub source file

147 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AtomicTriangular.FiniteCertificate.targetZBox line 9
  2. lemma OAI.AtomicTriangular.FiniteCertificate.targetZBox_mem line 10
  3. def OAI.AtomicTriangular.FiniteCertificate.targetRateBox line 12
  4. lemma OAI.AtomicTriangular.FiniteCertificate.targetRateBox_mem line 13
  5. def OAI.AtomicTriangular.FiniteCertificate.targetExpInput line 17
  6. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpInput_mem line 19
  7. def OAI.AtomicTriangular.FiniteCertificate.targetEnvBox line 25
  8. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvBox_mem line 28
  9. def OAI.AtomicTriangular.FiniteCertificate.targetExpf9 line 38
  10. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpf9_calc line 39
  11. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpf9_mem line 40
  12. def OAI.AtomicTriangular.FiniteCertificate.targetEnvf9 line 43
  13. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvf9_calc line 44
  14. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvf9_mem line 45
  15. def OAI.AtomicTriangular.FiniteCertificate.targetExpf12 line 50
  16. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpf12_calc line 51
  17. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpf12_mem line 52
  18. def OAI.AtomicTriangular.FiniteCertificate.targetEnvf12 line 55
  19. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvf12_calc line 56
  20. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvf12_mem line 57
  21. def OAI.AtomicTriangular.FiniteCertificate.targetExpf13 line 62
  22. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpf13_calc line 63
  23. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpf13_mem line 64
  24. def OAI.AtomicTriangular.FiniteCertificate.targetEnvf13 line 67
  25. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvf13_calc line 68
  26. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvf13_mem line 69
  27. def OAI.AtomicTriangular.FiniteCertificate.targetExpf16 line 74
  28. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpf16_calc line 75
  29. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpf16_mem line 76
  30. def OAI.AtomicTriangular.FiniteCertificate.targetEnvf16 line 79
  31. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvf16_calc line 80
  32. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvf16_mem line 81
  33. def OAI.AtomicTriangular.FiniteCertificate.targetExpf19 line 86
  34. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpf19_calc line 87
  35. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpf19_mem line 88
  36. def OAI.AtomicTriangular.FiniteCertificate.targetEnvf19 line 91
  37. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvf19_calc line 92
  38. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvf19_mem line 93
  39. def OAI.AtomicTriangular.FiniteCertificate.targetExpf21 line 98
  40. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpf21_calc line 99
  41. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpf21_mem line 100
  42. def OAI.AtomicTriangular.FiniteCertificate.targetEnvf21 line 103
  43. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvf21_calc line 104
  44. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvf21_mem line 105
  45. def OAI.AtomicTriangular.FiniteCertificate.targetEnvTablef line 110
  46. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvTablef_mem line 111
  47. def OAI.AtomicTriangular.FiniteCertificate.targetExpt36 line 119
  48. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt36_calc line 120
  49. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt36_mem line 121
  50. def OAI.AtomicTriangular.FiniteCertificate.targetEnvt36 line 124
  51. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt36_calc line 125
  52. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt36_mem line 126
  53. def OAI.AtomicTriangular.FiniteCertificate.targetExpt37 line 131
  54. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt37_calc line 132
  55. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt37_mem line 133
  56. def OAI.AtomicTriangular.FiniteCertificate.targetEnvt37 line 136
  57. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt37_calc line 137
  58. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt37_mem line 138
  59. def OAI.AtomicTriangular.FiniteCertificate.targetExpt39 line 143
  60. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt39_calc line 144
  61. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt39_mem line 145
  62. def OAI.AtomicTriangular.FiniteCertificate.targetEnvt39 line 148
  63. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt39_calc line 149
  64. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt39_mem line 150
  65. def OAI.AtomicTriangular.FiniteCertificate.targetExpt40 line 155
  66. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt40_calc line 156
  67. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt40_mem line 157
  68. def OAI.AtomicTriangular.FiniteCertificate.targetEnvt40 line 160
  69. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt40_calc line 161
  70. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt40_mem line 162
  71. def OAI.AtomicTriangular.FiniteCertificate.targetExpt43 line 167
  72. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt43_calc line 168
  73. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt43_mem line 169
  74. def OAI.AtomicTriangular.FiniteCertificate.targetEnvt43 line 172
  75. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt43_calc line 173
  76. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt43_mem line 174
  77. def OAI.AtomicTriangular.FiniteCertificate.targetExpt45 line 179
  78. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt45_calc line 180
  79. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt45_mem line 181
  80. def OAI.AtomicTriangular.FiniteCertificate.targetEnvt45 line 184
  81. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt45_calc line 185
  82. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt45_mem line 186
  83. def OAI.AtomicTriangular.FiniteCertificate.targetExpt48 line 191
  84. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt48_calc line 192
  85. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt48_mem line 193
  86. def OAI.AtomicTriangular.FiniteCertificate.targetEnvt48 line 196
  87. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt48_calc line 197
  88. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt48_mem line 198
  89. def OAI.AtomicTriangular.FiniteCertificate.targetExpt49 line 203
  90. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt49_calc line 204
  91. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt49_mem line 205
  92. def OAI.AtomicTriangular.FiniteCertificate.targetEnvt49 line 208
  93. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt49_calc line 209
  94. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt49_mem line 210
  95. def OAI.AtomicTriangular.FiniteCertificate.targetExpt52 line 215
  96. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt52_calc line 216
  97. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt52_mem line 217
  98. def OAI.AtomicTriangular.FiniteCertificate.targetEnvt52 line 220
  99. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt52_calc line 221
  100. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt52_mem line 222
  101. def OAI.AtomicTriangular.FiniteCertificate.targetExpt55 line 227
  102. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt55_calc line 228
  103. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt55_mem line 229
  104. def OAI.AtomicTriangular.FiniteCertificate.targetEnvt55 line 232
  105. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt55_calc line 233
  106. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt55_mem line 234
  107. def OAI.AtomicTriangular.FiniteCertificate.targetExpt57 line 239
  108. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt57_calc line 240
  109. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt57_mem line 241
  110. def OAI.AtomicTriangular.FiniteCertificate.targetEnvt57 line 244
  111. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt57_calc line 245
  112. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt57_mem line 246
  113. def OAI.AtomicTriangular.FiniteCertificate.targetExpt25 line 251
  114. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt25_calc line 252
  115. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt25_mem line 253
  116. def OAI.AtomicTriangular.FiniteCertificate.targetEnvt25 line 256
  117. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt25_calc line 257
  118. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt25_mem line 258
  119. def OAI.AtomicTriangular.FiniteCertificate.targetExpt27 line 263
  120. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt27_calc line 264
  121. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt27_mem line 265
  122. def OAI.AtomicTriangular.FiniteCertificate.targetEnvt27 line 268
  123. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt27_calc line 269
  124. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt27_mem line 270
  125. def OAI.AtomicTriangular.FiniteCertificate.targetExpt28 line 275
  126. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt28_calc line 276
  127. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt28_mem line 277
  128. def OAI.AtomicTriangular.FiniteCertificate.targetEnvt28 line 280
  129. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt28_calc line 281
  130. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt28_mem line 282
  131. def OAI.AtomicTriangular.FiniteCertificate.targetExpt31 line 287
  132. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt31_calc line 288
  133. lemma OAI.AtomicTriangular.FiniteCertificate.targetExpt31_mem line 289
  134. def OAI.AtomicTriangular.FiniteCertificate.targetEnvt31 line 292
  135. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt31_calc line 293
  136. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvt31_mem line 294
  137. def OAI.AtomicTriangular.FiniteCertificate.targetEnvTablet line 299
  138. lemma OAI.AtomicTriangular.FiniteCertificate.targetEnvTablet_mem line 300
  139. def OAI.AtomicTriangular.FiniteCertificate.finiteTargetBox line 317
  140. lemma OAI.AtomicTriangular.FiniteCertificate.finiteTargetBox_calc line 318
  141. lemma OAI.AtomicTriangular.FiniteCertificate.finiteTargetEnvelope_bound line 319
  142. def OAI.AtomicTriangular.FiniteCertificate.targetRatioBox line 324
  143. lemma OAI.AtomicTriangular.FiniteCertificate.targetRatioBox_calc line 325
  144. lemma OAI.AtomicTriangular.FiniteCertificate.targetRatioBox_mem line 326
  145. def OAI.AtomicTriangular.FiniteCertificate.tailTargetBox line 332
  146. lemma OAI.AtomicTriangular.FiniteCertificate.tailTargetBox_calc line 333
  147. lemma OAI.AtomicTriangular.FiniteCertificate.tailTargetEnvelope_bound line 334