OAI/Analysis/TriangularHilbert/NormBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TriangularHilbert.MatrixEnergy.norm_sqrt_gram line 14
2. lemma OAI.TriangularHilbert.MatrixEnergy.norm_traceReal_le line 19
3. lemma OAI.TriangularHilbert.MatrixEnergy.norm_energy_gram_le line 23
4. lemma OAI.TriangularHilbert.MatrixEnergy.energy_gram_nonneg line 35
5. lemma OAI.TriangularHilbert.MatrixEnergy.norm_energyGradient_inserted_gram_le line 42
6. lemma OAI.TriangularHilbert.MatrixEnergy.hessianCost_nonneg line 64
7. lemma OAI.TriangularHilbert.MatrixEnergy.norm_hessianCost_inserted_gram_le line 72
8. def OAI.TriangularHilbert.MatrixEnergy.entryNormConstant line 83
9. lemma OAI.TriangularHilbert.MatrixEnergy.entryNormConstant_nonneg line 86
10. lemma OAI.TriangularHilbert.MatrixEnergy.norm_matrix_le_entries line 89