OAI/Geometry/LatticeCovering/GaussianSections.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SingleLatticeCovering.Sections.map_normalizedRestriction line 13
  2. lemma OAI.SingleLatticeCovering.Sections.canonical_gaussian_coefficient_of_density line 30
  3. def OAI.SingleLatticeCovering.Inputs.orthogonalCoordinates line 69
  4. lemma OAI.SingleLatticeCovering.Inputs.orthogonalCoordinates_measurePreserving line 73
  5. def OAI.SingleLatticeCovering.Inputs.EldanKlartagAt line 83
  6. lemma OAI.SingleLatticeCovering.Inputs.gaussian_relative_lower line 95
  7. lemma OAI.SingleLatticeCovering.Inputs.orthogonalCoordinates_uniform line 102
  8. lemma OAI.SingleLatticeCovering.Inputs.body_marginal_eq line 110
  9. lemma OAI.SingleLatticeCovering.Inputs.orthogonalBody_interior line 134
  10. lemma OAI.SingleLatticeCovering.Inputs.orthogonalBody_flatten line 142
  11. lemma OAI.SingleLatticeCovering.Inputs.canonical_sections_of_marginal line 153
  12. theorem OAI.SingleLatticeCovering.Inputs.gaussianPositions_of_EldanKlartagAt line 207
  13. theorem OAI.SingleLatticeCovering.Inputs.gaussianPositions_of_eventual_EldanKlartagAt line 240
  14. lemma OAI.SingleLatticeCovering.Horizontal.latticeProjection_isOpen line 264
  15. lemma OAI.SingleLatticeCovering.Horizontal.exists_torus_transport line 273
  16. def OAI.SingleLatticeCovering.Horizontal.FullLattice.image line 318
  17. lemma OAI.SingleLatticeCovering.Horizontal.FullLattice.image_covolume line 321
  18. lemma OAI.SingleLatticeCovering.Horizontal.FullLattice.image_hole line 328
  19. def OAI.SingleLatticeCovering.Inputs.determinantScale line 363
  20. lemma OAI.SingleLatticeCovering.Inputs.determinantScale_det line 368
  21. lemma OAI.SingleLatticeCovering.Inputs.compact_linear_preimage line 376
  22. lemma OAI.SingleLatticeCovering.Inputs.interior_linear_preimage line 380
  23. lemma OAI.SingleLatticeCovering.Inputs.determinant_preimage_volume line 387
  24. def OAI.SingleLatticeCovering.Inputs.MeanHoleModel.scale line 405
  25. theorem OAI.SingleLatticeCovering.Assembly.main_reduction_to_cited_inputs line 461
  26. abbrev OAI.SingleLatticeCovering.FiniteKernel.integerLattice line 497
  27. def OAI.SingleLatticeCovering.FiniteKernel.integerCoordinates line 500
  28. lemma OAI.SingleLatticeCovering.FiniteKernel.integerCoordinates_cast line 503
  29. lemma OAI.SingleLatticeCovering.FiniteKernel.integerLattice_covolume line 508
  30. def OAI.SingleLatticeCovering.FiniteKernel.kernelLattice line 516
  31. lemma OAI.SingleLatticeCovering.FiniteKernel.kernelLattice_le line 519
  32. instance OAI.SingleLatticeCovering.FiniteKernel.kernelLattice_discrete line 524
  33. lemma OAI.SingleLatticeCovering.FiniteKernel.mem_kernelLattice_iff line 529
  34. instance OAI.SingleLatticeCovering.FiniteKernel.kernelLattice_full line 539
  35. lemma OAI.SingleLatticeCovering.FiniteKernel.kernelLattice_relIndex line 563
  36. theorem OAI.SingleLatticeCovering.FiniteKernel.kernelLattice_covolume line 574
  37. def OAI.SingleLatticeCovering.FiniteKernel.gridRelationForm line 591
  38. lemma OAI.SingleLatticeCovering.FiniteKernel.gridRelationForm_surjective line 603
  39. lemma OAI.SingleLatticeCovering.FiniteKernel.primitive_bezout_mod line 617
  40. theorem OAI.SingleLatticeCovering.FiniteKernel.primitive_grid_covolume line 630