OAI/NumberTheory/Jacobsthal/Partitions/DilationCoordinates.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos970.ErdosHyperbolaError.nonzeroFrequencies line 15
  2. def OAI.Erdos970.ErdosHyperbolaError.intervalLength line 18
  3. def OAI.Erdos970.ErdosHyperbolaError.l1Norm line 20
  4. def OAI.Erdos970.ErdosHyperbolaError.gcdL1Norm line 23
  5. theorem OAI.Erdos970.ErdosHyperbolaError.l1Norm_nonneg line 26
  6. theorem OAI.Erdos970.ErdosHyperbolaError.gcdL1Norm_nonneg line 30
  7. theorem OAI.Erdos970.ErdosHyperbolaError.l1Norm_le line 34
  8. theorem OAI.Erdos970.ErdosHyperbolaError.gcdL1Norm_le line 38
  9. theorem OAI.Erdos970.ErdosHyperbolaError.intervalLength_nonneg line 43
  10. theorem OAI.Erdos970.ErdosHyperbolaError.weight_zero_eq_count line 46
  11. theorem OAI.Erdos970.ErdosHyperbolaError.interval_count_error line 50
  12. theorem OAI.Erdos970.ErdosHyperbolaError.interval_average_le_length line 55
  13. theorem OAI.Erdos970.ErdosHyperbolaError.interval_count_le_length_add_one line 62
  14. theorem OAI.Erdos970.ErdosHyperbolaError.norm_weight_zero_le line 68
  15. theorem OAI.Erdos970.ErdosHyperbolaError.unit_mul_eq_iff line 83
  16. def OAI.Erdos970.ErdosHyperbolaError.inverseResidue line 93
  17. theorem OAI.Erdos970.ErdosHyperbolaError.inverseResidue_cast line 96
  18. theorem OAI.Erdos970.ErdosHyperbolaError.residue_dilation_iff line 101
  19. def OAI.Erdos970.ErdosHyperbolaError.pulledInterval line 107
  20. theorem OAI.Erdos970.ErdosHyperbolaError.pulledInterval_length line 117
  21. theorem OAI.Erdos970.ErdosHyperbolaError.pulledInterval_ordered line 122
  22. theorem OAI.Erdos970.ErdosHyperbolaError.mem_pulledInterval_iff line 127
  23. def OAI.Erdos970.ErdosHyperbolaError.dilatePair line 139
  24. theorem OAI.Erdos970.ErdosHyperbolaError.dilatePair_injective line 141