OAI/MathematicalPhysics/AlternatingFlow/Quantitative.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AlternatingNS.Quantitative.rhoTerm line 12
2. lemma OAI.AlternatingNS.Quantitative.rhoTerm_smooth line 14
3. lemma OAI.AlternatingNS.Quantitative.rhoTerm_deriv line 19
4. lemma OAI.AlternatingNS.Quantitative.exp_monomial_bound line 33
5. lemma OAI.AlternatingNS.Quantitative.rhoTerm_bound line 43
6. lemma OAI.AlternatingNS.Quantitative.rhoTerm_derivative_bound line 51
7. lemma OAI.AlternatingNS.Quantitative.rho_derivative_bound line 85
8. def OAI.AlternatingNS.Quantitative.rhoBound line 90
9. lemma OAI.AlternatingNS.Quantitative.rho_jet_bound line 92
10. lemma OAI.AlternatingNS.Quantitative.transition_denom_lower line 97
11. lemma OAI.AlternatingNS.Quantitative.inverse_jet_bound line 115
12. def OAI.AlternatingNS.Quantitative.reciprocalBound line 125
13. lemma OAI.AlternatingNS.Quantitative.reciprocal_jet_bound line 129
14. def OAI.AlternatingNS.Quantitative.transitionDenom line 164
15. lemma OAI.AlternatingNS.Quantitative.transitionDenom_smooth line 166
16. lemma OAI.AlternatingNS.Quantitative.transitionDenom_bound line 169
17. def OAI.AlternatingNS.Quantitative.transitionInvBound line 186
18. lemma OAI.AlternatingNS.Quantitative.transitionInv_bound line 188
19. def OAI.AlternatingNS.Quantitative.transitionBound line 197
20. lemma OAI.AlternatingNS.Quantitative.transition_jet_bound line 200