OAI/Probability/BinarySweep/Processes/GridSweepPath.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BinaryCoordinateSweeps.gridSweep_path line 11
  2. abbrev OAI.BinaryCoordinateSweeps.FreeSlot line 16
  3. instance OAI.BinaryCoordinateSweeps.freeSlotFintype line 19
  4. lemma OAI.BinaryCoordinateSweeps.card_freeSlot line 22
  5. def OAI.BinaryCoordinateSweeps.freeIdentification line 34
  6. def OAI.BinaryCoordinateSweeps.remainingBijection line 38
  7. def OAI.BinaryCoordinateSweeps.remainingPerm line 53
  8. def OAI.BinaryCoordinateSweeps.conditionalNormalizer line 57
  9. def OAI.BinaryCoordinateSweeps.conditionalOperator line 62
  10. def OAI.BinaryCoordinateSweeps.lineHoles line 71
  11. def OAI.BinaryCoordinateSweeps.pathCost line 77
  12. def OAI.BinaryCoordinateSweeps.ConditionalMomentTarget line 82
  13. theorem OAI.BinaryCoordinateSweeps.pathEvent_nonempty line 92
  14. lemma OAI.BinaryCoordinateSweeps.lineLaw_pos line 127
  15. lemma OAI.BinaryCoordinateSweeps.lineLaw_sum line 136
  16. lemma OAI.BinaryCoordinateSweeps.gridWeight_pos line 141
  17. lemma OAI.BinaryCoordinateSweeps.gridWeight_sum line 147
  18. theorem OAI.BinaryCoordinateSweeps.conditionalNormalizer_pos line 160
  19. lemma OAI.BinaryCoordinateSweeps.uniformLaw_probability line 173
  20. lemma OAI.BinaryCoordinateSweeps.convolution_sub_left line 176
  21. lemma OAI.BinaryCoordinateSweeps.convolution_smul_left line 181
  22. lemma OAI.BinaryCoordinateSweeps.convolution_uniform_right_mass line 186
  23. lemma OAI.BinaryCoordinateSweeps.convolution_minorization line 191