OAI/Combinatorics/SparsestCut/PositiveKernels.lean
9 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.UniformSparsestCut.TriangleRepair.gram_posSemidefline 17 - lemma
OAI.UniformSparsestCut.TriangleRepair.ones_posSemidefline 37 - lemma
OAI.UniformSparsestCut.TriangleRepair.entrywise_pow_posSemidefline 43 - lemma
OAI.UniformSparsestCut.TriangleRepair.sum_posSemidefline 50 - lemma
OAI.UniformSparsestCut.TriangleRepair.posSemidef_of_tendstoline 60 - lemma
OAI.UniformSparsestCut.TriangleRepair.entrywise_exp_posSemidefline 80 - lemma
OAI.UniformSparsestCut.TriangleRepair.gaussian_posSemidefline 99 - lemma
OAI.UniformSparsestCut.TriangleRepair.integral_posSemidefline 121 - lemma
OAI.UniformSparsestCut.TriangleRepair.exists_gramline 150