OAI/Analysis/Triangular/Certificate/WaveExpData.lean

GitHub source file

83 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AtomicTriangular.FiniteCertificate.lambdaTable0 line 9
  2. lemma OAI.AtomicTriangular.FiniteCertificate.lambdaTable0_calc line 41
  3. lemma OAI.AtomicTriangular.FiniteCertificate.lambdaTable0_mem line 44
  4. def OAI.AtomicTriangular.FiniteCertificate.phaseHTable0 line 47
  5. lemma OAI.AtomicTriangular.FiniteCertificate.phaseHTable0_calc line 79
  6. lemma OAI.AtomicTriangular.FiniteCertificate.phaseHTable0_mem line 82
  7. def OAI.AtomicTriangular.FiniteCertificate.lambdaTable1 line 85
  8. lemma OAI.AtomicTriangular.FiniteCertificate.lambdaTable1_calc line 117
  9. lemma OAI.AtomicTriangular.FiniteCertificate.lambdaTable1_mem line 120
  10. def OAI.AtomicTriangular.FiniteCertificate.phaseHTable1 line 123
  11. lemma OAI.AtomicTriangular.FiniteCertificate.phaseHTable1_calc line 155
  12. lemma OAI.AtomicTriangular.FiniteCertificate.phaseHTable1_mem line 158
  13. def OAI.AtomicTriangular.FiniteCertificate.lambdaTable line 161
  14. lemma OAI.AtomicTriangular.FiniteCertificate.lambdaTable_mem line 162
  15. def OAI.AtomicTriangular.FiniteCertificate.phaseHTable line 166
  16. lemma OAI.AtomicTriangular.FiniteCertificate.phaseHTable_mem line 167
  17. def OAI.AtomicTriangular.FiniteCertificate.waveExp0_1 line 172
  18. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp0_1_calc line 204
  19. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp0_1_mem line 207
  20. def OAI.AtomicTriangular.FiniteCertificate.waveExp0_3 line 213
  21. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp0_3_calc line 245
  22. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp0_3_mem line 248
  23. def OAI.AtomicTriangular.FiniteCertificate.waveExp0_4 line 254
  24. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp0_4_calc line 286
  25. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp0_4_mem line 289
  26. def OAI.AtomicTriangular.FiniteCertificate.waveExp0_7 line 295
  27. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp0_7_calc line 327
  28. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp0_7_mem line 330
  29. def OAI.AtomicTriangular.FiniteCertificate.waveExp0_9 line 336
  30. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp0_9_calc line 368
  31. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp0_9_mem line 371
  32. def OAI.AtomicTriangular.FiniteCertificate.waveExp0_12 line 377
  33. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp0_12_calc line 409
  34. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp0_12_mem line 412
  35. def OAI.AtomicTriangular.FiniteCertificate.waveExp0_13 line 418
  36. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp0_13_calc line 450
  37. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp0_13_mem line 453
  38. def OAI.AtomicTriangular.FiniteCertificate.waveExp0_16 line 459
  39. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp0_16_calc line 491
  40. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp0_16_mem line 494
  41. def OAI.AtomicTriangular.FiniteCertificate.waveExp0_19 line 500
  42. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp0_19_calc line 532
  43. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp0_19_mem line 535
  44. def OAI.AtomicTriangular.FiniteCertificate.waveExp0_21 line 541
  45. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp0_21_calc line 573
  46. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp0_21_mem line 576
  47. def OAI.AtomicTriangular.FiniteCertificate.waveExp1_1 line 582
  48. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp1_1_calc line 614
  49. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp1_1_mem line 617
  50. def OAI.AtomicTriangular.FiniteCertificate.waveExp1_3 line 623
  51. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp1_3_calc line 655
  52. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp1_3_mem line 658
  53. def OAI.AtomicTriangular.FiniteCertificate.waveExp1_4 line 664
  54. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp1_4_calc line 696
  55. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp1_4_mem line 699
  56. def OAI.AtomicTriangular.FiniteCertificate.waveExp1_7 line 705
  57. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp1_7_calc line 737
  58. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp1_7_mem line 740
  59. def OAI.AtomicTriangular.FiniteCertificate.waveExp1_9 line 746
  60. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp1_9_calc line 778
  61. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp1_9_mem line 781
  62. def OAI.AtomicTriangular.FiniteCertificate.waveExp1_12 line 787
  63. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp1_12_calc line 819
  64. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp1_12_mem line 822
  65. def OAI.AtomicTriangular.FiniteCertificate.waveExp1_13 line 828
  66. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp1_13_calc line 860
  67. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp1_13_mem line 863
  68. def OAI.AtomicTriangular.FiniteCertificate.waveExp1_16 line 869
  69. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp1_16_calc line 901
  70. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp1_16_mem line 904
  71. def OAI.AtomicTriangular.FiniteCertificate.waveExp1_19 line 910
  72. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp1_19_calc line 942
  73. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp1_19_mem line 945
  74. def OAI.AtomicTriangular.FiniteCertificate.waveExp1_21 line 951
  75. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp1_21_calc line 983
  76. lemma OAI.AtomicTriangular.FiniteCertificate.waveExp1_21_mem line 986
  77. def OAI.AtomicTriangular.FiniteCertificate.waveExpTable line 992
  78. lemma OAI.AtomicTriangular.FiniteCertificate.waveExpTable_mem line 995
  79. def OAI.AtomicTriangular.FiniteCertificate.QTable line 1018
  80. lemma OAI.AtomicTriangular.FiniteCertificate.QTable_mem line 1019
  81. def OAI.AtomicTriangular.FiniteCertificate.DTable line 1031
  82. lemma OAI.AtomicTriangular.FiniteCertificate.DTable_mem line 1032
  83. lemma OAI.AtomicTriangular.FiniteCertificate.QTable_pos line 1044