OAI/Geometry/CAT0Fillings/Tangent/CurrentDensity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.TangentDensity.kernel_rescaled line 15
2. lemma OAI.CAT0Fillings.TangentDensity.rescaled_transform_identity line 26
3. lemma OAI.CAT0Fillings.ChordMeasure.exists_nonnegative_borel line 63
4. lemma OAI.CAT0Fillings.ChordMeasure.ae_positive_probability line 69
5. def OAI.CAT0Fillings.TangentDensity.HasTangentBound line 88
6. lemma OAI.CAT0Fillings.ChartGeometry.ae_current_tangent_density_imp line 103
7. lemma OAI.CAT0Fillings.ChartGeometry.ae_current_tangent_density line 112
8. lemma OAI.CAT0Fillings.TangentDensity.rescaled_power_eq line 132
9. lemma OAI.CAT0Fillings.TangentDensity.rescaled_spherical_limit line 144