OAI/Geometry/CAT0Fillings/Mass/Gradient.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CAT0Fillings.ChartGeometry.ae_coarea_mass_le_gradient line 19
2. lemma OAI.CAT0Fillings.densityPush_add_of_nonneg line 75
3. lemma OAI.CAT0Fillings.weighted_young_real line 93
4. lemma OAI.CAT0Fillings.densityPush_quadratic_le line 98
5. lemma OAI.CAT0Fillings.ChartGeometry.chart_gradient_quadratic_le line 128
6. lemma OAI.CAT0Fillings.ChartGeometry.gradient_quadratic_le line 140