OAI/MathematicalPhysics/RecorderFlows/Effective.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Finite oracle programs and effective mixed-derivative evaluation.

  1. inductive OAI.Solenoidal.Effective.OracleCode line 10
  2. def OAI.Solenoidal.Effective.OracleCode.eval line 18
  3. def OAI.Solenoidal.Effective.decodeRat line 34
  4. def OAI.Solenoidal.Effective.tolerance line 36
  5. def OAI.Solenoidal.Effective.Names line 38
  6. def OAI.Solenoidal.Effective.ComputableReal line 41
  7. def OAI.Solenoidal.Effective.NamesArguments line 47
  8. def OAI.Solenoidal.Effective.machineCode line 52
  9. def OAI.Solenoidal.Effective.wordCode line 61
  10. def OAI.Solenoidal.Effective.request line 64
  11. def OAI.Solenoidal.Effective.boundRequest line 67
  12. abbrev OAI.Solenoidal.Effective.ForceFamily line 70
  13. def OAI.Solenoidal.Effective.RelativeEffective line 74
  14. def OAI.Solenoidal.Effective.SuppliesArgument line 88
  15. def OAI.Solenoidal.Effective.EffectiveAt line 94