OAI/Analysis/SphereIsometry/Basic.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Sphere maps and the maximal cross-radius defect

The sphere carries the ambient distance. All defects below use the actual sphere isometry and ordinary real scalar multiplication; no extension law is assumed.

  1. theorem OAI.Tingley.UnitSphere.norm_coe line 26
  2. theorem OAI.Tingley.UnitSphere.coe_ne_zero line 29
  3. theorem OAI.Tingley.normalize_coe line 34
  4. theorem OAI.Tingley.norm_smul_normalize line 37
  5. instance OAI.Tingley.UnitSphere.instNonempty line 41
  6. theorem OAI.Tingley.sphere_norm_sub line 46
  7. def OAI.Tingley.signedDefect line 50
  8. def OAI.Tingley.HasDefectBound line 54
  9. def OAI.Tingley.absoluteDefects line 57
  10. def OAI.Tingley.maxDefect line 60
  11. theorem OAI.Tingley.signedDefect_zero line 62
  12. theorem OAI.Tingley.signedDefect_one line 66
  13. theorem OAI.Tingley.signedDefect_symm line 70
  14. theorem OAI.Tingley.HasDefectBound.symm line 76
  15. theorem OAI.Tingley.norm_sub_smul_lipschitz line 83
  16. theorem OAI.Tingley.signedDefect_lipschitz line 94
  17. theorem OAI.Tingley.signedDefect_le_endpoints line 110
  18. theorem OAI.Tingley.signedDefect_abs_le_one line 119
  19. theorem OAI.Tingley.absoluteDefects_bddAbove line 125
  20. theorem OAI.Tingley.zero_mem_absoluteDefects line 131
  21. theorem OAI.Tingley.hasDefectBound_maxDefect line 136
  22. theorem OAI.Tingley.maxDefect_nonneg line 141
  23. theorem OAI.Tingley.maxDefect_le_one line 145
  24. theorem OAI.Tingley.absoluteDefects_symm line 151
  25. theorem OAI.Tingley.maxDefect_symm line 162
  26. theorem OAI.Tingley.signedDefect_eq_zero_of_bound_zero line 167