OAI/Analysis/LiebThirring/SchrodingerOperator.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLiebThirring.OperatorProof.operator line 14

   Source documentation

   The self-adjoint realization of -d²/dx²-W, obtained by inverting the coercively shifted H¹ form. The graph identity below characterizes it without reference to the choice of potential decomposition or shift.

   def operator {W : ℝ → ℝ} (d : PotentialData W) : L2C →ₗ.[ℂ] L2C :=
   …

   Mentions: OAI.SharpLiebThirring.OperatorProof.PotentialData, OAI.SharpLiebThirring.OperatorProof.L2C

2. lemma OAI.SharpLiebThirring.OperatorProof.operator_selfAdjoint line 17
3. lemma OAI.SharpLiebThirring.OperatorProof.operator_dense line 22
4. lemma OAI.SharpLiebThirring.OperatorProof.operator_graph line 25
5. lemma OAI.SharpLiebThirring.OperatorProof.operator_associated line 62