OAI/Geometry/Cannon/Beltrami/TwoPointNormalize.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CannonBeltrami.hasCompactSupport_partialZ line 27
  2. lemma OAI.CannonBeltrami.smoothBeurling_decay line 35
  3. lemma OAI.CannonBeltrami.smoothBeurling_compatibility line 45
  4. theorem OAI.CannonBeltrami.smooth_nonvanishing_factor line 52
  5. theorem OAI.CannonBeltrami.smooth_beltrami_nondegenerate line 96
  6. lemma OAI.CannonBeltrami.beltrami_fderiv_injective line 117
  7. lemma OAI.CannonBeltrami.localHomeomorph_of_beltrami line 134
  8. lemma OAI.CannonBeltrami.isProperMap_of_asymptotic_id line 148
  9. lemma OAI.CannonBeltrami.global_homeomorph_of_proper_local line 167
  10. theorem OAI.CannonBeltrami.smooth_beltrami_homeomorph line 193
  11. lemma OAI.CannonBeltrami.contDiff_symm_beltrami line 206
  12. lemma OAI.CannonBeltrami.smooth_beltrami_l2_bound line 216
  13. theorem OAI.CannonBeltrami.smooth_principal_solution line 236
  14. lemma OAI.CannonBeltrami.partials_comp line 280
  15. lemma OAI.CannonBeltrami.inverse_partialBar line 301
  16. lemma OAI.CannonBeltrami.realCLM_det_wirtinger line 322
  17. lemma OAI.CannonBeltrami.realCLM_opNorm_wirtinger line 338
  18. theorem OAI.CannonBeltrami.wirtinger_energy_distortion line 347
  19. def OAI.CannonBeltrami.twoPointNormalize line 377
  20. lemma OAI.CannonBeltrami.twoPointNormalize_apply line 389
  21. lemma OAI.CannonBeltrami.twoPointNormalize_symm_apply line 391
  22. lemma OAI.CannonBeltrami.twoPointNormalize_zero line 394
  23. lemma OAI.CannonBeltrami.twoPointNormalize_one line 395
  24. lemma OAI.CannonBeltrami.twoPointNormalize_contDiff line 399
  25. lemma OAI.CannonBeltrami.twoPointNormalize_partials line 406
  26. theorem OAI.CannonBeltrami.normalized_smooth_beltrami_solution line 421