OAI/NumberTheory/DirichletL/Detector/LowCutoff.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SevenEighths.ProbePhysical.lowOuterCutoff line 11
2. lemma OAI.SevenEighths.ProbePhysical.lowOuterCutoff_small line 14
3. lemma OAI.SevenEighths.ProbePhysical.lowOuterCutoff_large line 21
4. lemma OAI.SevenEighths.ProbePhysical.lowOuterCutoff_one line 28
5. lemma OAI.SevenEighths.ProbePhysical.lowOuterCutoff_smooth line 39
6. lemma OAI.SevenEighths.ProbePhysical.lowOuterCutoff_support line 44
7. lemma OAI.SevenEighths.ProbePhysical.lowOuterCutoff_compact line 53
8. lemma OAI.SevenEighths.ProbePhysical.physical_ratio_factor line 57
9. lemma OAI.SevenEighths.ProbePhysical.physical_window_cutoff_one line 61
10. theorem OAI.SevenEighths.ProbePhysical.physicalRowWeight_insert_cutoff line 78