OAI/Analysis/MatrixSigning/Potential/QuadGram.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentKS.Covariance.quad_gram line 19
2. theorem OAI.CurrentKS.Covariance.exists_singular_subspace line 25
3. lemma OAI.CurrentKS.Covariance.gram_trace line 49
4. lemma OAI.CurrentKS.Covariance.weighted_singular_subspace line 66
5. lemma OAI.CurrentKS.Covariance.coupled_singular_subspace line 79
6. theorem OAI.CurrentKS.Covariance.coupled_covariance line 99