OAI/Combinatorics/Progressions/Linear/ContainedKernelPhysicalDisplacement.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.fixedSpatialKernelMap line 12
  2. theorem OAI.Erdos3.fixedSpatialKernelMap_lipschitz line 16
  3. theorem OAI.Erdos3.fixedSpatialKernelMap_lipschitz_one line 42
  4. theorem OAI.Erdos3.fixedSpatialKernelMap_integer line 55
  5. def OAI.Erdos3.fixedSpatialKernelBlock line 86
  6. def OAI.Erdos3.fixedSpatialKernelRest line 90
  7. theorem OAI.Erdos3.fixedSpatialKernelRest_measurable line 95
  8. theorem OAI.Erdos3.fixedSpatialKernelMap_blocks line 101
  9. theorem OAI.Erdos3.fixedSpatialKernelMap_blocks_actual line 117
  10. theorem OAI.Erdos3.rectangularWeightIndices_normalized_norm_le line 148
  11. theorem OAI.Erdos3.selectedResidueSmoothPMF_normalized_norm_le line 157
  12. theorem OAI.Erdos3.fixedSpatialKernelMap_narrow_physical_dist line 175
  13. theorem OAI.Erdos3.fixedSpatialKernelMap_narrow_physical_test_error line 210
  14. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedSpatialKernelMap_narrow_physical_dist line 243
  15. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedSpatialKernelMap_supported_narrow_physical_dist line 269
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedFixedSpatialKernelMap_supported_narrow_physical_test_error line 288
  17. def OAI.Erdos3.fixedSpatialKernelBlockCoordinates line 323
  18. theorem OAI.Erdos3.fixedSpatialKernelBlockCoordinates_measurePreserving line 328
  19. theorem OAI.Erdos3.fixedSpatialKernelBlockCoordinates_image_law line 342
  20. theorem OAI.Erdos3.fixedSpatialKernelMap_block_image_law line 349
  21. def OAI.Erdos3.fixedSpatialKernelSliceFrame line 388
  22. theorem OAI.Erdos3.fixedSpatialKernelSliceFrame_none line 394
  23. theorem OAI.Erdos3.fixedSpatialKernelSliceFrame_some line 399
  24. theorem OAI.Erdos3.fixedSpatialKernelMap_slice line 404
  25. theorem OAI.Erdos3.fixedSpatialKernelBlock_slice line 417
  26. theorem OAI.Erdos3.fixedSpatialKernelBlock_slice_det line 426
  27. theorem OAI.Erdos3.fixedSpatialKernelBlock_slice_det_ne_zero line 441
  28. def OAI.Erdos3.containedKernelCubeMap line 464
  29. theorem OAI.Erdos3.containedKernelCubeMap_value line 471
  30. theorem OAI.Erdos3.containedKernelCubeMap_normalized line 491
  31. theorem OAI.Erdos3.VectorPolynomial.allocatedContainedKernel_supported_narrow_physical_dist line 518