OAI/NumberTheory/DirichletL/Detector/CorrectionBounds.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SevenEighths.ProbeLocal.one_sub_ne_zero_of_norm_le_half line 11
2. lemma OAI.SevenEighths.ProbeLocal.inv_one_sub_norm_le_two line 17
3. theorem OAI.SevenEighths.ProbeLocal.unramified_marked_error_bound line 24
4. theorem OAI.SevenEighths.ProbeLocal.continuedCorrection_defect_bound line 56