OAI/Analysis/BiholderTransport/Regularity/OuterTemplatePrimitive.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.WeakMTWTransport.outerTemplate_eq_primitive line 12
2. lemma OAI.WeakMTWTransport.outerTemplate_zero line 17
3. lemma OAI.WeakMTWTransport.outerTemplate_nonneg line 22
4. lemma OAI.WeakMTWTransport.outerTemplate_lower line 29
5. lemma OAI.WeakMTWTransport.outerTemplate_upper line 37
6. lemma OAI.WeakMTWTransport.outerTemplate_zero_level line 49
7. lemma OAI.WeakMTWTransport.centerTemplate_le_outer line 54
8. lemma OAI.WeakMTWTransport.outerPrimitive_core_gain line 62
9. lemma OAI.WeakMTWTransport.outerTemplate_barrier line 83