OAI/Geometry/CAT0Fillings/Sobolev/Truncation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CAT0Fillings.positiveTrunc line 15
2. lemma OAI.CAT0Fillings.positiveTrunc_lipschitz line 17
3. lemma OAI.CAT0Fillings.positiveTrunc_nonneg line 27
4. lemma OAI.CAT0Fillings.positiveTrunc_sub_bounds line 29
5. lemma OAI.CAT0Fillings.ae_fderiv_trunc_cases line 37
6. lemma OAI.CAT0Fillings.ChartGeometry.ae_normSq_trunc_le line 81
7. lemma OAI.CAT0Fillings.ChartGeometry.energyMeasure_trunc_le line 121
8. lemma OAI.CAT0Fillings.ChartGeometry.energy_trunc_le line 133
9. lemma OAI.CAT0Fillings.continuous_memLp line 153
10. lemma OAI.CAT0Fillings.lpNorm_sq_moment line 156
11. lemma OAI.CAT0Fillings.lpNorm_two_sq line 172
12. lemma OAI.CAT0Fillings.truncation_small_support line 180
13. lemma OAI.CAT0Fillings.truncation_norm_bound line 204