OAI/Probability/Contingency/AllMarginLaw.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

All Margin Law.

  1. theorem OAI.Contingency.Parameters.D_positive line 22
  2. theorem OAI.Contingency.Parameters.table_card_D_all line 28
  3. theorem OAI.Contingency.Parameters.bits_le_input line 43
  4. theorem OAI.Contingency.Parameters.D_le_input line 51
  5. theorem OAI.Contingency.Parameters.schedule_base_le_input line 61
  6. theorem OAI.Contingency.arbitraryDraw_bits_input line 76
  7. def OAI.Contingency.arbitraryResidual line 97
  8. theorem OAI.Contingency.arbitraryResidual_data line 99
  9. theorem OAI.Contingency.arbitraryResidual_total_pos line 108
  10. theorem OAI.Contingency.arbitrary_corrected_exact line 115
  11. def OAI.Contingency.BinaryArithmetic.predCost line 141
  12. theorem OAI.Contingency.BinaryArithmetic.predCost_le line 146
  13. theorem OAI.Contingency.BinaryArithmetic.pred_size_le line 149
  14. def OAI.Contingency.BinaryArithmetic.signedSize line 154
  15. theorem OAI.Contingency.BinaryArithmetic.signedSize_pos line 156
  16. theorem OAI.Contingency.BinaryArithmetic.signedSize_neg line 157
  17. theorem OAI.Contingency.BinaryArithmetic.signedSize_zero line 158
  18. theorem OAI.Contingency.BinaryArithmetic.signedSize_toZNum line 159
  19. theorem OAI.Contingency.BinaryArithmetic.signedSize_toZNumNeg line 160
  20. theorem OAI.Contingency.BinaryArithmetic.signedSize_bit0 line 162
  21. theorem OAI.Contingency.BinaryArithmetic.predCase_size line 165
  22. theorem OAI.Contingency.BinaryArithmetic.signedSize_bit1 line 168
  23. theorem OAI.Contingency.BinaryArithmetic.signedSize_bitm1 line 176
  24. theorem OAI.Contingency.BinaryArithmetic.sub'_size line 184
  25. def OAI.Contingency.BinaryArithmetic.signedBitCost line 217
  26. theorem OAI.Contingency.BinaryArithmetic.signedBitCost_le line 222
  27. def OAI.Contingency.BinaryArithmetic.subCost line 229
  28. theorem OAI.Contingency.BinaryArithmetic.subCost_le line 237
  29. def OAI.Contingency.BinaryArithmetic.divisionAuxCost line 270
  30. theorem OAI.Contingency.BinaryArithmetic.divisionAuxCost_le line 275
  31. def OAI.Contingency.BinaryArithmetic.divisionCost line 285
  32. theorem OAI.Contingency.BinaryArithmetic.remainder_size line 290
  33. theorem OAI.Contingency.BinaryArithmetic.numBit0_size line 296
  34. theorem OAI.Contingency.BinaryArithmetic.numBit1_size line 299
  35. theorem OAI.Contingency.BinaryArithmetic.divisionCost_le line 302
  36. theorem OAI.Contingency.BinaryArithmetic.division_certificate line 323
  37. theorem OAI.Contingency.Grid.vertex_card line 341
  38. theorem OAI.Contingency.Grid.vertex_card_dyadic line 345
  39. theorem OAI.Contingency.Dense.offsets_card_dyadic line 356
  40. def OAI.Contingency.IntegerTabulation.arithmeticTerms line 371
  41. theorem OAI.Contingency.IntegerTabulation.arithmeticTerms_bound line 376
  42. def OAI.Contingency.Dense.BinProblem.cornerEntries line 407
  43. def OAI.Contingency.Dense.BinProblem.rationalPenalty line 413
  44. def OAI.Contingency.Dense.BinProblem.rationalExponent line 418
  45. theorem OAI.Contingency.Dense.BinProblem.cornerEntries_cast line 424
  46. theorem OAI.Contingency.Dense.BinProblem.rationalPenalty_cast line 434
  47. theorem OAI.Contingency.Dense.BinProblem.rationalExponent_eq line 451
  48. def OAI.Contingency.Dense.BinProblem.cellExponent line 474
  49. def OAI.Contingency.Dense.BinProblem.integerExponent line 479
  50. theorem OAI.Contingency.Dense.BinProblem.cellExponent_eq line 486
  51. theorem OAI.Contingency.Dense.BinProblem.integerExponent_eq_rational line 500
  52. theorem OAI.Contingency.Dense.BinProblem.integerExponent_eq line 514
  53. def OAI.Contingency.BitModel.StackCode.HighPad.pushCode line 530
  54. abbrev OAI.Contingency.BitModel.StackCode.HighPad.pushProgram line 533
  55. abbrev OAI.Contingency.BitModel.StackCode.HighPad.back line 534
  56. abbrev OAI.Contingency.BitModel.StackCode.HighPad.program line 535
  57. theorem OAI.Contingency.BitModel.StackCode.HighPad.push_noCoin line 537
  58. theorem OAI.Contingency.BitModel.StackCode.HighPad.back_noCoin line 538
  59. theorem OAI.Contingency.BitModel.StackCode.HighPad.noCoin line 541
  60. theorem OAI.Contingency.BitModel.StackCode.HighPad.back_run line 545
  61. theorem OAI.Contingency.BitModel.StackCode.HighPad.pad line 575
  62. def OAI.Contingency.BitModel.StackCode.PreparedIntegerCall.outputRegister line 628
  63. theorem OAI.Contingency.BitModel.StackCode.PreparedIntegerCall.finite_memory_safe line 630