OAI/Geometry/QuadricBundles/Curvature.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.QuadricCounterexample.fderiv_apply_const line 12
  2. lemma OAI.QuadricCounterexample.hessian_mul line 19
  3. lemma OAI.QuadricCounterexample.hessian_re line 50
  4. lemma OAI.QuadricCounterexample.hessian_clm line 72
  5. lemma OAI.QuadricCounterexample.hessian_sum line 96
  6. lemma OAI.QuadricCounterexample.hessian_pullback_clm line 118
  7. lemma OAI.QuadricCounterexample.hessian_linear_zero line 130
  8. lemma OAI.QuadricCounterexample.hessian_linear_mul_linear line 136
  9. def OAI.QuadricCounterexample.entryCLM line 156
  10. def OAI.QuadricCounterexample.fiberEntryCLM line 160
  11. def OAI.QuadricCounterexample.starFiberEntryCLM line 163
  12. lemma OAI.QuadricCounterexample.base_entry_C2 line 166
  13. lemma OAI.QuadricCounterexample.base_entry_fderiv line 171
  14. lemma OAI.QuadricCounterexample.base_entry_hessian line 180
  15. def OAI.QuadricCounterexample.complexQuadratic line 190
  16. def OAI.QuadricCounterexample.hermitianQuadratic line 193
  17. lemma OAI.QuadricCounterexample.complexQuadratic_eq_sum line 197
  18. lemma OAI.QuadricCounterexample.complexQuadratic_C2 line 203
  19. lemma OAI.QuadricCounterexample.complexQuadratic_hessian line 214
  20. def OAI.QuadricCounterexample.matrixAdjointCLM line 255
  21. lemma OAI.QuadricCounterexample.hermitian_fderiv line 262
  22. lemma OAI.QuadricCounterexample.hermitian_hessian line 271
  23. lemma OAI.QuadricCounterexample.matrix_completed_square line 296
  24. lemma OAI.QuadricCounterexample.matrix_completed_square_nonneg line 318
  25. lemma OAI.QuadricCounterexample.quadratic_levi_expansion line 335
  26. def OAI.QuadricCounterexample.wirtingerDerivative line 368
  27. def OAI.QuadricCounterexample.mixedHessian line 371
  28. lemma OAI.QuadricCounterexample.hermitianQuadratic_C2 line 375
  29. lemma OAI.QuadricCounterexample.hermitianQuadratic_levi line 380
  30. lemma OAI.QuadricCounterexample.hermitianQuadratic_levi_nonneg line 401
  31. lemma OAI.QuadricCounterexample.curvature_nonneg_of_strict line 411
  32. theorem OAI.QuadricCounterexample.chern_positive_dual_norm_psh line 422