OAI/Analysis/CoulombRadii/FormDomain/PatchErrors.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Coulomb.unitWindowKinetic line 14
2. lemma OAI.Coulomb.unitWindowKinetic_nonneg line 15
3. lemma OAI.Coulomb.patch_packet_bound line 17
4. lemma OAI.Coulomb.weighted_cap_integrable line 39
5. lemma OAI.Coulomb.slice_ensemble_mean_le_sqrt line 46
6. lemma OAI.Coulomb.ensemble_number_rpow line 62
7. lemma OAI.Coulomb.ensemble_number_mean line 76