OAI/Analysis/TriangularHilbert/AbsCost.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.TriangularHilbert.MatrixEnergy.two_abs_hessianPairPD_leline 13 - lemma
OAI.TriangularHilbert.MatrixEnergy.two_abs_hessianPair_le_of_projectionline 28 - lemma
OAI.TriangularHilbert.MatrixEnergy.two_abs_hessianPair_weightedGram_leline 39 - lemma
OAI.TriangularHilbert.Heat.two_abs_heatMixed_leline 60