OAI/Geometry/CAT0Fillings/Density/InverseCutoff.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CAT0Fillings.inverseSquareCutoff line 14
2. lemma OAI.CAT0Fillings.inverseSquareCutoff_nonneg line 16
3. lemma OAI.CAT0Fillings.inverseSquareCutoff_le_one line 19
4. lemma OAI.CAT0Fillings.inverseSquareCutoff_eq_one line 24
5. lemma OAI.CAT0Fillings.hasDerivAt_inverse_square line 29
6. lemma OAI.CAT0Fillings.inverseSquareCutoff_lipschitz line 39
7. lemma OAI.CAT0Fillings.hasDerivAt_inverseSquareCutoff_lt line 61
8. lemma OAI.CAT0Fillings.hasDerivAt_inverseSquareCutoff_gt line 67
9. lemma OAI.CAT0Fillings.IntegerChart.fderivWithin_scalar_comp line 75
10. lemma OAI.CAT0Fillings.ChartGeometry.weighted_density_integrable_borel line 93
11. lemma OAI.CAT0Fillings.ChartGeometry.integral_massMeasure_borel line 99
12. lemma OAI.CAT0Fillings.ChartGeometry.weighted_density_summable_borel line 116
13. def OAI.CAT0Fillings.ChartGeometry.radialNormSq line 131
14. lemma OAI.CAT0Fillings.ChartGeometry.ae_radialNormSq_bounds line 135
15. lemma OAI.CAT0Fillings.ChartGeometry.aestronglyMeasurable_radialNormSq line 155