OAI/Geometry/LatticeCovering/PrimeKernels.lean

GitHub source file

57 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SingleLatticeCovering.PrimeKernel.scaleFactor line 40
  2. lemma OAI.SingleLatticeCovering.PrimeKernel.scaleFactor_pos line 41
  3. def OAI.SingleLatticeCovering.PrimeKernel.normalizeEquiv line 44
  4. lemma OAI.SingleLatticeCovering.PrimeKernel.normalizeEquiv_det line 47
  5. abbrev OAI.SingleLatticeCovering.PrimeKernel.normalized line 58
  6. lemma OAI.SingleLatticeCovering.PrimeKernel.covolume_normalized line 61
  7. def OAI.SingleLatticeCovering.PrimeKernel.gridMap line 68
  8. lemma OAI.SingleLatticeCovering.PrimeKernel.gridMap_injective line 79
  9. def OAI.SingleLatticeCovering.PrimeKernel.modForm line 85
  10. lemma OAI.SingleLatticeCovering.PrimeKernel.grid_mem_normalized_iff line 92
  11. lemma OAI.SingleLatticeCovering.PrimeKernel.exists_grid_of_mem line 100
  12. def OAI.SingleLatticeCovering.PrimeKernel.kernelEquiv line 110
  13. def OAI.SingleLatticeCovering.PrimeKernel.rectangularCell line 133
  14. lemma OAI.SingleLatticeCovering.PrimeKernel.mem_rectangularCell_iff line 136
  15. lemma OAI.SingleLatticeCovering.PrimeKernel.rectangularCell_measurable line 140
  16. lemma OAI.SingleLatticeCovering.PrimeKernel.integer_displacement_unique line 143
  17. lemma OAI.SingleLatticeCovering.PrimeKernel.rectangularCell_exists_shift line 186
  18. lemma OAI.SingleLatticeCovering.PrimeKernel.rectangularCell_fundamental line 227
  19. abbrev OAI.SingleLatticeCovering.PrimeKernel.normalizedRectangularCell line 248
  20. lemma OAI.SingleLatticeCovering.PrimeKernel.normalizedRectangularCell_fundamental line 251
  21. lemma OAI.SingleLatticeCovering.PrimeKernel.rectangularCell_bounded line 266
  22. lemma OAI.SingleLatticeCovering.PrimeKernel.normalizedRectangularCell_measurable line 272
  23. lemma OAI.SingleLatticeCovering.PrimeKernel.volume_rectangularCell line 277
  24. lemma OAI.SingleLatticeCovering.PrimeKernel.volume_normalizedRectangularCell line 287
  25. def OAI.SingleLatticeCovering.PrimeKernel.gridUnitCell line 306
  26. def OAI.SingleLatticeCovering.PrimeKernel.offsetVector line 307
  27. def OAI.SingleLatticeCovering.PrimeKernel.offsetCell line 309
  28. lemma OAI.SingleLatticeCovering.PrimeKernel.volume_gridUnitCell line 312
  29. lemma OAI.SingleLatticeCovering.PrimeKernel.volume_offsetCell line 316
  30. lemma OAI.SingleLatticeCovering.PrimeKernel.rectangularCell_unit_decomposition line 325
  31. lemma OAI.SingleLatticeCovering.PrimeKernel.normalizedRectangularCell_subset_offsetCells line 354
  32. lemma OAI.SingleLatticeCovering.PrimeKernel.modForm_offsetVector line 363
  33. lemma OAI.SingleLatticeCovering.PrimeKernel.offsetCell_hit line 376
  34. def OAI.SingleLatticeCovering.PrimeKernel.badOffsets line 410
  35. lemma OAI.SingleLatticeCovering.PrimeKernel.cell_hole_le_badOffsets line 414
  36. lemma OAI.SingleLatticeCovering.RogersPreparation.pointCount_zero_iff_no_hit line 441
  37. lemma OAI.SingleLatticeCovering.RogersPreparation.hole_eq_unit_fundamental_hole line 452
  38. def OAI.SingleLatticeCovering.PrimeKernel.normalizedFull line 479
  39. lemma OAI.SingleLatticeCovering.PrimeKernel.normalizedFull_hole_le_badOffsets line 482
  40. def OAI.SingleLatticeCovering.AffineVoid.normalDual line 499
  41. def OAI.SingleLatticeCovering.AffineVoid.fullMiss line 502
  42. def OAI.SingleLatticeCovering.AffineVoid.normalizedMiss line 506
  43. lemma OAI.SingleLatticeCovering.AffineVoid.fullMiss_nonneg line 510
  44. lemma OAI.SingleLatticeCovering.AffineVoid.normalizedMiss_nonneg line 515
  45. lemma OAI.SingleLatticeCovering.AffineVoid.normalDual_injective line 521
  46. lemma OAI.SingleLatticeCovering.AffineVoid.normalDual_dot line 540
  47. lemma OAI.SingleLatticeCovering.AffineVoid.fullMiss_normalDual line 547
  48. lemma OAI.SingleLatticeCovering.AffineVoid.raw_conditioning_bound line 562
  49. def OAI.SingleLatticeCovering.AffineVoid.meanFull line 579
  50. def OAI.SingleLatticeCovering.AffineVoid.meanNormalized line 581
  51. lemma OAI.SingleLatticeCovering.AffineVoid.conditioning_bound line 584
  52. lemma OAI.SingleLatticeCovering.ConvexCore.interior_nonempty_of_volume_pos line 611
  53. lemma OAI.SingleLatticeCovering.ConvexCore.core_subset_interior line 622
  54. lemma OAI.SingleLatticeCovering.ConvexCore.core_compact line 629
  55. lemma OAI.SingleLatticeCovering.ConvexCore.core_volume line 633
  56. lemma OAI.SingleLatticeCovering.ConvexCore.compact_uniform_add line 640
  57. lemma OAI.SingleLatticeCovering.ConvexCore.exists_shrink_exp line 648