OAI/Analysis/MatrixSigning/Potential/PairVec.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentKS.Covariance.pairVec line 16
  2. def OAI.CurrentKS.Covariance.fstVec line 19
  3. def OAI.CurrentKS.Covariance.sndVec line 20
  4. lemma OAI.CurrentKS.Covariance.pairVec_left line 22
  5. lemma OAI.CurrentKS.Covariance.pairVec_right line 24
  6. lemma OAI.CurrentKS.Covariance.pairVec_fst_snd line 26
  7. lemma OAI.CurrentKS.Covariance.pairVec_ext line 31
  8. lemma OAI.CurrentKS.Covariance.sum_pair line 34
  9. lemma OAI.CurrentKS.Covariance.offBlock_apply_left line 38
  10. lemma OAI.CurrentKS.Covariance.offBlock_apply_right line 47
  11. def OAI.CurrentKS.Covariance.fstLin line 56
  12. def OAI.CurrentKS.Covariance.sndLin line 61
  13. def OAI.CurrentKS.Covariance.responseLin line 66
  14. def OAI.CurrentKS.Covariance.constraintLin line 68
  15. lemma OAI.CurrentKS.Covariance.response_decomposition line 71
  16. lemma OAI.CurrentKS.Covariance.weight_norm_sq line 88
  17. lemma OAI.CurrentKS.Covariance.pair_weighted_energy line 95
  18. lemma OAI.CurrentKS.Covariance.weighted_response_bound line 105