OAI/Geometry/CAT0Fillings/Calculus/Smoothing.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.hasFDerivAt_convolution_lipschitz line 32
2. lemma OAI.CAT0Fillings.locallyIntegrable_fderiv_lipschitz line 64
3. lemma OAI.CAT0Fillings.fderiv_bump_convolution line 71
4. lemma OAI.CAT0Fillings.ae_fderiv_bump_convolution_tendsto line 78
5. lemma OAI.CAT0Fillings.norm_fderiv_bump_convolution_le line 89
6. lemma OAI.CAT0Fillings.lipschitzWith_bump_convolution line 101
7. lemma OAI.CAT0Fillings.contDiff_bump_convolution line 110
8. def OAI.CAT0Fillings.shrinkingBump line 116
9. lemma OAI.CAT0Fillings.shrinkingBump_tendsto line 123
10. lemma OAI.CAT0Fillings.exists_smooth_lipschitz_approximation line 128