OAI/NumberTheory/Jacobsthal/Partitions/IntervalHyperbolaAdapter.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.ErdosHyperbolaFourier.norm_characterProgression_le line 12
  2. theorem OAI.Erdos970.ErdosHyperbolaFourier.characterProgression_modulus_one line 28
  3. def OAI.Erdos970.ErdosHyperbolaFourier.intervalWeight line 44
  4. theorem OAI.Erdos970.ErdosHyperbolaFourier.intervalWeight_eq_progression line 48
  5. theorem OAI.Erdos970.ErdosHyperbolaFourier.intervalWeight_zero line 68
  6. theorem OAI.Erdos970.ErdosHyperbolaFourier.intervalWeight_zero_error line 72
  7. theorem OAI.Erdos970.ErdosHyperbolaFourier.norm_intervalWeight_le line 80
  8. theorem OAI.Erdos970.ErdosHyperbolaFourier.norm_intervalWeight_le_of_coprime line 87
  9. theorem OAI.Erdos970.ErdosHyperbolaFourier.progressionPoints_eq_literal_filter line 103
  10. theorem OAI.Erdos970.ErdosHyperbolaFourier.progressionPoints_open_singleton_empty line 125
  11. theorem OAI.Erdos970.ErdosHyperbolaFourier.literal_filter_zero_weight line 132
  12. structure OAI.Erdos970.ErdosHyperbolaIdentities.ProgressionInterval line 149
  13. def OAI.Erdos970.ErdosHyperbolaIdentities.ProgressionInterval.points line 158
  14. def OAI.Erdos970.ErdosHyperbolaIdentities.ProgressionInterval.weight line 161
  15. theorem OAI.Erdos970.ErdosHyperbolaIdentities.mem_interval_points line 165
  16. theorem OAI.Erdos970.ErdosHyperbolaIdentities.integerWeight_interval line 173
  17. theorem OAI.Erdos970.ErdosHyperbolaIdentities.interval_count_eq_fourier line 176