OAI/Probability/BinarySweep/Processes/AssignmentWeight.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryCoordinateSweeps.assignmentWeight line 14
  2. lemma OAI.BinaryCoordinateSweeps.assignmentWeight_mono line 18
  3. lemma OAI.BinaryCoordinateSweeps.assignmentWeight_nonneg line 28
  4. lemma OAI.BinaryCoordinateSweeps.assignmentWeight_smul line 37
  5. lemma OAI.BinaryCoordinateSweeps.assignmentWeight_uniform line 44
  6. lemma OAI.BinaryCoordinateSweeps.assignmentWeight_uniform_pos line 49
  7. lemma OAI.BinaryCoordinateSweeps.assignmentWeight_comparison line 55
  8. lemma OAI.BinaryCoordinateSweeps.assignmentWeight_ratio_le line 69
  9. abbrev OAI.BinaryCoordinateSweeps.LinePaths line 98
  10. def OAI.BinaryCoordinateSweeps.lineInput line 102
  11. def OAI.BinaryCoordinateSweeps.lineOutput line 113
  12. lemma OAI.BinaryCoordinateSweeps.lineHoles_le line 125
  13. lemma OAI.BinaryCoordinateSweeps.sum_lineHoles line 130
  14. lemma OAI.BinaryCoordinateSweeps.pathCost_nonneg line 137
  15. lemma OAI.BinaryCoordinateSweeps.pathCost_le line 145
  16. lemma OAI.BinaryCoordinateSweeps.pathEvent_iff_assigns line 156
  17. lemma OAI.BinaryCoordinateSweeps.finiteLaw_le_one line 175
  18. def OAI.BinaryCoordinateSweeps.linePerturbationRadius line 181
  19. lemma OAI.BinaryCoordinateSweeps.linePerturbationRadius_pos line 183
  20. lemma OAI.BinaryCoordinateSweeps.lineLaw_comparison line 187