OAI/Combinatorics/Progressions/Lattices/LatticeSheetHaar.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.zspan_covolume_sq_eq_det_gram_fintype line 14
  2. theorem OAI.Erdos3.lattice_covolume_sq_eq_gram line 31
  3. theorem OAI.Erdos3.latticeHyperplane_covolume_sq line 50
  4. theorem OAI.Erdos3.latticeHyperplane_covolume line 89
  5. theorem OAI.Erdos3.basis_equivFun_measurePreserving line 120
  6. theorem OAI.Erdos3.volume_eq_covolume_smul_basis_addHaar line 132
  7. theorem OAI.Erdos3.latticeBasis_integral_cube line 148
  8. def OAI.Erdos3.latticeGaussianNormalizer line 185
  9. def OAI.Erdos3.normalizedLatticeGaussian line 188
  10. theorem OAI.Erdos3.latticeGaussianNormalizer_nonneg line 191
  11. theorem OAI.Erdos3.latticeGaussianNormalizer_pos line 195
  12. theorem OAI.Erdos3.normalizedLatticeGaussian_nonneg line 199
  13. theorem OAI.Erdos3.normalizedLatticeGaussian_pos line 203
  14. theorem OAI.Erdos3.latticeGaussianNormalizer_hyperplane line 208
  15. theorem OAI.Erdos3.normalizedLatticeGaussian_transfer line 223
  16. theorem OAI.Erdos3.exists_normalized_schmidt_hyperplane_transfer line 252
  17. theorem OAI.Erdos3.lattice_fundamentalDomain_volume line 283
  18. theorem OAI.Erdos3.lattice_quotient_scaled_haar line 291
  19. theorem OAI.Erdos3.latticeGaussianMass_antitone line 327
  20. theorem OAI.Erdos3.normalizedLatticeGaussian_hyperplane_origin_le line 337
  21. theorem OAI.Erdos3.lattice_covolume_of_finrank_zero line 352
  22. theorem OAI.Erdos3.normalizedLatticeGaussian_of_finrank_zero line 363
  23. theorem OAI.Erdos3.lattice_quotient_haar_image line 386
  24. theorem OAI.Erdos3.lattice_quotient_haar_translated_image line 410
  25. theorem OAI.Erdos3.lattice_quotient_haar_countable_sheets line 435
  26. theorem OAI.Erdos3.orthogonalLattice_covolume_sq line 464
  27. theorem OAI.Erdos3.orthogonalLattice_covolume line 515
  28. theorem OAI.Erdos3.lattice_sheet_haar_formula line 539