OAI/Geometry/CAT0Fillings/Slicing/WeakRestriction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CAT0Fillings.Slicing.levelBarrier line 95
2. lemma OAI.CAT0Fillings.Slicing.levelBarrier_bounds line 99
3. lemma OAI.CAT0Fillings.Slicing.levelBarrier_boundedLip line 106
4. lemma OAI.CAT0Fillings.Slicing.profile_error_le_levelBarrier line 127
5. lemma OAI.CAT0Fillings.Slicing.levelBarrier_integral_tendsto line 139
6. lemma OAI.CAT0Fillings.Slicing.restrictCurrent_apply_of_controls line 158
7. lemma OAI.CAT0Fillings.Slicing.restriction_profile_error_bound line 168
8. theorem OAI.CAT0Fillings.Slicing.restrictCurrent_weak_tendsto line 199