OAI/Analysis/LiebThirring/FormCongruence.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpLiebThirring.OperatorProof.form_congr_ae line 11
2. lemma OAI.SharpLiebThirring.OperatorProof.toH1_ofH1_val line 24
3. lemma OAI.SharpLiebThirring.OperatorProof.toH1_ofH1_grad line 27
4. lemma OAI.SharpLiebThirring.OperatorProof.form_ofH1 line 30
5. lemma OAI.SharpLiebThirring.OperatorProof.ofH1_toH1 line 35
6. lemma OAI.SharpLiebThirring.OperatorProof.form_eq_of_valLp_eq line 39
7. def OAI.SharpLiebThirring.OperatorProof.IsAssociated line 47

   Source documentation

   The usual graph characterization of the operator associated with a closed semibounded form. The quantifier is over the entire weak H¹ domain.

   def IsAssociated (W : ℝ → ℝ) (A : L2C →ₗ.[ℂ] L2C) : Prop :=
   …

   Mentions: OAI.SharpLiebThirring.OperatorProof.L2C

8. lemma OAI.SharpLiebThirring.OperatorProof.isAssociated_iff_graph line 52
9. lemma OAI.SharpLiebThirring.OperatorProof.negativeEigenfunction_iff_operator line 76