OAI/Analysis/MatrixSigning/Potential/CovarianceE.lean

GitHub source file

72 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.CurrentKS.Covariance.E line 14
  2. abbrev OAI.CurrentKS.Covariance.Mat line 15
  3. def OAI.CurrentKS.Covariance.projectionMatrix line 22
  4. theorem OAI.CurrentKS.Covariance.projectionMatrix_toEuclideanLin line 26
  5. theorem OAI.CurrentKS.Covariance.projectionMatrix_posSemidef line 30
  6. theorem OAI.CurrentKS.Covariance.projectionMatrix_range line 35
  7. theorem OAI.CurrentKS.Covariance.projectionMatrix_trace line 40
  8. theorem OAI.CurrentKS.Covariance.projectionMatrix_add_orthogonal line 47
  9. theorem OAI.CurrentKS.Covariance.projectionMatrix_diag_le_one line 56
  10. theorem OAI.CurrentKS.Covariance.abs_entry_le_trace line 63
  11. theorem OAI.CurrentKS.Covariance.isClosed_psd line 75
  12. def OAI.CurrentKS.Covariance.psdTraceBound line 82
  13. theorem OAI.CurrentKS.Covariance.isClosed_psdTraceBound line 85
  14. theorem OAI.CurrentKS.Covariance.isCompact_psdTraceBound line 88
  15. theorem OAI.CurrentKS.Covariance.convex_psdTraceBound line 99
  16. def OAI.CurrentKS.Covariance.Supported line 108
  17. def OAI.CurrentKS.Covariance.feasible line 111
  18. theorem OAI.CurrentKS.Covariance.isClosed_supported line 114
  19. theorem OAI.CurrentKS.Covariance.isClosed_feasible line 124
  20. theorem OAI.CurrentKS.Covariance.feasible_trace_le line 130
  21. theorem OAI.CurrentKS.Covariance.isCompact_feasible line 136
  22. theorem OAI.CurrentKS.Covariance.convex_feasible line 140
  23. theorem OAI.CurrentKS.Covariance.zero_mem_feasible line 154
  24. theorem OAI.CurrentKS.Covariance.projectionMatrix_mem_feasible line 161
  25. theorem OAI.CurrentKS.Covariance.entry_sq_le_diag_mul line 168
  26. theorem OAI.CurrentKS.Covariance.entry_eq_zero_of_diag_eq_zero line 180
  27. def OAI.CurrentKS.Covariance.sqrtDiagonal line 186
  28. def OAI.CurrentKS.Covariance.whiten line 188
  29. theorem OAI.CurrentKS.Covariance.whiten_posSemidef line 192
  30. theorem OAI.CurrentKS.Covariance.whiten_apply line 197
  31. theorem OAI.CurrentKS.Covariance.whiten_diag_le_one line 201
  32. theorem OAI.CurrentKS.Covariance.whiten_trace_le line 215
  33. theorem OAI.CurrentKS.Covariance.reconstruct_whiten line 221
  34. theorem OAI.CurrentKS.Covariance.sqrtDiagonal_sq line 239
  35. theorem OAI.CurrentKS.Covariance.toEuclideanLin_mul line 246
  36. def OAI.CurrentKS.Covariance.quad line 250
  37. theorem OAI.CurrentKS.Covariance.quad_add line 252
  38. theorem OAI.CurrentKS.Covariance.quad_sub line 257
  39. theorem OAI.CurrentKS.Covariance.quad_smul line 262
  40. theorem OAI.CurrentKS.Covariance.quad_congr line 267
  41. theorem OAI.CurrentKS.Covariance.posSemidef_iff_quad_nonneg line 272
  42. theorem OAI.CurrentKS.Covariance.eigenvector_toEuclideanLin line 279
  43. theorem OAI.CurrentKS.Covariance.quad_eq_sum_eigenvalues line 286
  44. theorem OAI.CurrentKS.Covariance.inner_self_eq_sum_eigenbasis line 296
  45. theorem OAI.CurrentKS.Covariance.low_eigen_quad_le line 303
  46. abbrev OAI.CurrentKS.Covariance.High line 313
  47. theorem OAI.CurrentKS.Covariance.high_count_mul_le_trace line 316
  48. def OAI.CurrentKS.Covariance.highCoordinates line 333
  49. theorem OAI.CurrentKS.Covariance.finrank_inf_ker_add line 339
  50. theorem OAI.CurrentKS.Covariance.sqrtDiagonal_isHermitian line 349
  51. theorem OAI.CurrentKS.Covariance.quad_diag_eq line 352
  52. theorem OAI.CurrentKS.Covariance.quad_whiten_eq line 360
  53. theorem OAI.CurrentKS.Covariance.exists_good_subspace line 367
  54. theorem OAI.CurrentKS.Covariance.linearFunctional_expansion line 398
  55. def OAI.CurrentKS.Covariance.rawDualMatrix line 407
  56. theorem OAI.CurrentKS.Covariance.rawDualMatrix_trace line 409
  57. def OAI.CurrentKS.Covariance.dualMatrix line 420
  58. theorem OAI.CurrentKS.Covariance.dualMatrix_isHermitian line 423
  59. theorem OAI.CurrentKS.Covariance.transpose_eq_of_isHermitian line 427
  60. theorem OAI.CurrentKS.Covariance.dualMatrix_trace line 431
  61. theorem OAI.CurrentKS.Covariance.trace_mul_vecMulVec line 440
  62. theorem OAI.CurrentKS.Covariance.dualMatrix_posSemidef line 446
  63. theorem OAI.CurrentKS.Covariance.projectionMatrix_mul_self line 456
  64. theorem OAI.CurrentKS.Covariance.trace_mul_projection_nonneg line 464
  65. theorem OAI.CurrentKS.Covariance.exists_dual_projection line 484
  66. def OAI.CurrentKS.Covariance.slack line 498
  67. theorem OAI.CurrentKS.Covariance.slack_isHermitian line 500
  68. theorem OAI.CurrentKS.Covariance.trace_slack_commutes line 504
  69. def OAI.CurrentKS.Covariance.constraintMap line 512
  70. theorem OAI.CurrentKS.Covariance.convex_psd line 528
  71. theorem OAI.CurrentKS.Covariance.nonneg_of_ray_lower_bound line 532
  72. theorem OAI.CurrentKS.Covariance.subspace_covariance line 547