OAI/Geometry/NodalSets/Waves/LatticeDirectionalCenters.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Yau.Geometry.unitDirection line 10
2. lemma OAI.Yau.Geometry.norm_unitDirection_le line 12
3. def OAI.Yau.Geometry.directionalLatticeIndex line 19
4. lemma OAI.Yau.Geometry.directional_rounding_error line 22
5. lemma OAI.Yau.Geometry.directional_center_distance line 27
6. lemma OAI.Yau.Geometry.directional_center_mem line 40