OAI/Combinatorics/MatchingEntropy/Covariance.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MatchingEntropyBounds.weightedColumns line 20
  2. def OAI.MatchingEntropyBounds.covariance line 23
  3. theorem OAI.MatchingEntropyBounds.covariance_posSemidef line 27
  4. theorem OAI.MatchingEntropyBounds.covariance_entry line 33
  5. theorem OAI.MatchingEntropyBounds.covariance_mulVec line 45
  6. theorem OAI.MatchingEntropyBounds.covariance_quadratic line 58
  7. def OAI.MatchingEntropyBounds.weightedDirectionSpace line 74
  8. theorem OAI.MatchingEntropyBounds.weightedColumns_span line 78
  9. theorem OAI.MatchingEntropyBounds.covariance_rank line 106
  10. def OAI.MatchingEntropyBounds.normalizedCentered line 110
  11. theorem OAI.MatchingEntropyBounds.normalizedCentered_mean line 114
  12. theorem OAI.MatchingEntropyBounds.normalizedCentered_variance line 121
  13. theorem OAI.MatchingEntropyBounds.normalized_covariance_trace line 141