OAI/Probability/BinarySweep/FiniteLaws/FiniteProductProbability.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinaryCoordinateSweeps.Sparse.productWeight line 11
  2. def OAI.BinaryCoordinateSweeps.Sparse.productProbability line 13
  3. lemma OAI.BinaryCoordinateSweeps.Sparse.productWeight_nonneg line 17
  4. lemma OAI.BinaryCoordinateSweeps.Sparse.productWeight_sum line 20
  5. lemma OAI.BinaryCoordinateSweeps.Sparse.indicator_prod line 27
  6. lemma OAI.BinaryCoordinateSweeps.Sparse.productWeight_split line 37
  7. lemma OAI.BinaryCoordinateSweeps.Sparse.productProbability_nonneg line 51
  8. lemma OAI.BinaryCoordinateSweeps.Sparse.productProbability_mono line 57
  9. lemma OAI.BinaryCoordinateSweeps.Sparse.productProbability_union_le line 67
  10. theorem OAI.BinaryCoordinateSweeps.Sparse.depthOne_probability_le line 84