OAI/NumberTheory/Jacobsthal/Estimates/LargeGapCountErrors.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos970.NumberTheoryLean.FiniteErrorTelescoping.endpoint_difference_le line 15
  2. theorem OAI.Erdos970.NumberTheoryLean.FiniteErrorTelescoping.exists_large_edge line 38
  3. theorem OAI.Erdos970.NumberTheoryLean.FiniteErrorTelescoping.witness_from_endpoints line 45
  4. def OAI.Erdos970.NumberTheoryLean.ActualCountErrorEdges.relativeCountError line 68
  5. def OAI.Erdos970.NumberTheoryLean.ActualCountErrorEdges.wordCountError line 70
  6. theorem OAI.Erdos970.NumberTheoryLean.ActualCountErrorEdges.relative_error_increment line 73
  7. theorem OAI.Erdos970.NumberTheoryLean.ActualCountErrorEdges.relative_large_edge_iff line 86
  8. theorem OAI.Erdos970.NumberTheoryLean.ActualCountErrorEdges.word_large_edge_iff line 99
  9. theorem OAI.Erdos970.NumberTheoryLean.ActualCountErrorMass.count_error_identity line 115
  10. theorem OAI.Erdos970.NumberTheoryLean.ActualCountErrorMass.word_count_error_weight line 128
  11. theorem OAI.Erdos970.NumberTheoryLean.ActualCountErrorMass.finite_count_error_weight line 136
  12. def OAI.Erdos970.NumberTheoryLean.CountErrorClassification.errorSum line 153
  13. def OAI.Erdos970.NumberTheoryLean.CountErrorClassification.largeGapWords line 155
  14. def OAI.Erdos970.NumberTheoryLean.CountErrorClassification.smallErrorWords line 157
  15. def OAI.Erdos970.NumberTheoryLean.CountErrorClassification.badCompactWords line 160
  16. theorem OAI.Erdos970.NumberTheoryLean.CountErrorClassification.error_sum_partition line 164
  17. theorem OAI.Erdos970.NumberTheoryLean.LiteralCountErrorLedger.negative_abs_le_signed line 190
  18. theorem OAI.Erdos970.NumberTheoryLean.LiteralCountErrorLedger.literal_count_error_ledger line 194
  19. theorem OAI.Erdos970.NumberTheoryLean.LiteralCountErrorLedger.expanded_reference_subset line 221
  20. theorem OAI.Erdos970.NumberTheoryLean.ReferenceCountEnvelope.reference_count_envelope line 236
  21. theorem OAI.Erdos970.NumberTheoryLean.CountErrorFamilyMajorant.count_error_family_majorant line 277
  22. theorem OAI.Erdos970.NumberTheoryLean.LargeGapCountErrors.uniform_large_gap_count_errors line 323