OAI/Probability/Contingency/DyadicLaws.lean

GitHub source file

73 declarations, 0 contain sorry, 0 declared as axioms

Dyadic Laws.

  1. structure OAI.Contingency.DyadicLaw line 21
  2. def OAI.Contingency.DyadicLaw.pure line 31
  3. def OAI.Contingency.DyadicLaw.bind line 38
  4. def OAI.Contingency.DyadicLaw.map line 48
  5. theorem OAI.Contingency.DyadicLaw.map_bits line 51
  6. theorem OAI.Contingency.DyadicLaw.map_count line 54
  7. def OAI.Contingency.DyadicLaw.walk line 64
  8. theorem OAI.Contingency.DyadicLaw.walk_bits line 69
  9. def OAI.Contingency.DyadicLaw.probability line 76
  10. theorem OAI.Contingency.DyadicLaw.probability_nonneg line 78
  11. theorem OAI.Contingency.DyadicLaw.probability_total line 83
  12. def OAI.Contingency.bitWordLaw line 94
  13. def OAI.Contingency.roundedOffset line 100
  14. def OAI.Contingency.offsetLaw line 106
  15. def OAI.Contingency.offsetNumerator line 110
  16. theorem OAI.Contingency.offset_preimage line 113
  17. theorem OAI.Contingency.offsetLaw_count line 134
  18. def OAI.Contingency.stoppedNumerator line 145
  19. theorem OAI.Contingency.stoppedNumerator_total line 150
  20. def OAI.Contingency.stoppedLaw line 163
  21. theorem OAI.Contingency.stoppedNumerator_closed line 174
  22. def OAI.Contingency.residualNumerator line 196
  23. theorem OAI.Contingency.residual_integers line 199
  24. structure OAI.Contingency.Law line 225
  25. theorem OAI.Contingency.Law.ext line 233
  26. def OAI.Contingency.Law.pure line 235
  27. def OAI.Contingency.Law.bind line 239
  28. def OAI.Contingency.Law.map line 244
  29. def OAI.Contingency.Law.tv line 246
  30. theorem OAI.Contingency.Law.tv_nonneg line 248
  31. theorem OAI.Contingency.Law.tv_self line 249
  32. theorem OAI.Contingency.Law.tv_symm line 250
  33. theorem OAI.Contingency.Law.tv_triangle line 252
  34. theorem OAI.Contingency.Law.tv_le_one line 258
  35. theorem OAI.Contingency.Law.tv_bind_left line 266
  36. theorem OAI.Contingency.Law.tv_bind_right line 279
  37. theorem OAI.Contingency.Law.tv_bind_right_bound line 293
  38. theorem OAI.Contingency.Law.tv_bind line 300
  39. theorem OAI.Contingency.Law.tv_map line 304
  40. def OAI.Contingency.Law.first line 307
  41. theorem OAI.Contingency.Law.first_tv line 312
  42. theorem OAI.Contingency.Law.bind_pure_mass line 323
  43. theorem OAI.Contingency.Law.first_mass line 327
  44. theorem OAI.Contingency.Law.first_ideal_tv line 344
  45. def OAI.Contingency.DyadicLaw.toLaw line 371
  46. theorem OAI.Contingency.DyadicLaw.toLaw_bind line 380
  47. def OAI.Contingency.Law.uniform line 392
  48. theorem OAI.Contingency.ceilDiv_error line 399
  49. theorem OAI.Contingency.offsetNumerator_error line 408
  50. theorem OAI.Contingency.offsetLaw_point_error line 418
  51. theorem OAI.Contingency.offsetLaw_tv line 433
  52. theorem OAI.Contingency.rounded_offset_accuracy line 446
  53. def OAI.Contingency.Law.pi line 470
  54. theorem OAI.Contingency.Law.tv_overlap line 477
  55. theorem OAI.Contingency.Law.deficit_prod_le_sum line 490
  56. theorem OAI.Contingency.Law.tv_pi line 502
  57. def OAI.Contingency.Law.prod line 524
  58. theorem OAI.Contingency.Law.prod_eq_bind line 529
  59. theorem OAI.Contingency.Law.tv_prod line 539
  60. theorem OAI.Contingency.DyadicLaw.toLaw_pure line 557
  61. theorem OAI.Contingency.DyadicLaw.toLaw_map line 563
  62. def OAI.Contingency.DyadicLaw.pad line 569
  63. theorem OAI.Contingency.DyadicLaw.toLaw_pad line 574
  64. def OAI.Contingency.DyadicLaw.pi line 583
  65. theorem OAI.Contingency.DyadicLaw.toLaw_pi line 588
  66. theorem OAI.Contingency.DyadicLaw.toLaw_walk line 593
  67. theorem OAI.Contingency.stoppedLaw_toLaw line 603
  68. def OAI.Contingency.Law.sigma line 639
  69. theorem OAI.Contingency.Law.sigma_eq_bind line 647
  70. theorem OAI.Contingency.Law.tv_sigma line 663
  71. def OAI.Contingency.DyadicLaw.sigma line 673
  72. theorem OAI.Contingency.DyadicLaw.sigma_bits line 681
  73. theorem OAI.Contingency.DyadicLaw.toLaw_sigma line 684