OAI/Analysis/CoulombRadii/FormDomain/Pullback.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.linear_form_eq_sum line 56
2. lemma OAI.Coulomb.H1Vector.weak_directional line 63
3. lemma OAI.Coulomb.H1Vector.weak_partial_isometry line 93
4. def OAI.Coulomb.H1Vector.pullback line 117
5. lemma OAI.Coulomb.isometry_complex_gradient_sq line 126
6. lemma OAI.Coulomb.mass_pullback line 143
7. lemma OAI.Coulomb.kinetic_pullback line 151
8. lemma OAI.Coulomb.test_L2 line 167
9. lemma OAI.Coulomb.test_derivative_L2 line 173
10. def OAI.Coulomb.H1Vector.scale line 180
11. def OAI.Coulomb.H1Vector.finiteSum line 190
12. def OAI.Coulomb.permutationIsometry line 207
13. lemma OAI.Coulomb.permutationIsometry_apply line 211
14. lemma OAI.Coulomb.permutationIsometry_single line 216
15. def OAI.Coulomb.H1Vector.permutation line 223
16. lemma OAI.Coulomb.permutation_value line 231
17. lemma OAI.Coulomb.permutation_gradient line 236
18. lemma OAI.Coulomb.permute_one line 245
19. lemma OAI.Coulomb.permute_mul line 247
20. lemma OAI.Coulomb.permute_inv line 250
21. lemma OAI.Coulomb.permute_integral line 253
22. def OAI.Coulomb.permutationSpins line 259
23. lemma OAI.Coulomb.permutationSpins_apply line 261
24. lemma OAI.Coulomb.sign_complex_sq line 264
25. lemma OAI.Coulomb.sign_complex_mul line 268
26. def OAI.Coulomb.H1Vector.fullAntisymmetrize line 272
27. lemma OAI.Coulomb.fullAntisymmetrize_value line 276
28. lemma OAI.Coulomb.fullAntisymmetrize_antisymmetric line 281