OAI/Probability/Contingency/ConcreteContexts.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Concrete Contexts.

  1. def OAI.Contingency.PaddedGraph.smallRank line 15
  2. theorem OAI.Contingency.PaddedGraph.smallRank_injective line 18
  3. def OAI.Contingency.PaddedGraph.smallIndex line 25
  4. theorem OAI.Contingency.PaddedGraph.smallRank_lt_iff line 30
  5. theorem OAI.Contingency.PaddedGraph.smallIndex_lt line 55
  6. def OAI.Contingency.PaddedGraph.contextCoordinates line 66
  7. def OAI.Contingency.PaddedGraph.contextKernel line 73
  8. theorem OAI.Contingency.PaddedGraph.balanceProfile_box line 79
  9. theorem OAI.Contingency.PaddedGraph.balanceProfile_total line 85
  10. theorem OAI.Contingency.PaddedGraph.contextKernel_signature line 92
  11. theorem OAI.Contingency.PaddedGraph.contextKernel_continuous line 111
  12. theorem OAI.Contingency.PaddedGraph.contextKernel_nonneg line 117
  13. theorem OAI.Contingency.PaddedGraph.context_child_no_holes line 123
  14. def OAI.Contingency.branchEquiv line 145
  15. theorem OAI.Contingency.branchEquiv_value line 153
  16. theorem OAI.Contingency.allBalance_sum_leaf line 162
  17. def OAI.Contingency.mixedDisplay line 175
  18. theorem OAI.Contingency.mixedDisplay_base line 179
  19. theorem OAI.Contingency.mixedDisplay_slot line 184
  20. theorem OAI.Contingency.leafDisplay_mixed line 190
  21. theorem OAI.Contingency.mixedDisplay_injective line 198
  22. theorem OAI.Contingency.leafDisplay_injective line 207
  23. def OAI.Contingency.mixedBalance line 213
  24. theorem OAI.Contingency.allBalance_mixed line 217
  25. theorem OAI.Contingency.mixedDisplay_succ line 226
  26. theorem OAI.Contingency.mixedBalance_succ line 237
  27. def OAI.Contingency.surplusCaps line 250
  28. theorem OAI.Contingency.allSurplus_sum_types line 255
  29. def OAI.Contingency.PaddedGraph.splitSlots line 298
  30. def OAI.Contingency.PaddedGraph.prefixSlot line 303
  31. def OAI.Contingency.PaddedGraph.suffixSlot line 307
  32. theorem OAI.Contingency.PaddedGraph.contextCoordinates_prefix line 311
  33. theorem OAI.Contingency.PaddedGraph.contextCoordinates_suffix line 319
  34. theorem OAI.Contingency.PaddedGraph.prefix_before_suffix line 328
  35. theorem OAI.Contingency.PaddedGraph.suffix_before line 337
  36. theorem OAI.Contingency.PaddedGraph.slot_cases line 344
  37. def OAI.Contingency.PaddedGraph.contextState line 352
  38. theorem OAI.Contingency.PaddedGraph.contextState_prefix line 357
  39. theorem OAI.Contingency.PaddedGraph.contextState_suffix line 364
  40. theorem OAI.Contingency.PaddedGraph.contextState_supported line 371
  41. theorem OAI.Contingency.PaddedGraph.contextState_injective line 377
  42. theorem OAI.Contingency.PaddedGraph.contextKernel_weight line 388
  43. theorem OAI.Contingency.PaddedGraph.State.ext line 412
  44. theorem OAI.Contingency.PaddedGraph.suffixSlot_val_inj line 418
  45. theorem OAI.Contingency.PaddedGraph.prefix_suffix_ne line 426
  46. theorem OAI.Contingency.PaddedGraph.mixedDisplay_current line 433
  47. theorem OAI.Contingency.PaddedGraph.mixedDisplay_ordinary line 438
  48. def OAI.Contingency.PaddedGraph.defectProfile line 446
  49. theorem OAI.Contingency.PaddedGraph.adjacent_removePair line 448
  50. def OAI.Contingency.PaddedGraph.defectState line 452
  51. theorem OAI.Contingency.PaddedGraph.defectState_current line 455
  52. theorem OAI.Contingency.PaddedGraph.defectState_ordinary line 464
  53. theorem OAI.Contingency.PaddedGraph.defectState_defect line 474
  54. def OAI.Contingency.PaddedGraph.stateSuffix line 510
  55. theorem OAI.Contingency.PaddedGraph.contextState_reconstruct line 516