OAI/Analysis/Triangular/Envelope/EnvelopeSums.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AtomicTriangular.FiniteCertificate.psiTableB line 13
  2. lemma OAI.AtomicTriangular.FiniteCertificate.psiTableB_mem line 14
  3. def OAI.AtomicTriangular.FiniteCertificate.envelopeSumBoxB line 26
  4. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeSumBoxB_calc line 27
  5. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeSumBoxB_mem line 30
  6. def OAI.AtomicTriangular.FiniteCertificate.psiTableC line 33
  7. lemma OAI.AtomicTriangular.FiniteCertificate.psiTableC_mem line 34
  8. def OAI.AtomicTriangular.FiniteCertificate.periodExpC line 51
  9. lemma OAI.AtomicTriangular.FiniteCertificate.periodExpC_calc line 52
  10. lemma OAI.AtomicTriangular.FiniteCertificate.periodExpC_pre line 55
  11. lemma OAI.AtomicTriangular.FiniteCertificate.periodExpC_mem line 58
  12. lemma OAI.AtomicTriangular.FiniteCertificate.periodDenC_pos line 65
  13. def OAI.AtomicTriangular.FiniteCertificate.envelopeSumBoxC line 68
  14. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeSumBoxC_calc line 69
  15. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeSumBoxC_mem line 72
  16. def OAI.AtomicTriangular.FiniteCertificate.psiTableD line 76
  17. lemma OAI.AtomicTriangular.FiniteCertificate.psiTableD_mem line 77
  18. def OAI.AtomicTriangular.FiniteCertificate.periodExpD line 94
  19. lemma OAI.AtomicTriangular.FiniteCertificate.periodExpD_calc line 95
  20. lemma OAI.AtomicTriangular.FiniteCertificate.periodExpD_pre line 98
  21. lemma OAI.AtomicTriangular.FiniteCertificate.periodExpD_mem line 101
  22. lemma OAI.AtomicTriangular.FiniteCertificate.periodDenD_pos line 108
  23. def OAI.AtomicTriangular.FiniteCertificate.envelopeSumBoxD line 111
  24. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeSumBoxD_calc line 112
  25. lemma OAI.AtomicTriangular.FiniteCertificate.envelopeSumBoxD_mem line 115
  26. def OAI.AtomicTriangular.FiniteCertificate.boundB line 119
  27. lemma OAI.AtomicTriangular.FiniteCertificate.boundB_calc line 120
  28. lemma OAI.AtomicTriangular.FiniteCertificate.boundB_mem line 123
  29. lemma OAI.AtomicTriangular.FiniteCertificate.finiteTailEnvelope_bound line 126
  30. def OAI.AtomicTriangular.FiniteCertificate.boundD line 129
  31. lemma OAI.AtomicTriangular.FiniteCertificate.boundD_calc line 130
  32. lemma OAI.AtomicTriangular.FiniteCertificate.boundD_mem line 133
  33. lemma OAI.AtomicTriangular.FiniteCertificate.tailTailEnvelope_bound line 136
  34. def OAI.AtomicTriangular.FiniteCertificate.boundC line 140
  35. lemma OAI.AtomicTriangular.FiniteCertificate.boundC_calc line 141
  36. lemma OAI.AtomicTriangular.FiniteCertificate.boundC_mem line 144
  37. lemma OAI.AtomicTriangular.FiniteCertificate.tailFiniteEnvelope_bound line 147
  38. def OAI.AtomicTriangular.FiniteCertificate.boundV line 151
  39. lemma OAI.AtomicTriangular.FiniteCertificate.boundV_calc line 152
  40. lemma OAI.AtomicTriangular.FiniteCertificate.boundV_mem line 155
  41. lemma OAI.AtomicTriangular.FiniteCertificate.tailConstantEnvelope_bound line 158
  42. def OAI.AtomicTriangular.FiniteCertificate.totalWBox line 161
  43. lemma OAI.AtomicTriangular.FiniteCertificate.totalWBox_calc line 162
  44. lemma OAI.AtomicTriangular.FiniteCertificate.fullW_column_bound line 165