OAI/Analysis/LiebThirring/BoundaryValues.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLiebThirring.MatrixProof.quadraticMatrix_diagonal line 27
2. lemma OAI.SharpLiebThirring.MatrixProof.fieldIntegrand_diagonal line 39
3. lemma OAI.SharpLiebThirring.MatrixProof.hermitianField_diagonal line 48
4. lemma OAI.SharpLiebThirring.MatrixProof.matrixField_diagonal line 89
5. lemma OAI.SharpLiebThirring.MatrixProof.continuous_scalarMu line 97
6. lemma OAI.SharpLiebThirring.MatrixProof.fieldPrimitive_diagonal line 101
7. lemma OAI.SharpLiebThirring.MatrixProof.fieldPrimitive_endpoint_jump line 122
8. lemma OAI.SharpLiebThirring.MatrixProof.scalar_boundary_regularized line 140
9. lemma OAI.SharpLiebThirring.MatrixProof.scalar_boundary_limit line 148
10. lemma OAI.SharpLiebThirring.MatrixProof.fieldPrimitive_endpoint_limit line 162
11. lemma OAI.SharpLiebThirring.MatrixProof.realHermitianComplexify_smul line 181
12. def OAI.SharpLiebThirring.MatrixProof.realHermitianComplexifyCLM line 187
13. lemma OAI.SharpLiebThirring.MatrixProof.realHermitianComplexifyCLM_apply line 197
14. def OAI.SharpLiebThirring.MatrixProof.realK2SelfAdjoint line 200
15. lemma OAI.SharpLiebThirring.MatrixProof.fieldPrimitive_eq_hermitianPotential line 203
16. lemma OAI.SharpLiebThirring.MatrixProof.fieldPrimitive_hasFDerivAt line 223
17. lemma OAI.SharpLiebThirring.MatrixProof.fieldPrimitive_path_derivative line 235
18. lemma OAI.SharpLiebThirring.MatrixProof.hermitian_integral line 251
19. lemma OAI.SharpLiebThirring.MatrixProof.hermitianField_isHermitian line 260
20. lemma OAI.SharpLiebThirring.MatrixProof.matrixField_isHermitian line 269