OAI/Geometry/LatticeCovering/Products.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SingleLatticeCovering.LatticeGeometry.appendEquiv line 42
  2. lemma OAI.SingleLatticeCovering.LatticeGeometry.appendEquiv_apply line 53
  3. lemma OAI.SingleLatticeCovering.LatticeGeometry.appendEquiv_symm_apply line 55
  4. instance OAI.SingleLatticeCovering.LatticeGeometry.prod_discrete line 62
  5. instance OAI.SingleLatticeCovering.LatticeGeometry.prod_full line 66
  6. def OAI.SingleLatticeCovering.LatticeGeometry.prodSubtypeEquiv line 75
  7. abbrev OAI.SingleLatticeCovering.LatticeGeometry.finProduct line 84
  8. lemma OAI.SingleLatticeCovering.LatticeGeometry.mem_finProduct line 88
  9. instance OAI.SingleLatticeCovering.LatticeGeometry.finProduct_discrete line 93
  10. instance OAI.SingleLatticeCovering.LatticeGeometry.finProduct_full line 100
  11. def OAI.SingleLatticeCovering.LatticeGeometry.finProductBasis line 107
  12. lemma OAI.SingleLatticeCovering.LatticeGeometry.finProduct_covolume line 113
  13. abbrev OAI.SingleLatticeCovering.LatticeGeometry.image line 142
  14. instance OAI.SingleLatticeCovering.LatticeGeometry.image_discrete line 145
  15. instance OAI.SingleLatticeCovering.LatticeGeometry.image_full line 150
  16. lemma OAI.SingleLatticeCovering.LatticeGeometry.mem_image line 155
  17. lemma OAI.SingleLatticeCovering.LatticeGeometry.image_covolume line 162
  18. def OAI.SingleLatticeCovering.LatticeGeometry.triangular line 182
  19. lemma OAI.SingleLatticeCovering.LatticeGeometry.triangular_append line 225
  20. lemma OAI.SingleLatticeCovering.LatticeGeometry.single_left line 232
  21. lemma OAI.SingleLatticeCovering.LatticeGeometry.single_right line 239
  22. lemma OAI.SingleLatticeCovering.LatticeGeometry.triangular_det line 246
  23. theorem OAI.SingleLatticeCovering.LatticeGeometry.triangular_lattice_covolume line 266
  24. instance OAI.SingleLatticeCovering.Vertical.Block.lattice_discrete line 285
  25. instance OAI.SingleLatticeCovering.Vertical.Block.lattice_full line 287
  26. lemma OAI.SingleLatticeCovering.Vertical.Block.lattice_covolume line 289
  27. def OAI.SingleLatticeCovering.Vertical.Block.linear line 292
  28. lemma OAI.SingleLatticeCovering.Vertical.Block.linear_apply line 294
  29. lemma OAI.SingleLatticeCovering.Vertical.Block.linear_det line 295
  30. lemma OAI.SingleLatticeCovering.Vertical.Block.physical_covolume line 299
  31. def OAI.SingleLatticeCovering.Vertical.Block.shiftMap line 304
  32. lemma OAI.SingleLatticeCovering.Vertical.Block.shiftMap_apply line 306
  33. def OAI.SingleLatticeCovering.Vertical.Chain.injectLast line 320
  34. lemma OAI.SingleLatticeCovering.Vertical.Chain.subLast_eq_sub line 324
  35. abbrev OAI.SingleLatticeCovering.Vertical.Chain.rawLattice line 332
  36. instance OAI.SingleLatticeCovering.Vertical.Chain.raw_discrete line 335
  37. instance OAI.SingleLatticeCovering.Vertical.Chain.raw_full line 339
  38. lemma OAI.SingleLatticeCovering.Vertical.Chain.mem_raw line 343
  39. def OAI.SingleLatticeCovering.Vertical.Chain.linear line 348
  40. def OAI.SingleLatticeCovering.Vertical.Chain.det line 352
  41. abbrev OAI.SingleLatticeCovering.Vertical.Chain.physicalLattice line 355
  42. lemma OAI.SingleLatticeCovering.Vertical.Chain.physical_covolume line 357
  43. lemma OAI.SingleLatticeCovering.Vertical.Chain.residual_append line 366
  44. lemma OAI.SingleLatticeCovering.Vertical.Chain.gamma_append line 379
  45. lemma OAI.SingleLatticeCovering.Vertical.Chain.weight_eq line 385
  46. lemma OAI.SingleLatticeCovering.Vertical.binaryExpansion line 403
  47. def OAI.SingleLatticeCovering.Vertical.terminalColumns line 421
  48. theorem OAI.SingleLatticeCovering.Vertical.terminal_exhaustion line 426
  49. abbrev OAI.SingleLatticeCovering.Vertical.integerLattice line 461
  50. lemma OAI.SingleLatticeCovering.Vertical.integerLattice_covolume line 463
  51. lemma OAI.SingleLatticeCovering.Vertical.integer_mem line 471
  52. abbrev OAI.SingleLatticeCovering.Vertical.Block.terminalDim line 477
  53. def OAI.SingleLatticeCovering.Vertical.Block.shiftDim line 479
  54. def OAI.SingleLatticeCovering.Vertical.Block.shiftDimMap line 482
  55. lemma OAI.SingleLatticeCovering.Vertical.Block.shiftDimMap_apply line 484
  56. lemma OAI.SingleLatticeCovering.Vertical.Block.shiftDim_grid_bits line 494
  57. abbrev OAI.SingleLatticeCovering.Vertical.Block.terminalShift line 525
  58. lemma OAI.SingleLatticeCovering.Vertical.Block.terminal_index line 530
  59. abbrev OAI.SingleLatticeCovering.Vertical.Chain.fullDim line 558
  60. abbrev OAI.SingleLatticeCovering.Vertical.Chain.FullVec line 559
  61. abbrev OAI.SingleLatticeCovering.Vertical.Chain.fullRaw line 560
  62. def OAI.SingleLatticeCovering.Vertical.Chain.fullLinear line 561
  63. abbrev OAI.SingleLatticeCovering.Vertical.Chain.fullLattice line 563
  64. lemma OAI.SingleLatticeCovering.Vertical.Chain.full_covolume line 565
  65. lemma OAI.SingleLatticeCovering.Vertical.Chain.full_residual line 573
  66. lemma OAI.SingleLatticeCovering.Vertical.Chain.full_weight line 582
  67. def OAI.SingleLatticeCovering.Vertical.Block.Selected line 600
  68. lemma OAI.SingleLatticeCovering.Vertical.Block.cell_selected line 605
  69. lemma OAI.SingleLatticeCovering.Vertical.Block.selected_weight_le line 631
  70. def OAI.SingleLatticeCovering.Vertical.Chain.Selected line 642
  71. lemma OAI.SingleLatticeCovering.Vertical.Chain.base_pattern_selected line 650
  72. theorem OAI.SingleLatticeCovering.Vertical.Chain.truncated_patterns_selected line 683