OAI/Analysis/CoulombRadii/FieldAnalysis/CoulombBilinear.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.fineKernel_continuous line 117
2. lemma OAI.Coulomb.flatFineKernel_neg line 129
3. lemma OAI.Coulomb.fineKernel_neg line 131
4. lemma OAI.Coulomb.fineKernel_isometry line 139
5. lemma OAI.Coulomb.fineKernel_radial line 183
6. lemma OAI.Coulomb.fineKernel_profile line 189
7. lemma OAI.Coulomb.fineKernel_coulomb_integrable line 194
8. lemma OAI.Coulomb.fineKernel_coulomb_le line 199
9. lemma OAI.Coulomb.fineKernel_coulomb_eq line 205
10. def OAI.Coulomb.coulombBilinear line 216
11. lemma OAI.Coulomb.coulombBilinear_iterated line 219
12. lemma OAI.Coulomb.fineKernel_shift_integrable line 232
13. lemma OAI.Coulomb.fineKernel_shift_integral line 235
14. lemma OAI.Coulomb.fineKernel_shift_coulomb_integral line 239
15. lemma OAI.Coulomb.fineKernel_coulomb_bound line 248
16. lemma OAI.Coulomb.fineKernel_pair_le line 255
17. lemma OAI.Coulomb.fineKernel_pair_self_le line 294