OAI/NumberTheory/CubicMoment/Estimates/ProfileCommonSmall.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CubicFirstMoment.ProfileControl.smallB_coprime_dispersion_height_power line 9
2. theorem OAI.CubicFirstMoment.ProfileControl.smallB_coprime_height_real line 38
3. theorem OAI.CubicFirstMoment.ProfileControl.smallB_common_row_height_power line 87
4. theorem OAI.CubicFirstMoment.ProfileControl.smallB_common_block_height_power line 157
5. theorem OAI.CubicFirstMoment.ProfileControl.smallB_common_sum_height_power line 221