OAI/NumberTheory/DirichletL/Detector/GaussianPartition.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.ProbePhysical.gaussianCutoff line 11
2. def OAI.SevenEighths.ProbePhysical.gaussianAnnulus line 12
3. lemma OAI.SevenEighths.ProbePhysical.gaussianCutoff_small line 14
4. lemma OAI.SevenEighths.ProbePhysical.gaussianCutoff_large line 16
5. lemma OAI.SevenEighths.ProbePhysical.gaussianAnnulus_small line 18
6. lemma OAI.SevenEighths.ProbePhysical.gaussianAnnulus_large line 20
7. lemma OAI.SevenEighths.ProbePhysical.gaussianAnnulus_contDiff line 22
8. lemma OAI.SevenEighths.ProbePhysical.gaussianAnnulus_compact line 26
9. lemma OAI.SevenEighths.ProbePhysical.gaussianAnnulus_nonneg line 36
10. lemma OAI.SevenEighths.ProbePhysical.gaussianAnnulus_norm line 41
11. lemma OAI.SevenEighths.ProbePhysical.gaussianAnnulus_support_scales line 47
12. lemma OAI.SevenEighths.ProbePhysical.gaussianAnnulus_partition line 65
13. lemma OAI.SevenEighths.ProbePhysical.gaussianAnnulus_partition_norm line 82