OAI/Geometry/Cannon/Conformal/LinearZ.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CannonConformal.linearZ line 19
  2. def OAI.CannonConformal.linearBar line 20
  3. lemma OAI.CannonConformal.linearZBar_apply line 22
  4. lemma OAI.CannonConformal.linearZ_ne_zero line 32
  5. lemma OAI.CannonConformal.linear_beltrami_evaluate line 39
  6. lemma OAI.CannonConformal.coefficient_scale_pos line 46
  7. theorem OAI.CannonConformal.beltrami_integrates_form line 55
  8. theorem OAI.CannonConformal.measurable_structure_integration line 77
  9. lemma OAI.CannonMobius.measurable_extend_form line 120
  10. lemma OAI.CannonMobius.roundForm_bounds line 129
  11. theorem OAI.CannonMobius.controlled_action_structure_integration line 139
  12. lemma OAI.CannonConformal.isConformalMap_of_normSq line 201
  13. lemma OAI.CannonConformal.evaluate_pull_derivative line 212
  14. lemma OAI.CannonConformal.invariant_form_evaluate line 217
  15. theorem OAI.CannonConformal.integrated_invariant_form_conformal line 229
  16. lemma OAI.CannonMobius.coordinate_onePoint line 257
  17. lemma OAI.CannonMobius.chart_conjugate_onePoint line 263
  18. theorem OAI.CannonMobius.integrated_conjugate_ae_conformal line 269