OAI/Analysis/TriangularHilbert/WeightedGram.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TriangularHilbert.MatrixEnergy.weightedGram line 15
2. lemma OAI.TriangularHilbert.MatrixEnergy.weightedGram_posSemidef line 18
3. lemma OAI.TriangularHilbert.MatrixEnergy.weightedGram_isHermitian line 22
4. lemma OAI.TriangularHilbert.MatrixEnergy.weightedGram_mul_zero line 29
5. lemma OAI.TriangularHilbert.MatrixEnergy.weightedGram_kernel_projection line 55
6. lemma OAI.TriangularHilbert.MatrixEnergy.weightedGram_mul_eq_zero line 63
7. lemma OAI.TriangularHilbert.MatrixEnergy.diagonal_real_hasDerivAt line 67
8. lemma OAI.TriangularHilbert.MatrixEnergy.weightedGram_hasDerivAt line 81
9. theorem OAI.TriangularHilbert.MatrixEnergy.energy_weightedGram_hasDerivAt line 87
10. theorem OAI.TriangularHilbert.MatrixEnergy.energyGradient_weightedGram_hasDerivAt line 99