OAI/Probability/SKGap/Localization/PhiResponse.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKGap.Stein.phiR line 12
2. def OAI.SKGap.Stein.phiRZ line 13
3. lemma OAI.SKGap.Stein.phiR_hasDerivAt line 15
4. lemma OAI.SKGap.Stein.phiR_hasDerivAt_z line 17
5. lemma OAI.SKGap.Stein.phiZR_commute line 19
6. lemma OAI.SKGap.Stein.phiZ_kernel line 23
7. lemma OAI.SKGap.Stein.phiZ_hasDerivAt_r line 25
8. theorem OAI.SKGap.Stein.phiR_stein line 28
9. lemma OAI.SKGap.Stein.phiR_bound line 44