OAI/Analysis/CoulombRadii/Localization/DyadicTailPartial.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.dyadic_tail_partial_le line 13
2. lemma OAI.Coulomb.dyadic_tail_hasSum line 30
3. lemma OAI.Coulomb.pow_eight_two_thirds line 44
4. lemma OAI.Coulomb.dyadic_density_bound line 53
5. lemma OAI.Coulomb.dyadic_spectral_tail_bound line 97