OAI/MathematicalPhysics/RapidForcing/SyntaxComputable.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RapidForcing.EffectiveArithmetic.computable_fin_eval line 10
  2. lemma OAI.RapidForcing.EffectiveArithmetic.computable_fin_apply line 12
  3. lemma OAI.RapidForcing.EffectiveArithmetic.computable_list_map line 15
  4. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_const line 28
  5. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_var line 29
  6. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_profile line 30
  7. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_add line 31
  8. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_mul line 32
  9. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_diff_comp line 33
  10. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_spaceIndex line 36
  11. abbrev OAI.RapidForcing.EffectiveProfile.Formula.MovingArgs line 38
  12. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_neg line 39
  13. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_sub line 40
  14. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_listSum line 41
  15. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_listProd line 43
  16. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_switch line 45
  17. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_theta line 46
  18. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_thetaDot line 47
  19. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_zeta line 48
  20. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_crossF line 51
  21. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_curlF line 55
  22. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_moving line 59
  23. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_sumVector line 84
  24. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_residualFormula line 89
  25. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_iterate_diff line 111
  26. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_iterate_diff_comp line 114
  27. lemma OAI.RapidForcing.EffectiveProfile.Formula.computable_mixed line 119