OAI/Geometry/QuadricBundles/MatrixRepresentative.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.QuadricCounterexample.quadraticValue line 15
  2. lemma OAI.QuadricCounterexample.star_basis line 19
  3. lemma OAI.QuadricCounterexample.basis_pair line 24
  4. lemma OAI.QuadricCounterexample.quadraticValue_basis line 29
  5. lemma OAI.QuadricCounterexample.quadraticValue_add_basis line 33
  6. lemma OAI.QuadricCounterexample.quadraticValue_add_I_basis line 41
  7. def OAI.QuadricCounterexample.matrixFromQuadratic line 54
  8. lemma OAI.QuadricCounterexample.matrixFromQuadratic_value line 60
  9. theorem OAI.QuadricCounterexample.quadraticValue_pointwise_limit line 73
  10. lemma OAI.QuadricCounterexample.isClosed_matrix_positive_semidefinite line 102
  11. lemma OAI.QuadricCounterexample.convex_matrix_positive_semidefinite line 114
  12. def OAI.QuadricCounterexample.quadraticValueCLM line 123
  13. lemma OAI.QuadricCounterexample.quadraticValue_average line 132
  14. lemma OAI.QuadricCounterexample.positive_semidefinite_average line 138
  15. lemma OAI.QuadricCounterexample.quadraticValue_nonneg line 144
  16. theorem OAI.QuadricCounterexample.matrix_ball_infimum_representative line 148
  17. lemma OAI.QuadricCounterexample.continuous_joint_averaged_quadratic line 176
  18. lemma OAI.QuadricCounterexample.joint_upperSemicontinuous_infimum line 187
  19. lemma OAI.QuadricCounterexample.matrixFromQuadratic_ae_recovery line 204
  20. theorem OAI.QuadricCounterexample.matrix_regularized_representative line 220
  21. lemma OAI.QuadricCounterexample.integral_ball_translate line 271
  22. theorem OAI.QuadricCounterexample.DiskPshOn.base_ball_average line 283
  23. lemma OAI.QuadricCounterexample.DiskPshOn.pointwise_limit_of_continuous_bound line 323
  24. theorem OAI.QuadricCounterexample.averaged_matrix_limit_psh line 338
  25. theorem OAI.QuadricCounterexample.joint_matrix_regularized_representative line 382