OAI/Geometry/Kahler/Definitions.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.PinchedHartogs.Base line 12

    Also declared: ComparatorChallenges/PinchedKahler.lean:12 (same declaration text).

  2. abbrev OAI.PinchedHartogs.Ambient line 13

    Also declared: ComparatorChallenges/PinchedKahler.lean:13 (same declaration text).

  3. abbrev OAI.PinchedHartogs.Target line 14

    Also declared: ComparatorChallenges/PinchedKahler.lean:14 (same declaration text).

  4. def OAI.PinchedHartogs.ball line 16

    Also declared: ComparatorChallenges/PinchedKahler.lean:16 (same declaration text).

  5. def OAI.PinchedHartogs.hartogs line 18

    Also declared: ComparatorChallenges/PinchedKahler.lean:18 (same declaration text).

  6. def OAI.PinchedHartogs.noMinorant line 21

    Also declared: ComparatorChallenges/PinchedKahler.lean:21 (same declaration text).

  7. def OAI.PinchedHartogs.coordVector line 25

    Also declared: ComparatorChallenges/PinchedKahler.lean:25 (same declaration text).

  8. def OAI.PinchedHartogs.jacobian line 28

    Distinct definitions of this name: ComparatorChallenges/PinchedKahler.lean:28 (same statement text; different proof or body). Qualify references as OAI.PinchedHartogs.jacobian@path.

  9. def OAI.PinchedHartogs.BoundedHolomorphic line 31
  10. def OAI.PinchedHartogs.MapObstruction line 34
  11. abbrev OAI.PinchedHartogs.CMatrix line 41

    Also declared: ComparatorChallenges/PinchedKahler.lean:33 (same declaration text).

  12. abbrev OAI.PinchedHartogs.CurvatureTensor line 42

    Also declared: ComparatorChallenges/PinchedKahler.lean:34 (same declaration text).

  13. def OAI.PinchedHartogs.coordinates line 44

    Also declared: ComparatorChallenges/PinchedKahler.lean:36 (same declaration text).

  14. def OAI.PinchedHartogs.dz line 46

    Also declared: ComparatorChallenges/PinchedKahler.lean:38 (same declaration text).

  15. def OAI.PinchedHartogs.dbar line 49

    Also declared: ComparatorChallenges/PinchedKahler.lean:41 (same declaration text).

  16. def OAI.PinchedHartogs.hermitianValue line 52

    Also declared: ComparatorChallenges/PinchedKahler.lean:44 (same declaration text).

  17. def OAI.PinchedHartogs.realArea line 55

    Also declared: ComparatorChallenges/PinchedKahler.lean:47 (same declaration text).

  18. def OAI.PinchedHartogs.tensorValue line 58

    Also declared: ComparatorChallenges/PinchedKahler.lean:50 (same declaration text).

  19. def OAI.PinchedHartogs.curvature line 62

    Also declared: ComparatorChallenges/PinchedKahler.lean:54 (same declaration text).

  20. def OAI.PinchedHartogs.sectional line 66

    Also declared: ComparatorChallenges/PinchedKahler.lean:58 (same declaration text).

  21. def OAI.PinchedHartogs.IsKahlerMetric line 70

    Also declared: ComparatorChallenges/PinchedKahler.lean:62 (same declaration text).

  22. def OAI.PinchedHartogs.christoffel line 76

    Also declared: ComparatorChallenges/PinchedKahler.lean:68 (same declaration text).

  23. def OAI.PinchedHartogs.GeodesicallyComplete line 79

    Also declared: ComparatorChallenges/PinchedKahler.lean:71 (same declaration text).

  24. def OAI.PinchedHartogs.IsNegativelyPinched line 86

    Also declared: ComparatorChallenges/PinchedKahler.lean:78 (same declaration text).

  25. def OAI.PinchedHartogs.NoBoundedCoordinates line 90

    Also declared: ComparatorChallenges/PinchedKahler.lean:82 (same declaration text).

  26. def OAI.PinchedHartogs.BiholomorphicToBoundedDomain line 95

    Also declared: ComparatorChallenges/PinchedKahler.lean:87 (same declaration text).

  27. def OAI.PinchedHartogs.MainTheorem line 100

    Also declared: ComparatorChallenges/PinchedKahler.lean:92 (same declaration text).

  28. def OAI.PinchedHartogs.psi line 106

    Also declared: ComparatorChallenges/PinchedKahler.lean:98 (same declaration text).

  29. def OAI.PinchedHartogs.metricPotential line 107

    Also declared: ComparatorChallenges/PinchedKahler.lean:99 (same declaration text).

  30. def OAI.PinchedHartogs.complexHessian line 110

    Also declared: ComparatorChallenges/PinchedKahler.lean:102 (same declaration text).

  31. def OAI.PinchedHartogs.hartogsMetric line 113

    Also declared: ComparatorChallenges/PinchedKahler.lean:105 (same declaration text).

  32. def OAI.PinchedHartogs.dzBase line 116

    Also declared: ComparatorChallenges/PinchedKahler.lean:108 (same declaration text).

  33. def OAI.PinchedHartogs.dbarBase line 120

    Also declared: ComparatorChallenges/PinchedKahler.lean:112 (same declaration text).

  34. def OAI.PinchedHartogs.baseHessian line 124

    Also declared: ComparatorChallenges/PinchedKahler.lean:116 (same declaration text).

  35. def OAI.PinchedHartogs.centeredChart line 127

    Also declared: ComparatorChallenges/PinchedKahler.lean:119 (same declaration text).

  36. def OAI.PinchedHartogs.ChartControl line 131

    Also declared: ComparatorChallenges/PinchedKahler.lean:123 (same declaration text).

  37. def OAI.PinchedHartogs.ChartJets line 136

    Also declared: ComparatorChallenges/PinchedKahler.lean:128 (same declaration text).

  38. def OAI.PinchedHartogs.ControlledPotential line 142

    Also declared: ComparatorChallenges/PinchedKahler.lean:134 (same declaration text).

  39. def OAI.PinchedHartogs.MetricTransfer line 146

    Also declared: ComparatorChallenges/PinchedKahler.lean:138 (same declaration text).