OAI/Geometry/CAT0Fillings/BV/Poincare.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CAT0Fillings.JointBV.DirectionalVariation line 16
2. lemma OAI.CAT0Fillings.JointBV.convolution_direction_bound line 21
3. lemma OAI.CAT0Fillings.JointBV.continuous_kernelIntegral line 44
4. lemma OAI.CAT0Fillings.JointBV.kernelIntegral_ball_bound line 52
5. lemma OAI.CAT0Fillings.JointBV.euclidean_opNorm_le_coordinate_bound line 90
6. lemma OAI.CAT0Fillings.JointBV.mollified_gradient_integral_bound line 108
7. lemma OAI.CAT0Fillings.JointBV.setIntegral_translate line 150
8. lemma OAI.CAT0Fillings.JointBV.affine_ball_integral_le line 159
9. def OAI.CAT0Fillings.JointBV.halfMean line 188
10. lemma OAI.CAT0Fillings.JointBV.halfMean_continuous line 192
11. lemma OAI.CAT0Fillings.JointBV.halfMean_nonneg line 199
12. lemma OAI.CAT0Fillings.JointBV.halfMean_integral_le line 202
13. lemma OAI.CAT0Fillings.JointBV.half_segment_bound line 221
14. lemma OAI.CAT0Fillings.JointBV.segment_pair_bound line 248
15. theorem OAI.CAT0Fillings.JointBV.smooth_ball_poincare line 266