OAI/Analysis/CoulombRadii/FormDomain/WeakFourierDerivative.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Coulomb.l2_weakDeriv_fourier line 15
2. lemma OAI.Coulomb.l2_weakDeriv_fourier_energy line 53
3. def OAI.Coulomb.cutL2 line 77
4. lemma OAI.Coulomb.cutL2_ae line 79
5. lemma OAI.Coulomb.cutL2_norm_le line 81
6. lemma OAI.Coulomb.cutL2_sub line 87
7. lemma OAI.Coulomb.cutL2_add_compl line 98
8. lemma OAI.Coulomb.l2_norm_sq_integral line 107
9. lemma OAI.Coulomb.cutL2_norm_sq line 118
10. lemma OAI.Coulomb.cutL2_mono_norm line 125
11. lemma OAI.Coulomb.l2_gradient_fourier_moment line 143
12. lemma OAI.Coulomb.l2_fourier_tail_bound line 161
13. lemma OAI.Coulomb.bounded_gradient_frequency_tight line 180