OAI/Probability/Contingency/SmallPoincare.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

Small Poincare.

  1. theorem OAI.Contingency.PaddedGraph.smallDim_one line 21
  2. theorem OAI.Contingency.PaddedGraph.small_poincare line 26
  3. def OAI.Contingency.PaddedGraph.smallPart line 101
  4. theorem OAI.Contingency.PaddedGraph.table_row_bound line 104
  5. theorem OAI.Contingency.PaddedGraph.table_col_bound line 108
  6. theorem OAI.Contingency.PaddedGraph.smallPart_bounds line 112
  7. theorem OAI.Contingency.PaddedGraph.smallPart_row line 124
  8. theorem OAI.Contingency.PaddedGraph.smallPart_col line 138
  9. def OAI.Contingency.PaddedGraph.initialTransversal line 154
  10. theorem OAI.Contingency.PaddedGraph.transverse_nonempty line 162
  11. theorem OAI.Contingency.PaddedGraph.graph_nonempty line 166
  12. def OAI.Contingency.PaddedGraph.transverseMass line 182
  13. def OAI.Contingency.PaddedGraph.graphMass line 183
  14. theorem OAI.Contingency.PaddedGraph.transverseMass_pos line 185
  15. def OAI.Contingency.PaddedGraph.taggedState line 192
  16. theorem OAI.Contingency.PaddedGraph.taggedState_injective line 195
  17. theorem OAI.Contingency.PaddedGraph.defectMass_le line 202
  18. theorem OAI.Contingency.PaddedGraph.graphMass_bounds line 218
  19. abbrev OAI.Contingency.PaddedGraph.Joint line 244
  20. instance OAI.Contingency.PaddedGraph.(instance at line 246) line 246
  21. theorem OAI.Contingency.PaddedGraph.joint_card line 250
  22. def OAI.Contingency.PaddedGraph.jointCoordinates line 258
  23. theorem OAI.Contingency.PaddedGraph.jointCoordinates_injective line 261
  24. def OAI.Contingency.PaddedGraph.jointCode line 296
  25. theorem OAI.Contingency.PaddedGraph.jointCode_injective line 304
  26. theorem OAI.Contingency.PaddedGraph.graphMass_upper line 317
  27. theorem OAI.Contingency.PaddedGraph.stationary_lower line 326
  28. theorem OAI.Contingency.PaddedGraph.small_total line 356
  29. theorem OAI.Contingency.PaddedGraph.small_mixing line 361
  30. lemma OAI.Contingency.PaddedGraph.comp_nonempty line 396
  31. lemma OAI.Contingency.PaddedGraph.blockRow_upper line 399
  32. abbrev OAI.Contingency.PaddedGraph.blockDraw line 414
  33. theorem OAI.Contingency.PaddedGraph.blockDraw_bits line 426
  34. theorem OAI.Contingency.PaddedGraph.blockDraw_tv line 431
  35. theorem OAI.Contingency.Law.uniform_event line 455
  36. lemma OAI.Contingency.PaddedGraph.proposal_degree line 478
  37. abbrev OAI.Contingency.PaddedGraph.smallProposal line 484
  38. def OAI.Contingency.PaddedGraph.completionTest line 488
  39. def OAI.Contingency.PaddedGraph.completionKernel line 491
  40. def OAI.Contingency.PaddedGraph.implementedTransition line 495
  41. theorem OAI.Contingency.PaddedGraph.implementedTransition_bits line 502
  42. theorem OAI.Contingency.PaddedGraph.toLaw_implementedTransition line 506
  43. theorem OAI.Contingency.PaddedGraph.completionKernel_tv line 514
  44. abbrev OAI.Contingency.PaddedGraph.idealCompletion line 522
  45. theorem OAI.Contingency.PaddedGraph.idealCompletion_test line 525
  46. theorem OAI.Contingency.PaddedGraph.idealCompletion_kernel line 543
  47. theorem OAI.Contingency.DyadicLaw.walk_tv_chain line 571
  48. abbrev OAI.Contingency.PaddedGraph.implementedWalk line 592
  49. theorem OAI.Contingency.PaddedGraph.implementedWalk_tv line 598