OAI/Geometry/RuledCovering/HyperbolicLattice.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RuledApproximation.swapLinear line 12
2. def OAI.RuledApproximation.swapCLM line 17
3. lemma OAI.RuledApproximation.norm_le_of_scaled_coordinates line 19
4. theorem OAI.RuledApproximation.hyperbolic_lattice_model line 29

   Source documentation

   The symmetric hyperbolic template, with its uniform distance bound.

   theorem hyperbolic_lattice_model {L lam : ℝ} (hL : 0 < L)
       (hlam : 0 < L * lam) (hsmall : L * lam < 1) :
       LatticeModel (lam • swapCLM) L (1 / (2 * (1 - L * lam))) := by
   …

   Mentions: OAI.RuledApproximation.LatticeModel, OAI.RuledApproximation.swapCLM