OAI/Geometry/IntegralFillings/Jacobian/Smoothing.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpIntegralFillings.VectorSmoothing.hasFDerivAt_convolution_lipschitz line 28
2. lemma OAI.SharpIntegralFillings.VectorSmoothing.locallyIntegrable_fderiv_lipschitz line 61
3. lemma OAI.SharpIntegralFillings.VectorSmoothing.fderiv_bump_convolution line 68
4. lemma OAI.SharpIntegralFillings.VectorSmoothing.ae_fderiv_bump_convolution_tendsto line 75
5. lemma OAI.SharpIntegralFillings.VectorSmoothing.norm_fderiv_bump_convolution_le line 86
6. lemma OAI.SharpIntegralFillings.VectorSmoothing.lipschitzWith_bump_convolution line 98
7. lemma OAI.SharpIntegralFillings.VectorSmoothing.contDiff_bump_convolution line 107
8. def OAI.SharpIntegralFillings.VectorSmoothing.shrinkingBump line 113
9. lemma OAI.SharpIntegralFillings.VectorSmoothing.shrinkingBump_tendsto line 120
10. lemma OAI.SharpIntegralFillings.VectorSmoothing.exists_smooth_lipschitz_approximation line 125