OAI/Combinatorics/Progressions/Lattices/LatticeHyperplaneBasis.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.latticeHyperplane line 11
  2. theorem OAI.Erdos3.mem_latticeHyperplane line 15
  3. def OAI.Erdos3.hyperplaneRetraction line 18
  4. theorem OAI.Erdos3.hyperplaneRetraction_coe line 32
  5. theorem OAI.Erdos3.hyperplaneRetraction_on_kernel line 36
  6. theorem OAI.Erdos3.hyperplaneRetraction_surjective line 41
  7. theorem OAI.Erdos3.hyperplaneRetraction_mem line 45
  8. theorem OAI.Erdos3.latticeHyperplane_span_top line 54
  9. instance OAI.Erdos3.latticeHyperplane_discrete line 72
  10. theorem OAI.Erdos3.latticeHyperplane_isZLattice line 76
  11. theorem OAI.Erdos3.hyperplane_finrank line 83
  12. def OAI.Erdos3.integralLatticeValue line 102
  13. theorem OAI.Erdos3.integralLatticeValue_cast line 106
  14. def OAI.Erdos3.integralLatticeCoordinate line 111
  15. theorem OAI.Erdos3.integralLatticeCoordinate_cast line 122
  16. theorem OAI.Erdos3.integralLatticeCoordinate_eq_iff line 127
  17. theorem OAI.Erdos3.integralLatticeCoordinate_surjective line 133
  18. theorem OAI.Erdos3.lattice_gaussian_summable line 155
  19. def OAI.Erdos3.latticeGaussianMass line 172
  20. theorem OAI.Erdos3.latticeGaussianMass_nonneg line 176
  21. theorem OAI.Erdos3.latticeGaussianMass_pos line 179
  22. theorem OAI.Erdos3.latticeGaussianMass_add_lattice line 185
  23. theorem OAI.Erdos3.latticeGaussianMass_eq_of_sub_mem line 191
  24. def OAI.Erdos3.latticeHyperplaneRetraction line 206
  25. theorem OAI.Erdos3.latticeHyperplaneRetraction_coe line 220
  26. def OAI.Erdos3.latticeHyperplaneSplit line 226
  27. theorem OAI.Erdos3.latticeHyperplaneSplit_symm_coe line 255
  28. theorem OAI.Erdos3.integer_functional_image_generator line 269
  29. theorem OAI.Erdos3.integralLatticeCoordinate_ne_zero line 287
  30. theorem OAI.Erdos3.exists_primitive_lattice_functional line 299
  31. theorem OAI.Erdos3.gaussian_translate_bound line 336
  32. theorem OAI.Erdos3.continuousOn_latticeGaussianMass line 357
  33. theorem OAI.Erdos3.continuous_latticeGaussianMass line 367
  34. def OAI.Erdos3.latticeHyperplaneBasis line 384
  35. theorem OAI.Erdos3.latticeHyperplaneBasis_inl line 392
  36. theorem OAI.Erdos3.latticeHyperplaneBasis_inr line 400