OAI/Geometry/CAT0Fillings/Mass/IntrinsicCoarea.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.SmoothCutoff.dprofile_nonneg line 15
2. lemma OAI.CAT0Fillings.SmoothCutoff.ae_density_smul_le line 18
3. lemma OAI.CAT0Fillings.SmoothCutoff.quadratic_implies_cauchy line 30
4. lemma OAI.CAT0Fillings.SmoothCutoff.ae_density_cauchy line 47
5. lemma OAI.CAT0Fillings.ChartGeometry.ae_distribution_gradient_bounds line 82
6. theorem OAI.CAT0Fillings.ChartGeometry.ae_intrinsic_coarea line 103