OAI/NumberTheory/Ostmann/Arithmetic/HistorySmoothWeightExprDeriv.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Ostmann.Characters.RationalHistory.Expr.logCurve line 10
  2. theorem OAI.Ostmann.Characters.RationalHistory.Expr.logCurve_zero line 13
  3. def OAI.Ostmann.Characters.RationalHistory.Expr.logDerivative line 17
  4. theorem OAI.Ostmann.Characters.RationalHistory.Expr.hasDerivAt_logCurve line 26
  5. def OAI.Ostmann.Characters.RationalHistory.Expr.logSlope line 45
  6. theorem OAI.Ostmann.Characters.RationalHistory.Expr.logSlope_mul line 47
  7. theorem OAI.Ostmann.Characters.RationalHistory.Expr.logSlope_divide line 53
  8. theorem OAI.Ostmann.Characters.RationalHistory.Expr.logSlope_add line 59
  9. theorem OAI.Ostmann.Characters.RationalHistory.Expr.logSlope_sub line 68