OAI/Analysis/TriangularHilbert/WeightedCompare.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularHilbert.MatrixEnergy.weightedGram_sub line 13
2. lemma OAI.TriangularHilbert.MatrixEnergy.weightedGram_mono line 22
3. lemma OAI.TriangularHilbert.MatrixEnergy.rowBare_apply_zero line 27
4. lemma OAI.TriangularHilbert.MatrixEnergy.weightedGram_rowBare_congr line 31
5. lemma OAI.TriangularHilbert.MatrixEnergy.hessianCost_smul_direction line 49
6. lemma OAI.TriangularHilbert.MatrixEnergy.blockD_real_diagonal line 55
7. lemma OAI.TriangularHilbert.MatrixEnergy.norm_blockD_real_diagonal_le line 62