OAI/NumberTheory/DirichletL/Detector/GaussianSeminorm.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.ProbePhysical.gaussianFixedWindow line 10
2. lemma OAI.SevenEighths.ProbePhysical.gaussianFixedWindow_small line 11
3. lemma OAI.SevenEighths.ProbePhysical.gaussianFixedWindow_large line 13
4. lemma OAI.SevenEighths.ProbePhysical.gaussianFixedWindow_compact line 15
5. lemma OAI.SevenEighths.ProbePhysical.gaussianFixedWindow_contDiff line 22
6. def OAI.SevenEighths.ProbePhysical.gaussianFixedSchwartz line 36
7. lemma OAI.SevenEighths.ProbePhysical.gaussianProfile_scaled_smooth line 38
8. lemma OAI.SevenEighths.ProbePhysical.gaussianDyadicProfile_factor line 45
9. lemma OAI.SevenEighths.ProbePhysical.gaussianDyadicProfile_derivative_outside line 53
10. lemma OAI.SevenEighths.ProbePhysical.gaussianDyadicProfile_derivative_uniform line 65
11. theorem OAI.SevenEighths.ProbePhysical.gaussianDyadicSchwartz_seminorm line 96
12. theorem OAI.SevenEighths.ProbePhysical.gaussianDyadicSchwartz_finite_seminorm line 116
13. theorem OAI.SevenEighths.ProbePhysical.gaussianDyadicSchwartz_two_sided line 137