OAI/Geometry/LatticeCovering/Horizontal.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SingleLatticeCovering.Horizontal.FullLattice line 15
2. def OAI.SingleLatticeCovering.Horizontal.FullLattice.hole line 24
3. theorem OAI.SingleLatticeCovering.Horizontal.common_horizontal_from_mean line 32
4. theorem OAI.SingleLatticeCovering.Assembly.sections_and_mean_cover line 79
5. structure OAI.SingleLatticeCovering.Inputs.MeanHoleModel line 180
6. def OAI.SingleLatticeCovering.Inputs.GaussianPositions line 200
7. def OAI.SingleLatticeCovering.FinalRates.sectionRadius line 220
8. lemma OAI.SingleLatticeCovering.FinalRates.sectionRadius_pos line 222
9. lemma OAI.SingleLatticeCovering.FinalRates.radius_sq_bound line 225
10. lemma OAI.SingleLatticeCovering.FinalRates.eventually_first_polynomial line 235
11. lemma OAI.SingleLatticeCovering.FinalRates.eventually_marginal_scales line 249
12. lemma OAI.SingleLatticeCovering.Assembly.body_volume_pos line 302
13. lemma OAI.SingleLatticeCovering.Assembly.affine_body line 307
14. lemma OAI.SingleLatticeCovering.Assembly.chain_first_le_dim line 319
15. def OAI.SingleLatticeCovering.Assembly.coversAtBound line 325
16. theorem OAI.SingleLatticeCovering.Assembly.eventual_main_reduction line 336
17. theorem OAI.SingleLatticeCovering.FiniteDimensions.maximal_basis line 433
18. lemma OAI.SingleLatticeCovering.FiniteDimensions.convex_basis_cube line 496
19. lemma OAI.SingleLatticeCovering.FiniteDimensions.integer_cube_cover line 521
20. theorem OAI.SingleLatticeCovering.FiniteDimensions.finite_dimension_cover line 556