OAI/NumberTheory/Ostmann/Arithmetic/PrimeCellIntegralFreezing.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Ostmann.Arithmetic.PrimeCellFreezing.logCellIntegral line 11
2. theorem OAI.Ostmann.Arithmetic.PrimeCellFreezing.logCell_freezing_of_variation line 15
3. theorem OAI.Ostmann.Arithmetic.PrimeCellFreezing.logRectangle_coordinate_dist_le line 49
4. theorem OAI.Ostmann.Arithmetic.PrimeCellFreezing.positive_integral_freezing_bound line 58
5. theorem OAI.Ostmann.Arithmetic.PrimeCellFreezing.residue_integral_freezing_bound line 77