OAI/Geometry/Kahler/BaseRadialMeasure.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PinchedHartogs.BaseConstruction.suMap line 20
  2. lemma OAI.PinchedHartogs.BaseConstruction.suMap_norm line 23
  3. def OAI.PinchedHartogs.BaseConstruction.suIsometry line 39
  4. lemma OAI.PinchedHartogs.BaseConstruction.suIsometry_zero line 43
  5. lemma OAI.PinchedHartogs.BaseConstruction.suIsometry_one line 47
  6. def OAI.PinchedHartogs.BaseConstruction.rotationIsometry line 51
  7. def OAI.PinchedHartogs.BaseConstruction.diagIsometry line 56
  8. lemma OAI.PinchedHartogs.BaseConstruction.diagIsometry_zero line 65
  9. lemma OAI.PinchedHartogs.BaseConstruction.diagIsometry_one line 69
  10. def OAI.PinchedHartogs.BaseConstruction.radialU line 73
  11. def OAI.PinchedHartogs.BaseConstruction.radialV line 74
  12. def OAI.PinchedHartogs.BaseConstruction.radialR line 75
  13. def OAI.PinchedHartogs.BaseConstruction.radialJ line 77
  14. lemma OAI.PinchedHartogs.BaseConstruction.radialUV line 79
  15. lemma OAI.PinchedHartogs.BaseConstruction.radialRI line 84
  16. lemma OAI.PinchedHartogs.BaseConstruction.radialU_continuous line 89
  17. lemma OAI.PinchedHartogs.BaseConstruction.radialV_continuous line 91
  18. lemma OAI.PinchedHartogs.BaseConstruction.radialR_continuous line 93
  19. lemma OAI.PinchedHartogs.BaseConstruction.radialJ_continuous line 96
  20. lemma OAI.PinchedHartogs.BaseConstruction.radial_phase_square line 100
  21. lemma OAI.PinchedHartogs.BaseConstruction.radial_square_integral line 115