OAI/MathematicalPhysics/NavierStokes/BalancedTransport/EffectiveLog.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BalancedTransport.Effectivity.computable_rat_lt line 10
  2. def OAI.BalancedTransport.Effectivity.logBracket line 18
  3. instance OAI.BalancedTransport.Effectivity.(instance at line 24) line 24
  4. lemma OAI.BalancedTransport.Effectivity.computable_logBracket line 27
  5. lemma OAI.BalancedTransport.Effectivity.cast_error line 44
  6. lemma OAI.BalancedTransport.Effectivity.error_tendsto line 47
  7. lemma OAI.BalancedTransport.Effectivity.exists_logBracket line 50
  8. lemma OAI.BalancedTransport.Effectivity.logBracket_spec line 78
  9. def OAI.BalancedTransport.Effectivity.logSearchPredicate line 96
  10. instance OAI.BalancedTransport.Effectivity.(instance at line 99) line 99
  11. lemma OAI.BalancedTransport.Effectivity.exists_logSearchPredicate line 104
  12. def OAI.BalancedTransport.Effectivity.logCutoff line 109
  13. lemma OAI.BalancedTransport.Effectivity.computable_logCutoff line 111
  14. def OAI.BalancedTransport.Effectivity.logApprox line 117
  15. lemma OAI.BalancedTransport.Effectivity.computable_logApprox line 120
  16. lemma OAI.BalancedTransport.Effectivity.logApprox_spec line 125
  17. lemma OAI.BalancedTransport.Effectivity.log_abs_bound line 132