OAI/Combinatorics/Progressions/Linear/PhysicalCubeMatrix.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.BooleanCubeKernel.physicalCubeCoefficient line 11
  2. def OAI.Erdos3.BooleanCubeKernel.physicalCubeOffset line 18
  3. def OAI.Erdos3.BooleanCubeKernel.physicalCubeRootDifferences line 22
  4. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeRootDifferences_root line 27
  5. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeRootDifferences_direction line 35
  6. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeRootDifferences_vertex line 41
  7. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeRootDifferences_star line 56
  8. def OAI.Erdos3.BooleanCubeKernel.physicalCubeBlockMatrix line 63
  9. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeBlockMatrix_mulVec line 67
  10. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeRootDifferences_matrix line 74