OAI/Analysis/CoulombRadii/FormDomain/L2TightCompact.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.cutL2_sub_self line 14
2. lemma OAI.Coulomb.double_cut_approximation line 18
3. lemma OAI.Coulomb.l2_tight_frequency_subsequence line 34
4. lemma OAI.Coulomb.l2_real_test_inner line 93
5. lemma OAI.Coulomb.weak_l2_pairing_tendsto line 100
6. lemma OAI.Coulomb.weak_l2_derivative_limit line 106
7. lemma OAI.Coulomb.h1_spatial_tight_subsequence line 129