OAI/Analysis/LiebThirring/Eigenspace.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpLiebThirring.OperatorProof.eigenSpace line 12

    Source documentation

    The true eigenspace, including the operator-domain condition.

    def eigenSpace (A : L2C →ₗ.[ℂ] L2C) (e : ℝ) : Submodule ℂ L2C :=
…

    Mentions: OAI.SharpLiebThirring.OperatorProof.L2C

  2. lemma OAI.SharpLiebThirring.OperatorProof.mem_eigenSpace line 16
  3. lemma OAI.SharpLiebThirring.OperatorProof.eigenSpace_closed line 22
  4. lemma OAI.SharpLiebThirring.OperatorProof.eigenSpace_orthogonal line 27
  5. lemma OAI.SharpLiebThirring.OperatorProof.eigenBasis_exists line 41
  6. def OAI.SharpLiebThirring.OperatorProof.eigenBasisSet line 47
  7. def OAI.SharpLiebThirring.OperatorProof.eigenBasis line 50
  8. abbrev OAI.SharpLiebThirring.OperatorProof.NegativeEnergy line 54
  9. abbrev OAI.SharpLiebThirring.OperatorProof.EigenIndex line 55
  10. def OAI.SharpLiebThirring.OperatorProof.eigenBasisVector line 58
  11. lemma OAI.SharpLiebThirring.OperatorProof.eigenBasisVector_member line 61
  12. lemma OAI.SharpLiebThirring.OperatorProof.eigenBasisVector_orthonormal line 65
  13. def OAI.SharpLiebThirring.OperatorProof.eigenvalueSum line 84

    Source documentation

    The extended sum over every negative eigenvalue, repeated once for each member of a full Hilbert basis of its eigenspace. This is a literal spectral sum with multiplicities; no enumeration and no finiteness assumption is made.

    def eigenvalueSum (γ : ℝ) (A : L2C →ₗ.[ℂ] L2C) (hA : IsSelfAdjoint A) : ℝ≥0∞ :=
…

    Mentions: OAI.SharpLiebThirring.OperatorProof.L2C