OAI/Combinatorics/Progressions/Lattices/PhysicalResidueOffsetShift.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.BooleanCubeKernel.physicalCubeResidueCoordinates line 12
  2. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeRootDifferences_residue line 19
  3. def OAI.Erdos3.BooleanCubeKernel.physicalCubeResidueLaw line 34
  4. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeResidueLaw_eq_map line 43
  5. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeResidueLaw_expectation line 57
  6. def OAI.Erdos3.BooleanCubeKernel.physicalCubeIndexCoordinates line 81
  7. def OAI.Erdos3.BooleanCubeKernel.physicalResidueReconstruct line 85
  8. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeResidueCoordinates_index line 91
  9. theorem OAI.Erdos3.BooleanCubeKernel.physicalResidue_index_test_error line 102
  10. theorem OAI.Erdos3.BooleanCubeKernel.selectedResidue_physical_index_test_error line 124
  11. def OAI.Erdos3.BooleanCubeKernel.physicalResidueCoordinateMap line 168
  12. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeResidueCoordinates_grouped line 175
  13. def OAI.Erdos3.BooleanCubeKernel.physicalResidueCoordinateLaw line 188
  14. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeResidueLaw_product line 201
  15. theorem OAI.Erdos3.BooleanCubeKernel.physicalSelectedResidue_recenter_test line 226
  16. theorem OAI.Erdos3.BooleanCubeKernel.trimmedSpatial_residue_width_lower line 248
  17. theorem OAI.Erdos3.BooleanCubeKernel.physicalSelectedResidue_trimmed_recenter line 260
  18. def OAI.Erdos3.BooleanCubeKernel.physicalRecenteringScale line 299
  19. theorem OAI.Erdos3.BooleanCubeKernel.physicalSelectedResidue_prescribed_recenter line 304
  20. def OAI.Erdos3.BooleanCubeKernel.physicalResidueReconstruction line 362
  21. theorem OAI.Erdos3.BooleanCubeKernel.physicalResidueReconstruction_centered line 368
  22. theorem OAI.Erdos3.BooleanCubeKernel.smoothPhysicalResidue_finite_expectation line 376
  23. theorem OAI.Erdos3.BooleanCubeKernel.smoothPhysicalResidue_site_error line 395
  24. theorem OAI.Erdos3.BooleanCubeKernel.physicalSelectedResidue_width_recenter line 428
  25. def OAI.Erdos3.BooleanCubeKernel.physicalResidueOffsetShift line 471
  26. theorem OAI.Erdos3.BooleanCubeKernel.physicalResidueOffsetShift_mem line 477
  27. theorem OAI.Erdos3.BooleanCubeKernel.physicalResidueReconstruction_offset_shift line 485
  28. theorem OAI.Erdos3.BooleanCubeKernel.physicalResidueOffsetShift_bound line 505
  29. theorem OAI.Erdos3.BooleanCubeKernel.physicalResidue_test_reference_offset line 515