OAI/NumberTheory/Jacobsthal/Estimates/UnitCyclicBounds.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.ErdosHyperbola.harmonicWeight_eq line 12
  2. def OAI.Erdos970.ErdosHyperbola.harmonicConstant line 16
  3. theorem OAI.Erdos970.ErdosHyperbola.harmonicConstant_pos line 18
  4. theorem OAI.Erdos970.ErdosHyperbola.harmonicWeight_log_le line 23
  5. theorem OAI.Erdos970.ErdosHyperbola.gcd_harmonic_log_le line 40
  6. theorem OAI.Erdos970.ErdosHyperbola.cyclic_weight_sum_le line 63
  7. theorem OAI.Erdos970.ErdosHyperbola.sum_representatives_le line 89
  8. theorem OAI.Erdos970.ErdosHyperbolaWeighted.log_two_mul_le_power line 121
  9. theorem OAI.Erdos970.ErdosHyperbola.gcd_val_neg line 145
  10. theorem OAI.Erdos970.ErdosHyperbola.cyclic_inverse_sum_le line 152
  11. theorem OAI.Erdos970.ErdosHyperbola.sqrt_gcd_cyclic_sum_le line 164
  12. def OAI.Erdos970.ErdosHyperbola.mulUnitEquiv line 196
  13. theorem OAI.Erdos970.ErdosHyperbola.mulUnitEquiv_apply line 202
  14. theorem OAI.Erdos970.ErdosHyperbola.gcd_mul_unit line 205
  15. theorem OAI.Erdos970.ErdosHyperbola.unit_cyclic_inverse_sum_le line 212
  16. theorem OAI.Erdos970.ErdosHyperbola.unit_sqrt_gcd_cyclic_sum_le line 221