OAI/Geometry/CAT0Fillings/Tangent/Kernel.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.TangentDensity.ae_blowup_inMeasure line 16
2. lemma OAI.CAT0Fillings.TangentDensity.ae_all_blowup_inMeasure line 31
3. lemma OAI.CAT0Fillings.TangentDensity.common_subsequence_three line 45
4. lemma OAI.CAT0Fillings.TangentDensity.indicator_one_eventually line 62
5. lemma OAI.CAT0Fillings.TangentDensity.lintegral_limit_le line 79
6. lemma OAI.CAT0Fillings.TangentDensity.integral_limit_le line 91
7. lemma OAI.CAT0Fillings.TangentDensity.kernel_tendsto line 119
8. def OAI.CAT0Fillings.TangentDensity.chartExtension line 129
9. lemma OAI.CAT0Fillings.TangentDensity.chartExtension_rescaled_tendsto line 133
10. lemma OAI.CAT0Fillings.TangentDensity.chart_kernel_tendsto line 150