OAI/Probability/Contingency/CompletionTranslation.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Completion Translation.

  1. def OAI.Contingency.CompletionTranslation.adjustment line 16
  2. theorem OAI.Contingency.CompletionTranslation.adjustment_row line 22
  3. theorem OAI.Contingency.CompletionTranslation.adjustment_col line 40
  4. theorem OAI.Contingency.CompletionTranslation.adjustment_neg line 57
  5. def OAI.Contingency.CompletionTranslation.Accepted line 65
  6. instance OAI.Contingency.CompletionTranslation.(instance at line 68) line 68
  7. def OAI.Contingency.CompletionTranslation.translate line 71
  8. theorem OAI.Contingency.CompletionTranslation.translate_value line 94
  9. def OAI.Contingency.CompletionTranslation.translationEquiv line 101
  10. theorem OAI.Contingency.CompletionTranslation.accepted_card_symm line 127
  11. def OAI.Contingency.CompletionTranslation.Rejected line 135
  12. theorem OAI.Contingency.CompletionTranslation.rejection_union_count line 138
  13. theorem OAI.Contingency.CompletionTranslation.rejection_count line 157
  14. theorem OAI.Contingency.CompletionTranslation.accepted_rejected_count line 175
  15. theorem OAI.Contingency.CompletionTranslation.accepted_half line 184
  16. def OAI.Contingency.PaddedGraph.blockRow line 231
  17. def OAI.Contingency.PaddedGraph.blockCol line 234
  18. def OAI.Contingency.PaddedGraph.blockEquiv line 237
  19. theorem OAI.Contingency.PaddedGraph.block_totals line 251
  20. theorem OAI.Contingency.PaddedGraph.block_row_lower line 261
  21. theorem OAI.Contingency.PaddedGraph.block_col_lower line 277
  22. theorem OAI.Contingency.PaddedGraph.block_dimensions line 293
  23. theorem OAI.Contingency.PaddedGraph.block_movement line 302
  24. theorem OAI.Contingency.CompletionTranslation.adjustment_bound line 320
  25. def OAI.Contingency.PaddedGraph.blockD line 354
  26. theorem OAI.Contingency.PaddedGraph.blockD_row line 359
  27. theorem OAI.Contingency.PaddedGraph.blockD_col line 364
  28. theorem OAI.Contingency.PaddedGraph.blockD_reverse line 370
  29. def OAI.Contingency.PaddedGraph.acceptCount line 379
  30. theorem OAI.Contingency.PaddedGraph.acceptCount_symm line 383
  31. theorem OAI.Contingency.PaddedGraph.block_card line 390
  32. theorem OAI.Contingency.PaddedGraph.acceptCount_le line 396
  33. theorem OAI.Contingency.PaddedGraph.acceptCount_half line 401
  34. def OAI.Contingency.PaddedGraph.edgeCount line 430
  35. theorem OAI.Contingency.PaddedGraph.edgeCount_nonneg line 433
  36. theorem OAI.Contingency.PaddedGraph.edgeCount_symm line 436
  37. theorem OAI.Contingency.PaddedGraph.edgeCount_diagonal line 442
  38. theorem OAI.Contingency.PaddedGraph.edgeCount_sum line 445
  39. theorem OAI.Contingency.PaddedGraph.proposal_hold line 459
  40. def OAI.Contingency.PaddedGraph.smallData line 470
  41. theorem OAI.Contingency.PaddedGraph.small_transition_lower line 491
  42. def OAI.Contingency.PaddedGraph.extendGraph line 533
  43. theorem OAI.Contingency.PaddedGraph.extendGraph_apply line 536
  44. lemma OAI.Contingency.PaddedGraph.sum_le_mapped_support line 540
  45. theorem OAI.Contingency.PaddedGraph.graphEdge_value line 569
  46. theorem OAI.Contingency.PaddedGraph.graphEnergy_le_pairs line 582
  47. theorem OAI.Contingency.PaddedGraph.graphEnergy_le_ordered line 599
  48. theorem OAI.Contingency.PaddedGraph.graphEnergy_le_accepted line 620