OAI/Probability/BinarySweep/Trajectories/EndpointFactors.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.BinaryCoordinateSweeps.EndpointLineIndex line 20
  2. def OAI.BinaryCoordinateSweeps.endpointPathLine line 22
  3. def OAI.BinaryCoordinateSweeps.endpointLineCount line 25
  4. lemma OAI.BinaryCoordinateSweeps.trackedLineCount_restrict line 30
  5. theorem OAI.BinaryCoordinateSweeps.endpointProbability_zero_scaled line 46
  6. lemma OAI.BinaryCoordinateSweeps.pathLine_occurrences line 71
  7. lemma OAI.BinaryCoordinateSweeps.multilineMoment_X_prod line 90
  8. theorem OAI.BinaryCoordinateSweeps.endpointProbability_zero_polynomial line 98
  9. def OAI.BinaryCoordinateSweeps.Sparse.mobiusSum line 125
  10. lemma OAI.BinaryCoordinateSweeps.Sparse.mobiusSum_empty line 129
  11. lemma OAI.BinaryCoordinateSweeps.Sparse.mobiusSum_congr line 132
  12. lemma OAI.BinaryCoordinateSweeps.Sparse.mobiusSum_sub line 139
  13. lemma OAI.BinaryCoordinateSweeps.Sparse.mobiusSum_insert line 143
  14. lemma OAI.BinaryCoordinateSweeps.Sparse.mobiusSum_union line 157
  15. lemma OAI.BinaryCoordinateSweeps.Sparse.mobiusSum_linear_product line 176