OAI/MathematicalPhysics/NavierStokes/BalancedTransport/NumericEvaluation.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BalancedTransport.Effectivity.NumericOp.magnitude line 8
  2. def OAI.BalancedTransport.Effectivity.NumericProgram.realFrom line 40
  3. def OAI.BalancedTransport.Effectivity.NumericProgram.rationalFrom line 43
  4. def OAI.BalancedTransport.Effectivity.NumericProgram.boundFrom line 46
  5. def OAI.BalancedTransport.Effectivity.NumericProgram.ValidFrom line 49
  6. def OAI.BalancedTransport.Effectivity.NumericProgram.Valid line 53
  7. def OAI.BalancedTransport.Effectivity.NumericProgram.real line 55
  8. def OAI.BalancedTransport.Effectivity.NumericProgram.bound line 57
  9. def OAI.BalancedTransport.Effectivity.NumericProgram.approximation line 59
  10. lemma OAI.BalancedTransport.Effectivity.NumericProgram.boundFrom_estimate line 62
  11. lemma OAI.BalancedTransport.Effectivity.NumericProgram.boundFrom_magnitude line 82
  12. lemma OAI.BalancedTransport.Effectivity.NumericProgram.approximation_spec line 96
  13. lemma OAI.BalancedTransport.Effectivity.NumericProgram.magnitude line 103
  14. lemma OAI.BalancedTransport.Effectivity.NumericProgram.computable_rationalStep line 107
  15. lemma OAI.BalancedTransport.Effectivity.NumericProgram.computable_rationalFrom line 122
  16. lemma OAI.BalancedTransport.Effectivity.NumericProgram.computable_boundStep line 131
  17. lemma OAI.BalancedTransport.Effectivity.NumericProgram.computable_boundFrom line 144
  18. lemma OAI.BalancedTransport.Effectivity.NumericProgram.computable_bound line 151
  19. lemma OAI.BalancedTransport.Effectivity.NumericProgram.computable_approximation line 156