OAI/MathematicalPhysics/RapidForcing/ComputableProfiles.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.RapidForcing.EffectiveProfile.ballEquiv line 13
  2. instance OAI.RapidForcing.EffectiveProfile.(instance at line 15) line 15
  3. lemma OAI.RapidForcing.EffectiveProfile.primrec_ball_center line 16
  4. lemma OAI.RapidForcing.EffectiveProfile.primrec_ball_radius line 18
  5. lemma OAI.RapidForcing.EffectiveProfile.primrec_ball_mk line 20
  6. lemma OAI.RapidForcing.EffectiveProfile.computable_ball_exact line 23
  7. lemma OAI.RapidForcing.EffectiveProfile.computable_ball_add line 25
  8. lemma OAI.RapidForcing.EffectiveProfile.computable_ball_mul line 27
  9. lemma OAI.RapidForcing.EffectiveProfile.computable_ball_denInv line 29
  10. lemma OAI.RapidForcing.EffectiveProfile.computable_ball_pow line 31
  11. lemma OAI.RapidForcing.EffectiveProfile.computable_glueDiff line 37
  12. lemma OAI.RapidForcing.EffectiveProfile.computable_glueBound line 45
  13. lemma OAI.RapidForcing.EffectiveProfile.computable_sum_range line 52
  14. lemma OAI.RapidForcing.EffectiveProfile.computable_expTerms line 63
  15. lemma OAI.RapidForcing.EffectiveProfile.computable_taylor_term line 65
  16. lemma OAI.RapidForcing.EffectiveProfile.computable_taylor_sum line 67
  17. lemma OAI.RapidForcing.EffectiveProfile.computable_taylor_error_fn line 70
  18. lemma OAI.RapidForcing.EffectiveProfile.computable_expBall line 72
  19. lemma OAI.RapidForcing.EffectiveProfile.computable_monoBall line 78
  20. lemma OAI.RapidForcing.EffectiveProfile.computable_glueBall line 86
  21. lemma OAI.RapidForcing.EffectiveProfile.Expr.computable_bound line 93
  22. lemma OAI.RapidForcing.EffectiveProfile.Expr.computable_diff line 103
  23. lemma OAI.RapidForcing.EffectiveProfile.Expr.computable_numeric line 115
  24. lemma OAI.RapidForcing.EffectiveProfile.Expr.partrec_approx line 126