OAI/Analysis/LiebThirring/FreeForm.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

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

   Source documentation

   Positive free form ∫|u'|² + a∫|u|² on the full H¹ graph.

   def freeFormMap (a : ℝ) : H1C →L[ℂ] H1C :=
   …

   Mentions: OAI.SharpLiebThirring.OperatorProof.H1C

2. lemma OAI.SharpLiebThirring.OperatorProof.freeFormMap_inner line 15
3. lemma OAI.SharpLiebThirring.OperatorProof.freeFormMap_coercive line 22
4. lemma OAI.SharpLiebThirring.OperatorProof.freeFormMap_bijective line 32
5. def OAI.SharpLiebThirring.OperatorProof.freeFormEquiv line 35
6. def OAI.SharpLiebThirring.OperatorProof.energyFormMap line 41

   Source documentation

   Form of H+a on H¹.

   def energyFormMap {W : ℝ → ℝ} (d : PotentialData W) (a : ℝ) : H1C →L[ℂ] H1C :=
   …

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

7. lemma OAI.SharpLiebThirring.OperatorProof.energyFormMap_inner line 44