OAI/Probability/Contingency/OuterAccuracy.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Outer Accuracy.

  1. theorem OAI.Contingency.PaddedGraph.stationary_failure_power line 26
  2. def OAI.Contingency.PaddedGraph.outerDraw line 41
  3. theorem OAI.Contingency.PaddedGraph.outerDraw_bits line 47
  4. theorem OAI.Contingency.PaddedGraph.outerDraw_tv line 57
  5. def OAI.Contingency.PaddedGraph.literalOuter line 107
  6. theorem OAI.Contingency.PaddedGraph.literalOuter_bits line 115
  7. theorem OAI.Contingency.PaddedGraph.literalOuter_tv line 120
  8. def OAI.Contingency.PaddedGraph.EmptyBlock line 144
  9. theorem OAI.Contingency.PaddedGraph.empty_completion_subsingleton line 146
  10. theorem OAI.Contingency.PaddedGraph.empty_weight line 154
  11. def OAI.Contingency.PaddedGraph.emptyCount line 161
  12. theorem OAI.Contingency.PaddedGraph.emptyCount_nonneg line 163
  13. def OAI.Contingency.PaddedGraph.emptyData line 166
  14. theorem OAI.Contingency.PaddedGraph.graphEnergy_le_empty line 188
  15. theorem OAI.Contingency.PaddedGraph.empty_poincare line 220
  16. theorem OAI.Contingency.PaddedGraph.empty_total line 301
  17. theorem OAI.Contingency.PaddedGraph.empty_mixing line 305
  18. theorem OAI.Contingency.DyadicLaw.walk_toLaw_chain line 333
  19. theorem OAI.Contingency.PaddedGraph.smallProposal_bits line 358
  20. theorem OAI.Contingency.PaddedGraph.proposal_pad_bound line 361
  21. theorem OAI.Contingency.PaddedGraph.completion_pure_bits line 366
  22. def OAI.Contingency.PaddedGraph.emptyTransition line 369
  23. theorem OAI.Contingency.PaddedGraph.emptyTransition_bits line 372
  24. theorem OAI.Contingency.PaddedGraph.emptyTransition_toLaw line 377
  25. def OAI.Contingency.PaddedGraph.emptyWalk line 391
  26. theorem OAI.Contingency.PaddedGraph.emptyWalk_toLaw line 395
  27. theorem OAI.Contingency.PaddedGraph.empty_invariant_joint line 400
  28. def OAI.Contingency.PaddedGraph.emptyTrial line 423
  29. theorem OAI.Contingency.PaddedGraph.emptyTrial_bits line 428
  30. theorem OAI.Contingency.PaddedGraph.empty_completion_law line 435
  31. theorem OAI.Contingency.PaddedGraph.emptyTrial_tv line 448
  32. def OAI.Contingency.PaddedGraph.emptyOuter line 484
  33. theorem OAI.Contingency.PaddedGraph.emptyOuter_bits line 490
  34. theorem OAI.Contingency.PaddedGraph.emptyOuter_tv line 499
  35. def OAI.Contingency.Parameters.dim line 538
  36. def OAI.Contingency.Parameters.L line 539
  37. def OAI.Contingency.Parameters.U line 540
  38. def OAI.Contingency.Parameters.cap line 541
  39. def OAI.Contingency.Parameters.bits line 542
  40. theorem OAI.Contingency.Parameters.dimensions line 544
  41. theorem OAI.Contingency.Parameters.cap_pos line 550
  42. theorem OAI.Contingency.Parameters.threshold_le_cap line 552
  43. theorem OAI.Contingency.Parameters.dimension_le_bits line 554
  44. theorem OAI.Contingency.Parameters.cap_pow_bits line 556
  45. theorem OAI.Contingency.Parameters.paddedRow_le_cap line 563
  46. theorem OAI.Contingency.Parameters.bits_le line 589
  47. theorem OAI.Contingency.Parameters.dim_le_size_square line 628