OAI/NumberTheory/Ostmann/Arithmetic/HistoryBulkReplacementErrorBasic.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Ostmann.Arithmetic.HistoryBulkReplacementError.bulkNormalizer_bounds_eventually line 17
  2. theorem OAI.Ostmann.Arithmetic.HistoryBulkReplacementError.bulk_harmonicIntegral line 27
  3. theorem OAI.Ostmann.Arithmetic.HistoryBulkReplacementError.bulk_principalMass_bounds line 34
  4. def OAI.Ostmann.Arithmetic.HistoryBulkReplacementError.residueCostExponent line 55
  5. theorem OAI.Ostmann.Arithmetic.HistoryBulkReplacementError.modulus_power_growth_le line 57
  6. theorem OAI.Ostmann.Arithmetic.HistoryBulkReplacementError.growth_mono line 74
  7. theorem OAI.Ostmann.Arithmetic.HistoryBulkReplacementError.growth_one_le line 79
  8. theorem OAI.Ostmann.Arithmetic.HistoryBulkReplacementError.two_le_growth line 82
  9. theorem OAI.Ostmann.Arithmetic.HistoryBulkReplacementError.amplitude_growth_le line 88
  10. theorem OAI.Ostmann.Arithmetic.HistoryBulkReplacementError.derivative_amplitude_growth_le line 94