OAI/Combinatorics/BooleanFunctions/SoftEvent.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SquareRootDegree.SoftEvent.average_div_const line 18
  2. def OAI.SquareRootDegree.SoftEvent.rawMoments line 22
  3. theorem OAI.SquareRootDegree.SoftEvent.weighted_shifted_sq line 26
  4. theorem OAI.SquareRootDegree.SoftEvent.weighted_deficit line 49
  5. theorem OAI.SquareRootDegree.SoftEvent.prod_set_one line 59
  6. theorem OAI.SquareRootDegree.SoftEvent.sum_set_zero line 67
  7. def OAI.SquareRootDegree.SoftEvent.without line 75
  8. theorem OAI.SquareRootDegree.SoftEvent.weighted_deficit_without line 77
  9. def OAI.SquareRootDegree.SoftEvent.softWeight line 122
  10. def OAI.SquareRootDegree.SoftEvent.deficit line 125
  11. theorem OAI.SquareRootDegree.SoftEvent.quadratic_average line 129
  12. theorem OAI.SquareRootDegree.SoftEvent.soft_deficit_eq_gain line 136