OAI/Analysis/MatrixSigning/Potential/Column.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentKS.Covariance.trace_mul_nonneg line 16
  2. lemma OAI.CurrentKS.Covariance.trace_mul_diagonal_eq line 23
  3. lemma OAI.CurrentKS.Covariance.energy_trace_domination line 27
  4. lemma OAI.CurrentKS.Covariance.sqrt_range_eq line 35
  5. lemma OAI.CurrentKS.Covariance.on_sqrt_range line 43
  6. def OAI.CurrentKS.Covariance.column line 53
  7. lemma OAI.CurrentKS.Covariance.column_eq_apply_basis line 55
  8. lemma OAI.CurrentKS.Covariance.sqrt_column_range line 60
  9. lemma OAI.CurrentKS.Covariance.sum_column_quadratic line 65
  10. lemma OAI.CurrentKS.Covariance.sqrt_moments line 79
  11. lemma OAI.CurrentKS.Covariance.row_moments line 84
  12. lemma OAI.CurrentKS.Covariance.total_movement line 96