OAI/Combinatorics/BooleanFunctions/Blocks.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Disjoint blocks and finite observation degree calculus

  1. def OAI.SquareRootDegree.blockCurry line 15
  2. theorem OAI.SquareRootDegree.average_pi_prod line 21
  3. theorem OAI.SquareRootDegree.average_pi_eval line 26
  4. theorem OAI.SquareRootDegree.fourierDegree_comp_coordinates_le line 34
  5. theorem OAI.SquareRootDegree.fourierDegree_comp_observation_le line 55
  6. theorem OAI.SquareRootDegree.cell_tuple line 66
  7. theorem OAI.SquareRootDegree.fourierDegree_comp_tuple_le line 84
  8. theorem OAI.SquareRootDegree.fourierDegree_block_cell_le line 98