OAI/Analysis/FreeGroupFactor/NCPolynomial.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.FreeGroupFactorMain.NCPolynomial.Expr line 16
  2. def OAI.FreeGroupFactorMain.NCPolynomial.degree line 22
  3. def OAI.FreeGroupFactorMain.NCPolynomial.mass line 28
  4. def OAI.FreeGroupFactorMain.NCPolynomial.eval line 34
  5. def OAI.FreeGroupFactorMain.NCPolynomial.delta line 40
  6. theorem OAI.FreeGroupFactorMain.NCPolynomial.mass_nonneg line 46
  7. theorem OAI.FreeGroupFactorMain.NCPolynomial.degree_delta line 53
  8. theorem OAI.FreeGroupFactorMain.NCPolynomial.mass_delta line 66
  9. theorem OAI.FreeGroupFactorMain.NCPolynomial.degree_iterate line 95
  10. theorem OAI.FreeGroupFactorMain.NCPolynomial.mass_iterate line 104
  11. theorem OAI.FreeGroupFactorMain.NCPolynomial.norm_eval line 127
  12. theorem OAI.FreeGroupFactorMain.NCPolynomial.hasDerivAt_eval line 154
  13. theorem OAI.FreeGroupFactorMain.NCPolynomial.eval_delta line 164
  14. theorem OAI.FreeGroupFactorMain.NCPolynomial.norm_eval_iterate line 177
  15. theorem OAI.FreeGroupFactorMain.NCPolynomial.smooth_eval line 197
  16. theorem OAI.FreeGroupFactorMain.NCPolynomial.iteratedDeriv_eval line 206