OAI/NumberTheory/DirichletL/RowCompletion/ZeroFreeRegion.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CanonicalRowCompletion.ActualFiber.reflectedFiber_four_mul_value line 89
2. theorem OAI.CanonicalRowCompletion.ActualFiber.completedT_eq_reflectedFiber_idealValue line 139
3. def OAI.CanonicalRowCompletion.actualReflectionScale line 171
4. theorem OAI.CanonicalRowCompletion.actual_fixedShellModels line 174
5. theorem OAI.CanonicalRowCompletion.exists_actual_fixedShellModels line 188
6. theorem OAI.CanonicalRowCompletion.dirichletTarget_unconditional line 197
7. theorem OAI.ShortDraft.dirichlet_LFunction_ne_zero line 204
8. theorem OAI.ShortDraft.riemannZeta_ne_zero_of_re_gt line 210