OAI/Geometry/CAT0Fillings/Compactness/BV.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.JointBV.scalar_precompR line 12
2. lemma OAI.CAT0Fillings.JointBV.convolution_bump_deriv_norm_integrable line 17
3. lemma OAI.CAT0Fillings.JointBV.convolution_bump_hasFDerivAt line 41
4. lemma OAI.CAT0Fillings.JointBV.convolution_bump_deriv_continuous line 47
5. lemma OAI.CAT0Fillings.JointBV.convolution_bump_integrable line 54
6. lemma OAI.CAT0Fillings.JointBV.mollified_gradient_total_bound line 59
7. theorem OAI.CAT0Fillings.JointBV.translation_integral_bound line 73
8. lemma OAI.CAT0Fillings.JointBV.DirectionalVariation.congr line 114
9. theorem OAI.CAT0Fillings.JointBV.totallyBounded_L1_of_directional_variation line 125