OAI/Probability/Contingency/Unpadding.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Unpadding.

  1. def OAI.Contingency.PaddedGraph.cellPadding line 16
  2. def OAI.Contingency.PaddedGraph.largePart line 18
  3. theorem OAI.Contingency.PaddedGraph.split_padding line 21
  4. def OAI.Contingency.PaddedGraph.paddedCompletion line 25
  5. abbrev OAI.Contingency.PaddedGraph.SuccessPair line 48
  6. theorem OAI.Contingency.PaddedGraph.successPair_ext line 51
  7. def OAI.Contingency.PaddedGraph.padOriginal line 60
  8. def OAI.Contingency.PaddedGraph.unpadEntry line 64
  9. theorem OAI.Contingency.PaddedGraph.unpadEntry_nonneg line 67
  10. def OAI.Contingency.PaddedGraph.unpadOriginal line 79
  11. theorem OAI.Contingency.PaddedGraph.unpad_pad line 102
  12. theorem OAI.Contingency.PaddedGraph.pad_unpad line 107
  13. def OAI.Contingency.PaddedGraph.successEquiv line 130
  14. def OAI.Contingency.shiftedRow line 148
  15. def OAI.Contingency.shiftedCol line 149
  16. abbrev OAI.Contingency.ShiftPassing line 150
  17. def OAI.Contingency.shiftTable line 152
  18. def OAI.Contingency.unshiftTable line 158
  19. def OAI.Contingency.shiftEquiv line 173
  20. theorem OAI.Contingency.shift_card line 179
  21. def OAI.Contingency.PaddedGraph.naturalPadding line 194
  22. abbrev OAI.Contingency.PaddedGraph.Enlarged line 195
  23. abbrev OAI.Contingency.PaddedGraph.EnlargedBad line 196
  24. abbrev OAI.Contingency.PaddedGraph.LargeCell line 197
  25. theorem OAI.Contingency.PaddedGraph.enlarged_partition line 199
  26. theorem OAI.Contingency.PaddedGraph.enlarged_bad_union line 205
  27. theorem OAI.Contingency.PaddedGraph.enlarged_bad_count line 226
  28. abbrev OAI.Contingency.PaddedGraph.TransverseJoint line 248
  29. def OAI.Contingency.PaddedGraph.enlargedOfTransverse line 250
  30. theorem OAI.Contingency.PaddedGraph.enlargedOfTransverse_injective line 273
  31. theorem OAI.Contingency.PaddedGraph.transverseMass_enlarged line 300
  32. theorem OAI.Contingency.PaddedGraph.enlarged_half line 321
  33. theorem OAI.Contingency.PaddedGraph.stationary_success_count line 342
  34. theorem OAI.Contingency.PaddedGraph.stationary_success_probability line 349
  35. def OAI.Contingency.PaddedGraph.successfulJoint line 362
  36. def OAI.Contingency.PaddedGraph.decodeJoint line 364
  37. theorem OAI.Contingency.PaddedGraph.decodeJoint_eq_some line 370
  38. def OAI.Contingency.PaddedGraph.stationaryTrial line 414
  39. theorem OAI.Contingency.PaddedGraph.stationaryTrial_some line 416
  40. theorem OAI.Contingency.PaddedGraph.stationaryTrial_none line 423
  41. theorem OAI.Contingency.PaddedGraph.stationaryTrial_uniform line 432
  42. theorem OAI.Contingency.PaddedGraph.invariant_joint line 460
  43. def OAI.Contingency.PaddedGraph.jointTrial line 483
  44. theorem OAI.Contingency.PaddedGraph.jointTrial_tv line 486
  45. theorem OAI.Contingency.Schedule.exp_neg_binary line 506
  46. theorem OAI.Contingency.Schedule.failure_schedule line 520
  47. theorem OAI.Contingency.Schedule.jo_binary line 529
  48. theorem OAI.Contingency.Schedule.transition_binary line 534
  49. theorem OAI.Contingency.Schedule.offset_schedule line 540
  50. theorem OAI.Contingency.Schedule.mixing_schedule line 562
  51. theorem OAI.Contingency.Schedule.outer_error_schedule line 592
  52. def OAI.Contingency.PaddedGraph.implementedTrial line 624
  53. theorem OAI.Contingency.PaddedGraph.implementedTrial_bits line 629
  54. theorem OAI.Contingency.PaddedGraph.toLaw_implementedTrial line 635
  55. theorem OAI.Contingency.PaddedGraph.implementedTrial_tv line 644