OAI/Combinatorics/BooleanFunctions/Grouping.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SquareRootDegree.Observations.eventCongr line 18
  2. theorem OAI.SquareRootDegree.Observations.deficit_equiv line 21
  3. def OAI.SquareRootDegree.Observations.groupScale line 31
  4. def OAI.SquareRootDegree.Observations.groupStandard line 32
  5. theorem OAI.SquareRootDegree.Observations.groupScale_sq line 36
  6. theorem OAI.SquareRootDegree.Observations.grouped_score_scaled line 41
  7. theorem OAI.SquareRootDegree.Observations.groupStandard_zero line 53
  8. theorem OAI.SquareRootDegree.Observations.groupStandard_sq line 60
  9. theorem OAI.SquareRootDegree.Observations.exists_amplification line 71