OAI/Analysis/MatrixSigning/Potential/PairIndex.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.Covariance.pairIndex line 19
  2. def OAI.CurrentKS.Covariance.offBlock line 22
  3. lemma OAI.CurrentKS.Covariance.offBlock_gram_trace line 25
  4. def OAI.CurrentKS.Covariance.weightEquiv line 45
  5. lemma OAI.CurrentKS.Covariance.weightEquiv_apply line 51
  6. lemma OAI.CurrentKS.Covariance.whiten_mul_weight line 54
  7. lemma OAI.CurrentKS.Covariance.combined_weighted_response line 67
  8. def OAI.CurrentKS.Covariance.pairWeight line 88
  9. lemma OAI.CurrentKS.Covariance.pairWeight_pos line 91
  10. lemma OAI.CurrentKS.Covariance.whiten_offBlock line 99
  11. lemma OAI.CurrentKS.Covariance.whiten_offBlock_gram line 110
  12. theorem OAI.CurrentKS.Covariance.weighted_block_covariance line 119