OAI/Analysis/SphereIsometry/ExtremalPropagation.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

The actual extremal return set and finite-hull propagation

The set is defined by equality in the original sphere-map defect. Its closedness, return identities and simultaneous support propagation are proved from that definition and the global absolute defect bound.

  1. def OAI.Tingley.extremalSphere line 30
  2. def OAI.Tingley.extremalSet line 33
  3. theorem OAI.Tingley.mem_extremalSet_coe line 36
  4. theorem OAI.Tingley.norm_eq_one_of_mem_extremalSet line 45
  5. theorem OAI.Tingley.isClosed_extremalSphere line 50
  6. theorem OAI.Tingley.isClosed_extremalSet line 54
  7. theorem OAI.Tingley.sRadius_eq_add line 58
  8. theorem OAI.Tingley.signedDefect_xPoint line 64
  9. theorem OAI.Tingley.extremalSphere_nonempty_of_attained line 71
  10. theorem OAI.Tingley.extremalSet_nonempty_of_attained line 80
  11. theorem OAI.Tingley.norm_fzPoint_sub_center line 86
  12. theorem OAI.Tingley.signedDefect_zPoint line 95
  13. theorem OAI.Tingley.norm_xPoint_sub_zPoint line 101
  14. theorem OAI.Tingley.norm_fxPoint_sub_fzPoint line 109
  15. theorem OAI.Tingley.extremal_radius_identities line 122
  16. theorem OAI.Tingley.rRadius_eq_add line 147
  17. theorem OAI.Tingley.extremal_common_support line 153
  18. theorem OAI.Tingley.mem_extremal_of_common_support_return line 161
  19. theorem OAI.Tingley.returnSphere_mem_extremal line 199
  20. theorem OAI.Tingley.positive_prefix_extension line 206