OAI/Geometry/WeakHessian/Transport/UpperEnvelope.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakHessianTransport.exists_sublinear_support line 31
2. def OAI.WeakHessianTransport.upperEnvelope line 68
3. lemma OAI.WeakHessianTransport.envelope_nonempty line 77
4. lemma OAI.WeakHessianTransport.envelope_bddBelow line 83
5. lemma OAI.WeakHessianTransport.lower_le_envelope line 90
6. lemma OAI.WeakHessianTransport.envelope_le line 97
7. lemma OAI.WeakHessianTransport.envelope_image line 102
8. lemma OAI.WeakHessianTransport.envelope_zero line 108
9. lemma OAI.WeakHessianTransport.envelope_mono line 113
10. lemma OAI.WeakHessianTransport.envelope_lt line 121
11. lemma OAI.WeakHessianTransport.envelope_add line 128
12. lemma OAI.WeakHessianTransport.envelope_smul line 140
13. lemma OAI.WeakHessianTransport.exists_envelope_support line 166