OAI/NumberTheory/DirichletL/Inversion/SecondChildWindows.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SevenEighths.InverseSecondChildWindows.positive_cutoff line 14
2. theorem OAI.SevenEighths.InverseSecondChildWindows.positiveSource_log_bound line 36
3. theorem OAI.SevenEighths.InverseSecondChildWindows.positiveSource_ratio_support line 48
4. theorem OAI.SevenEighths.InverseSecondChildWindows.translated_log_bound line 56
5. def OAI.SevenEighths.InverseSecondChildWindows.outerIndex line 69
6. theorem OAI.SevenEighths.InverseSecondChildWindows.fixed_windows line 71
7. def OAI.SevenEighths.InverseSecondChildWindows.actualOuterRatios line 142
8. lemma OAI.SevenEighths.InverseSecondChildWindows.actualRelativeNorm_outer line 148
9. theorem OAI.SevenEighths.InverseSecondChildWindows.actual_second_child_windows line 156