OAI/Geometry/CAT0Fillings/Tangent/Blowup.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.TangentDensity.tangent_kernel_mono line 12
2. def OAI.CAT0Fillings.TangentDensity.boundedCoordinate line 30
3. lemma OAI.CAT0Fillings.TangentDensity.boundedCoordinate_nonneg line 31
4. lemma OAI.CAT0Fillings.TangentDensity.boundedCoordinate_le line 33
5. lemma OAI.CAT0Fillings.TangentDensity.boundedCoordinate_eq line 36
6. lemma OAI.CAT0Fillings.TangentDensity.integrable_coordinate_truncation line 39
7. lemma OAI.CAT0Fillings.MetricDifferentiation.rescaled_distance_tendsto line 60
8. lemma OAI.CAT0Fillings.TangentDensity.integral_affine_closedBall line 95
9. lemma OAI.CAT0Fillings.TangentDensity.integral_affine_eq_average line 110
10. lemma OAI.CAT0Fillings.TangentDensity.integrable_affine line 124
11. lemma OAI.CAT0Fillings.TangentDensity.tendsto_integral_blowup line 130
12. lemma OAI.CAT0Fillings.TangentDensity.tendstoInMeasure_blowup line 140