OAI/Combinatorics/Progressions/Lattices/PhysicalSpatialResidueSupport.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.residueSiteIndicator_affine line 11
  2. def OAI.Erdos3.affineResidueIntervalSiteWeight line 36
  3. theorem OAI.Erdos3.affineResidueIntervalSiteWeight_range line 42
  4. theorem OAI.Erdos3.affineResidueIntervalSiteWeight_pullback line 53
  5. def OAI.Erdos3.affineVectorResidueSiteWeight line 65
  6. theorem OAI.Erdos3.affineVectorResidueSiteWeight_bound line 70
  7. theorem OAI.Erdos3.affineVectorResidueSiteWeight_pullback line 80
  8. theorem OAI.Erdos3.affineVectorResidueSiteWeight_factorization line 101
  9. theorem OAI.Erdos3.vectorIntervalSiteWeight_affine_lipschitz line 111
  10. theorem OAI.Erdos3.affineVectorInterval_normalized_lipschitz line 131
  11. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeVertexValue_residueReconstruction line 157
  12. def OAI.Erdos3.BooleanCubeKernel.physicalResidueStarFactor line 168
  13. def OAI.Erdos3.BooleanCubeKernel.physicalResidueSpatialSiteFactor line 176
  14. theorem OAI.Erdos3.BooleanCubeKernel.physicalResidueSpatialSiteFactor_bound line 183
  15. theorem OAI.Erdos3.BooleanCubeKernel.physicalResidueStarFactor_pullback line 194
  16. theorem OAI.Erdos3.BooleanCubeKernel.physicalResidueSpatialSiteFactor_prod line 216
  17. theorem OAI.Erdos3.BooleanCubeKernel.physicalResidue_spatialSiteExpansion line 232
  18. theorem OAI.Erdos3.BooleanCubeKernel.exists_physicalResidue_spatialSiteExpansion line 257
  19. theorem OAI.Erdos3.BooleanCubeKernel.exists_physicalResidue_coarseSiteExpansion line 297
  20. def OAI.Erdos3.BooleanCubeKernel.physicalResidueQuotient line 352
  21. theorem OAI.Erdos3.BooleanCubeKernel.physicalResidueQuotient_reconstruction line 358
  22. theorem OAI.Erdos3.BooleanCubeKernel.physicalResidueReconstruction_quotient line 369
  23. theorem OAI.Erdos3.BooleanCubeKernel.physicalResidueReconstruction_mem_range_iff line 382
  24. theorem OAI.Erdos3.BooleanCubeKernel.physicalResidueReconstruction_mem_range_star_iff line 395
  25. theorem OAI.Erdos3.BooleanCubeKernel.physicalResidueReconstruction_mem_range_sites_iff line 419
  26. theorem OAI.Erdos3.BooleanCubeKernel.physicalResidueReconstruction_mem_image_iff line 433
  27. theorem OAI.Erdos3.BooleanCubeKernel.affineResidueIntervalSiteWeight_nonzero_residue line 461
  28. theorem OAI.Erdos3.BooleanCubeKernel.affineVectorResidueSiteWeight_nonzero_residue line 481
  29. theorem OAI.Erdos3.BooleanCubeKernel.physicalResidueSpatialSiteFactor_prod_nonzero_mem_range line 493