OAI/Analysis/TriangularHilbert/GramDeriv.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TriangularHilbert.MatrixEnergy.gramGradientAt line 15
2. lemma OAI.TriangularHilbert.MatrixEnergy.gramGradientAt_apply line 18
3. lemma OAI.TriangularHilbert.MatrixEnergy.regularized_energyGram_hasFDerivAt line 21
4. lemma OAI.TriangularHilbert.MatrixEnergy.continuousAt_tendstoUniformlyOnFilter line 39
5. def OAI.TriangularHilbert.MatrixEnergy.gramRegularization line 55
6. lemma OAI.TriangularHilbert.MatrixEnergy.continuous_gramRegularization line 58
7. lemma OAI.TriangularHilbert.MatrixEnergy.gramRegularization_posSemidef line 63
8. lemma OAI.TriangularHilbert.MatrixEnergy.gramRegularization_zero line 67
9. lemma OAI.TriangularHilbert.MatrixEnergy.continuous_regularizedGradient line 70
10. lemma OAI.TriangularHilbert.MatrixEnergy.eventually_regularizedEnergy_deriv line 89
11. lemma OAI.TriangularHilbert.MatrixEnergy.continuous_regularizedEnergy_single line 99
12. lemma OAI.TriangularHilbert.MatrixEnergy.tendsto_regularizedEnergy line 107
13. theorem OAI.TriangularHilbert.MatrixEnergy.energyGram_hasFDerivAt line 114