OAI/NumberTheory/Ostmann/Arithmetic/HistorySmoothWeightCutoff.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Arithmetic.giantCell line 10
  2. theorem OAI.Ostmann.Arithmetic.giantCell_of_pos line 13
  3. theorem OAI.Ostmann.Arithmetic.giantCell_of_nonpos line 17
  4. theorem OAI.Ostmann.Arithmetic.giantCell_bounds line 20
  5. theorem OAI.Ostmann.Arithmetic.giantCell_zero_of_le_lower line 27
  6. theorem OAI.Ostmann.Arithmetic.giantCell_zero_of_upper_le line 36
  7. theorem OAI.Ostmann.Arithmetic.giantCell_eventually_zero line 45
  8. theorem OAI.Ostmann.Arithmetic.giantCell_contDiff line 51
  9. theorem OAI.Ostmann.Arithmetic.giantCell_log_deriv line 63
  10. theorem OAI.Ostmann.Arithmetic.giantCell_log_deriv_bound line 74