OAI/Combinatorics/Progressions/Lattices/NormalizedLatticeSheet.lean

GitHub source file

61 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.latticeBasisEquiv line 21
  2. theorem OAI.Erdos3.latticeBasisEquiv_coordinates line 26
  3. theorem OAI.Erdos3.latticeBasisEquiv_synthesis line 36
  4. theorem OAI.Erdos3.exists_primitive_lattice_normal line 54
  5. def OAI.Erdos3.euclideanDualLattice line 103
  6. theorem OAI.Erdos3.mem_euclideanDualLattice line 106
  7. theorem OAI.Erdos3.realInner_nondegenerate line 112
  8. theorem OAI.Erdos3.euclideanDualLattice_eq_span_dualBasis line 121
  9. instance OAI.Erdos3.euclideanDualLattice_discrete line 130
  10. instance OAI.Erdos3.euclideanDualLattice_isZLattice line 135
  11. theorem OAI.Erdos3.euclideanDualLattice_involutive line 141
  12. theorem OAI.Erdos3.exists_bounded_primitive_lattice_normal line 158
  13. def OAI.Erdos3.latticeSection line 183
  14. instance OAI.Erdos3.latticeSection_discrete line 186
  15. def OAI.Erdos3.orthogonalLatticeImage line 190
  16. theorem OAI.Erdos3.orthogonalLatticeImage_le_dual_section line 193
  17. theorem OAI.Erdos3.orthogonalLatticeImage_discrete line 206
  18. theorem OAI.Erdos3.orthogonalLatticeImage_full line 216
  19. def OAI.Erdos3.standardEuclideanLattice line 238
  20. instance OAI.Erdos3.standardEuclideanLattice_discrete line 241
  21. instance OAI.Erdos3.standardEuclideanLattice_full line 244
  22. theorem OAI.Erdos3.mem_standardEuclideanLattice line 247
  23. def OAI.Erdos3.standardEuclideanPoint line 254
  24. theorem OAI.Erdos3.standardEuclideanPoint_apply line 258
  25. theorem OAI.Erdos3.standardEuclideanPoint_bijective line 261
  26. def OAI.Erdos3.standardEuclideanEquiv line 274
  27. theorem OAI.Erdos3.standardEuclideanLattice_self_dual line 277
  28. def OAI.Erdos3.orthogonalLatticeProjection line 310
  29. theorem OAI.Erdos3.orthogonalLatticeProjection_surjective line 315
  30. def OAI.Erdos3.orthogonalLatticeKernelEquiv line 320
  31. theorem OAI.Erdos3.exists_orthogonal_lattice_split_basis line 332
  32. def OAI.Erdos3.integerBasisOfReal line 360
  33. theorem OAI.Erdos3.integerBasisOfReal_apply line 364
  34. theorem OAI.Erdos3.integerBasisOfReal_synthesis line 369
  35. def OAI.Erdos3.standardEuclideanLinearEquiv line 377
  36. theorem OAI.Erdos3.standardEuclideanLinearEquiv_apply line 381
  37. theorem OAI.Erdos3.standardEuclideanLinearEquiv_eq_point line 392
  38. def OAI.Erdos3.standardLatticeSmallBox line 408
  39. theorem OAI.Erdos3.standardLatticeSmallBox_isOpen line 411
  40. theorem OAI.Erdos3.standardLatticeSmallBox_separates line 418
  41. def OAI.Erdos3.orthogonalSectionKernelEquiv line 446
  42. def OAI.Erdos3.latticeLiftSection line 460
  43. theorem OAI.Erdos3.latticeLiftSection_rightInverse line 466
  44. def OAI.Erdos3.latticeIntegerLift line 473
  45. theorem OAI.Erdos3.latticeIntegerLift_projection line 477
  46. def OAI.Erdos3.latticeSignedCoordinates line 482
  47. theorem OAI.Erdos3.latticeSignedCoordinates_fst line 488
  48. theorem OAI.Erdos3.latticeSignedCoordinates_symm_apply line 493
  49. theorem OAI.Erdos3.latticeSignedCoordinates_reconstruction line 503
  50. def OAI.Erdos3.projectedLatticeLift line 524
  51. theorem OAI.Erdos3.projectedLatticeLift_projection line 528
  52. def OAI.Erdos3.latticeSheetPoint line 533
  53. theorem OAI.Erdos3.latticeSheetPoint_projection line 536
  54. theorem OAI.Erdos3.latticeSheetPoint_projection_orthogonal line 542
  55. def OAI.Erdos3.projectedLatticeShift line 548
  56. def OAI.Erdos3.latticeSheetQuotient line 552
  57. theorem OAI.Erdos3.latticeSheetPoint_reconstruction line 556
  58. theorem OAI.Erdos3.latticeSheetPoint_sub_mem_of_quotient_eq line 570
  59. theorem OAI.Erdos3.latticeSheetQuotient_injective_on_region line 582
  60. theorem OAI.Erdos3.normalizedLatticeSheet_point line 606
  61. theorem OAI.Erdos3.normalizedLatticeSheet_tsum_volume line 621