OAI/MathematicalPhysics/NavierStokes/BalancedTransport/EffectiveExp.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.BalancedTransport.Effectivity.expAccurate line 11
2. instance OAI.BalancedTransport.Effectivity.(instance at line 15) line 15
3. lemma OAI.BalancedTransport.Effectivity.computable_decide_and line 18
4. lemma OAI.BalancedTransport.Effectivity.computable_expAccurate line 25
5. lemma OAI.BalancedTransport.Effectivity.exists_expAccurate line 41
6. def OAI.BalancedTransport.Effectivity.expCutoff line 59
7. lemma OAI.BalancedTransport.Effectivity.computable_expCutoff line 62
8. def OAI.BalancedTransport.Effectivity.expApprox line 65
9. lemma OAI.BalancedTransport.Effectivity.computable_expApprox line 68
10. lemma OAI.BalancedTransport.Effectivity.real_exp_tail_bound line 75
11. lemma OAI.BalancedTransport.Effectivity.expApprox_spec line 85