OAI/Analysis/CoulombRadii/FormDomain/H1VectorL2.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Coulomb.H1Vector.valueL2 line 14
2. def OAI.Coulomb.H1Vector.gradientL2 line 16
3. lemma OAI.Coulomb.H1Vector.valueL2_ae line 18
4. lemma OAI.Coulomb.H1Vector.gradientL2_ae line 20
5. lemma OAI.Coulomb.H1Vector.mass_eq_norm line 23
6. lemma OAI.Coulomb.H1Vector.kinetic_eq_norm line 30
7. lemma OAI.Coulomb.H1Vector.weak_partial_L2 line 41
8. def OAI.Coulomb.H1Vector.ofL2 line 57
9. lemma OAI.Coulomb.H1Vector.ofL2_valueL2 line 68
10. lemma OAI.Coulomb.H1Vector.ofL2_gradientL2 line 73
11. lemma OAI.Coulomb.antisymmetric_iff_valueL2 line 80
12. lemma OAI.Coulomb.antisymmetric_strong_limit line 105
13. lemma OAI.Coulomb.memlp_real_inner_integrable line 127
14. lemma OAI.Coulomb.l2_weakDeriv_skew line 136
15. lemma OAI.Coulomb.h1_green line 154
16. lemma OAI.Coulomb.h1_multiplier_ibp line 175