OAI/Geometry/TranslativeCovering/ConeStretch.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ConeStretch.Space line 23
  2. def OAI.ConeStretch.stretch line 25
  3. lemma OAI.ConeStretch.stretch_apply line 28
  4. lemma OAI.ConeStretch.stretch_det line 32
  5. lemma OAI.ConeStretch.norm_sq line 39
  6. lemma OAI.ConeStretch.stretch_norm_sq line 42
  7. lemma OAI.ConeStretch.coordinate_sq_le line 56
  8. lemma OAI.ConeStretch.stretch_norm_bounds line 60
  9. lemma OAI.ConeStretch.stretch_inverse line 72
  10. def OAI.ConeStretch.cone line 78
  11. lemma OAI.ConeStretch.threshold_iff line 81
  12. lemma OAI.ConeStretch.stretch_threshold line 106
  13. lemma OAI.ConeStretch.stretch_cone_lower_norm line 114
  14. lemma OAI.ConeStretch.cone_smul line 129
  15. lemma OAI.ConeStretch.cone_volume_scale line 150
  16. lemma OAI.ConeStretch.stretch_cone_outer line 155
  17. lemma OAI.ConeStretch.stretch_cone_inner line 166
  18. lemma OAI.ConeStretch.cone_volume_comparison line 188