OAI/Probability/BinarySweep/Trajectories/FallingMoment.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryCoordinateSweeps.Sparse.fallingMoment line 15
  2. lemma OAI.BinaryCoordinateSweeps.Sparse.fallingMoment_zero line 17
  3. lemma OAI.BinaryCoordinateSweeps.Sparse.fallingMoment_pos line 20
  4. lemma OAI.BinaryCoordinateSweeps.Sparse.fallingMoment_succ line 25
  5. def OAI.BinaryCoordinateSweeps.Sparse.lineMoment line 38
  6. lemma OAI.BinaryCoordinateSweeps.Sparse.lineMoment_monomial line 41
  7. lemma OAI.BinaryCoordinateSweeps.Sparse.lineMoment_X_pow line 45
  8. def OAI.BinaryCoordinateSweeps.Sparse.stein line 49
  9. lemma OAI.BinaryCoordinateSweeps.Sparse.stein_apply line 54
  10. lemma OAI.BinaryCoordinateSweeps.Sparse.lineMoment_stein_monomial line 57
  11. lemma OAI.BinaryCoordinateSweeps.lineLaw_zero line 77
  12. lemma OAI.BinaryCoordinateSweeps.assignmentWeight_uniform_of_eq line 81
  13. lemma OAI.BinaryCoordinateSweeps.localPathWeight_zero line 92
  14. lemma OAI.BinaryCoordinateSweeps.card_fin_sum_pred line 107
  15. def OAI.BinaryCoordinateSweeps.trackedLineCount line 119
  16. lemma OAI.BinaryCoordinateSweeps.lineHoles_augment line 124
  17. lemma OAI.BinaryCoordinateSweeps.uniform_extension_ratio line 150
  18. theorem OAI.BinaryCoordinateSweeps.placementProbability_zero_factor line 160
  19. lemma OAI.BinaryCoordinateSweeps.sum_trackedLineCount line 174
  20. theorem OAI.BinaryCoordinateSweeps.placementProbability_zero_scaled line 185