OAI/Geometry/Kahler/HartogsModelBridge.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PinchedHartogs.normalIndex line 16
  2. def OAI.PinchedHartogs.verticalScale line 20
  3. def OAI.PinchedHartogs.normalCurvature line 24
  4. lemma OAI.PinchedHartogs.normalCurvature_symmetries line 29
  5. lemma OAI.PinchedHartogs.tensor_symmetries_sub line 38
  6. lemma OAI.PinchedHartogs.tensor_symmetries_add line 45
  7. lemma OAI.PinchedHartogs.tensor_symmetries_smul line 52
  8. lemma OAI.PinchedHartogs.tensor_S_symmetries line 59
  9. lemma OAI.PinchedHartogs.block_isHermitian line 71
  10. lemma OAI.PinchedHartogs.principal_symmetries line 77
  11. def OAI.PinchedHartogs.horizontalPart line 90
  12. lemma OAI.PinchedHartogs.horizontalPart_supported line 93
  13. lemma OAI.PinchedHartogs.horizontalPart_symmetries line 97
  14. lemma OAI.PinchedHartogs.tensor_split_of_low_blocks line 110
  15. lemma OAI.PinchedHartogs.baseHessian_isHermitian line 133
  16. lemma OAI.PinchedHartogs.complex_horizontalMetric line 142
  17. lemma OAI.PinchedHartogs.mixedMatrix_component line 147
  18. lemma OAI.PinchedHartogs.sqrt_normalization line 159
  19. lemma OAI.PinchedHartogs.normalCurvature_HVHV line 170
  20. lemma OAI.PinchedHartogs.normalCurvature_HHVV line 187
  21. lemma OAI.PinchedHartogs.normalCurvature_HVVV line 197
  22. lemma OAI.PinchedHartogs.normalCurvature_VVVV line 207
  23. lemma OAI.PinchedHartogs.principal_HHHH line 218
  24. lemma OAI.PinchedHartogs.principal_HHHV line 223
  25. lemma OAI.PinchedHartogs.principal_HVHV line 227
  26. lemma OAI.PinchedHartogs.principal_HHVV line 231
  27. lemma OAI.PinchedHartogs.principal_HVVV line 235
  28. lemma OAI.PinchedHartogs.principal_VVVV line 239
  29. def OAI.PinchedHartogs.normalError line 243
  30. lemma OAI.PinchedHartogs.normalError_symmetries line 246
  31. lemma OAI.PinchedHartogs.normalCurvature_model line 252