OAI/Geometry/IntegralFillings/Slicing/Profiles.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpIntegralFillings.SmoothCutoff.profile line 32
2. def OAI.SharpIntegralFillings.SmoothCutoff.dprofile line 34
3. lemma OAI.SharpIntegralFillings.SmoothCutoff.affine_lipschitz line 37
4. lemma OAI.SharpIntegralFillings.SmoothCutoff.profile_hasDerivAt line 44
5. lemma OAI.SharpIntegralFillings.SmoothCutoff.profile_bounds line 52
6. lemma OAI.SharpIntegralFillings.SmoothCutoff.profile_zero line 56
7. lemma OAI.SharpIntegralFillings.SmoothCutoff.dprofile_zero line 59
8. lemma OAI.SharpIntegralFillings.SmoothCutoff.exists_profile_bounds line 75
9. lemma OAI.SharpIntegralFillings.SmoothCutoff.profile_sequence_tendsto line 91