OAI/Combinatorics/Progressions/Geometry/PrincipalSpatialSiteComparison.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.rootDifferenceMatrix_vertex line 13
  2. theorem OAI.Erdos3.integerAffineCube_shifted_scalar line 25
  3. theorem OAI.Erdos3.scalarCubeWindow_root_bound line 34
  4. theorem OAI.Erdos3.affineScalarCubeWindowWeights_root_bound line 43
  5. def OAI.Erdos3.scalarTupleColumn line 67
  6. def OAI.Erdos3.scalarTupleSpatialColumns line 70
  7. theorem OAI.Erdos3.scalarTupleColumn_residue_iff line 74
  8. theorem OAI.Erdos3.scalarTupleColumn_bound line 88
  9. theorem OAI.Erdos3.scalarTupleSpatialColumns_scaled_bound line 98
  10. theorem OAI.Erdos3.scalarTupleSpatialColumns_vertex line 107
  11. def OAI.Erdos3.principalSpatialColumns line 131
  12. def OAI.Erdos3.principalSpatialResidueColumns line 136
  13. theorem OAI.Erdos3.principalSpatialColumns_residue line 142
  14. theorem OAI.Erdos3.principalSpatialColumns_scaled_bound line 151
  15. theorem OAI.Erdos3.principalSpatialColumns_vertex line 159
  16. theorem OAI.Erdos3.smoothVectorSpatial_site_error line 178
  17. theorem OAI.Erdos3.principalVectorSpatial_site_error line 248