OAI/Probability/BinarySweep/Processes/CoordinateLayerEdgeSwap.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryCoordinateSweeps.coordinateLayer_edgeSwap line 11
  2. lemma OAI.BinaryCoordinateSweeps.swap_update_mem_reachable line 28
  3. lemma OAI.BinaryCoordinateSweeps.swap_mem_sweepReachable line 39
  4. theorem OAI.BinaryCoordinateSweeps.every_permutation_sweepReachable line 60
  5. def OAI.BinaryCoordinateSweeps.IsProbability line 71
  6. lemma OAI.BinaryCoordinateSweeps.sum_mulLeft line 73
  7. lemma OAI.BinaryCoordinateSweeps.sum_inv_mulRight line 76
  8. lemma OAI.BinaryCoordinateSweeps.convolution_sum line 79
  9. lemma OAI.BinaryCoordinateSweeps.convolution_nonneg line 86
  10. lemma OAI.BinaryCoordinateSweeps.convolution_probability line 90
  11. lemma OAI.BinaryCoordinateSweeps.convolution_uniform_right line 94
  12. lemma OAI.BinaryCoordinateSweeps.convolution_uniform_left line 99
  13. lemma OAI.BinaryCoordinateSweeps.convolution_assoc line 104
  14. lemma OAI.BinaryCoordinateSweeps.totalVariation_nonneg line 115
  15. lemma OAI.BinaryCoordinateSweeps.totalVariation_le_one line 119
  16. lemma OAI.BinaryCoordinateSweeps.convolution_tv_contract line 129
  17. abbrev OAI.BinaryCoordinateSweeps.GridSlot line 154
  18. abbrev OAI.BinaryCoordinateSweeps.GridOutside line 155
  19. abbrev OAI.BinaryCoordinateSweeps.GridChoices line 157
  20. def OAI.BinaryCoordinateSweeps.gridSize line 160
  21. lemma OAI.BinaryCoordinateSweeps.card_gridSlot line 162
  22. def OAI.BinaryCoordinateSweeps.gridLayer line 166
  23. def OAI.BinaryCoordinateSweeps.gridSweep line 171
  24. def OAI.BinaryCoordinateSweeps.lineLaw line 174
  25. def OAI.BinaryCoordinateSweeps.gridWeight line 177
  26. structure OAI.BinaryCoordinateSweeps.PathFamily line 180
  27. def OAI.BinaryCoordinateSweeps.pathEvent line 186
  28. lemma OAI.BinaryCoordinateSweeps.chronological_trajectory line 191