OAI/Geometry/NodalSets/Waves/GaussianFactor.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Yau.Probability.covarianceMatrix line 16
2. def OAI.Yau.Probability.covarianceFactor line 19
3. lemma OAI.Yau.Probability.covarianceMatrix_posSemidef line 22
4. lemma OAI.Yau.Probability.covarianceFactor_selfAdjoint line 28
5. lemma OAI.Yau.Probability.covarianceFactor_sq line 31
6. lemma OAI.Yau.Probability.covarianceFactor_inner line 38
7. lemma OAI.Yau.Probability.gaussian_covariance_factorization line 48