OAI/Probability/SKValue/Equations/ShortStripClose.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SKValue.weighted_bound_algebra line 12
2. lemma OAI.SKValue.SmoothEvolution.short_strip_jet_bound line 31
3. def OAI.SKValue.lowerJetConstant line 67
4. lemma OAI.SKValue.lowerJetConstant_nonneg line 70
5. lemma OAI.SKValue.SmoothTerminal.product_jet_bound line 74
6. lemma OAI.SKValue.exists_short_length line 114
7. theorem OAI.SKValue.uniform_bulk_jets line 128