OAI/Geometry/CAT0Fillings/BV/JointPoincare.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.JointBV.scalar_convolution_comm line 15
2. def OAI.CAT0Fillings.JointBV.shrinkingBump line 22
3. lemma OAI.CAT0Fillings.JointBV.shrinkingBump_tendsto line 30
4. theorem OAI.CAT0Fillings.JointBV.ball_poincare_of_directional_variation line 35
5. def OAI.CAT0Fillings.Slicing.parameterEquiv line 86
6. lemma OAI.CAT0Fillings.Slicing.parameterEquiv_apply line 89
7. lemma OAI.CAT0Fillings.Slicing.coordinateMap_lipschitz line 93
8. def OAI.CAT0Fillings.Slicing.fullSliceControl line 101
9. instance OAI.CAT0Fillings.Slicing.fullSliceControl_finite line 106
10. lemma OAI.CAT0Fillings.Slicing.fullSlice_directional_variation line 110
11. theorem OAI.CAT0Fillings.Slicing.fullSlice_ball_poincare line 148