OAI/Geometry/IntegralFillings/Optimality/BallStokes.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpIntegralFillings.Optimality.radiusFunction line 15
2. lemma OAI.SharpIntegralFillings.Optimality.radiusFunction_lipschitz line 17
3. lemma OAI.SharpIntegralFillings.Optimality.radiusFunction_boundedLip line 25
4. def OAI.SharpIntegralFillings.Optimality.radialProfile line 31
5. lemma OAI.SharpIntegralFillings.Optimality.radialProfile_contDiff line 34
6. lemma OAI.SharpIntegralFillings.Optimality.radialProfile_compact line 49
7. lemma OAI.SharpIntegralFillings.Optimality.radialProfile_zero_outside line 57
8. lemma OAI.SharpIntegralFillings.Optimality.radialProfile_fderiv_zero_outside line 63
9. lemma OAI.SharpIntegralFillings.Optimality.ballChart_param_lipschitz line 73
10. lemma OAI.SharpIntegralFillings.Optimality.ballChart_scalar_extension line 79
11. lemma OAI.SharpIntegralFillings.Optimality.ballChart_action_extensions line 86
12. lemma OAI.SharpIntegralFillings.Optimality.radialProfile_lipschitz line 103
13. lemma OAI.SharpIntegralFillings.Optimality.ballChart_local_stokes line 114