OAI/Probability/LatticeSurface/Convexity/USCEnvelope.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.USCEnvelope.hypo line 15
2. def OAI.USCEnvelope.envelope line 17
3. lemma OAI.USCEnvelope.compact_hypo line 20
4. lemma OAI.USCEnvelope.nonempty_hypo line 32
5. lemma OAI.USCEnvelope.continuous_kernel line 37
6. lemma OAI.USCEnvelope.continuous_envelope line 41
7. lemma OAI.USCEnvelope.envelope_max line 45
8. lemma OAI.USCEnvelope.le_envelope line 52
9. lemma OAI.USCEnvelope.self_le_envelope line 59
10. lemma OAI.USCEnvelope.envelope_nonneg line 64
11. lemma OAI.USCEnvelope.envelope_pos line 71
12. lemma OAI.USCEnvelope.envelope_bound line 78
13. lemma OAI.USCEnvelope.tendsto_envelope line 88
14. lemma OAI.USCEnvelope.dist_combination line 120
15. lemma OAI.USCEnvelope.envelope_combination line 128