OAI/Geometry/Cannon/Conformal/SphereMeasure.lean

GitHub source file

54 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.CannonMobius.sphereMeasurableSpace line 20
  2. instance OAI.CannonMobius.sphereBorelSpace line 21
  3. def OAI.CannonMobius.sphereMeasure line 23
  4. lemma OAI.CannonMobius.sphereMeasure_apply line 25
  5. lemma OAI.CannonMobius.chartDomain_ae line 29
  6. lemma OAI.CannonMobius.sphere_image_null_of_chart line 38
  7. lemma OAI.CannonMobius.analytic_sphere_image_null line 61
  8. lemma OAI.CannonMobius.onePoint_image_null line 69
  9. theorem OAI.CannonMobius.controlled_sphere_image_null line 81
  10. theorem OAI.CannonMobius.controlled_sphere_quasiMeasurePreserving line 97
  11. lemma OAI.CannonMobius.chart_mul_eventually line 112
  12. lemma OAI.CannonMobius.chart_symm_domain line 121
  13. lemma OAI.CannonMobius.chart_symm_comp_eventually line 129
  14. lemma OAI.CannonMobius.analytic_chart_bijective line 137
  15. lemma OAI.CannonMobius.analytic_chart_conformal line 150
  16. theorem OAI.CannonMobius.controlled_sphere_ae_differentiable line 163
  17. lemma OAI.CannonMobius.ae_sphere_iff line 190
  18. lemma OAI.CannonMobius.controlled_chart_ae_pullback line 194
  19. theorem OAI.CannonMobius.controlled_sphere_ae_bijective_fderiv line 204
  20. theorem OAI.CannonMobius.controlled_sphere_ae_chain line 220
  21. lemma OAI.CannonMetricQC.WeakQS.derivative_distortion line 241
  22. abbrev OAI.CannonConformal.Form line 261
  23. def OAI.CannonConformal.determinant line 262
  24. def OAI.CannonConformal.evaluate line 263
  25. def OAI.CannonConformal.Positive line 264
  26. def OAI.CannonConformal.LowerBound line 265
  27. def OAI.CannonConformal.UpperBound line 266
  28. lemma OAI.CannonConformal.determinant_nonneg_of_evaluate line 268
  29. lemma OAI.CannonConformal.determinant_ge_sq_lower line 285
  30. def OAI.CannonMetricQC.derivativeMatrix line 303
  31. def OAI.CannonMetricQC.derivativeDet line 305
  32. def OAI.CannonMetricQC.derivativeForm line 308
  33. lemma OAI.CannonMetricQC.derivative_apply line 311
  34. lemma OAI.CannonMetricQC.derivativeForm_evaluate line 319
  35. lemma OAI.CannonMetricQC.derivativeForm_det line 325
  36. lemma OAI.CannonMetricQC.linear_distortion_scaled line 330
  37. theorem OAI.CannonMetricQC.linear_distortion_jacobian line 345
  38. lemma OAI.CannonMetricQC.WeakQS.derivative_jacobian line 374
  39. lemma OAI.CannonMetricQC.derivativeDet_eq_det line 379
  40. lemma OAI.CannonMetricQC.derivativeDet_ne_zero line 383
  41. lemma OAI.CannonMobius.chart_normalized_eq line 397
  42. theorem OAI.CannonMobius.controlled_sphere_ae_distortion line 405
  43. theorem OAI.CannonMobius.controlled_sphere_ae_jacobian_bound line 434
  44. def OAI.CannonConformal.orbitCore line 452
  45. lemma OAI.CannonConformal.orbitCore_subset line 456
  46. lemma OAI.CannonConformal.orbitCore_invariant line 461
  47. lemma OAI.CannonConformal.orbitCore_measurable line 470
  48. theorem OAI.CannonConformal.ae_orbitCore line 476
  49. theorem OAI.CannonConformal.invariant_conull_core line 481
  50. def OAI.CannonMobius.spherePermAction line 507
  51. def OAI.CannonMobius.sphereDerivative line 512
  52. def OAI.CannonMobius.GoodDifferentials line 515
  53. theorem OAI.CannonMobius.controlled_action_derivative_core line 521
  54. theorem OAI.CannonMobius.sphereDerivative_mul_on_core line 565