OAI/Geometry/CAT0Fillings/Chord/AverageProfile.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.ChartGeometry.chord_energy line 19
2. def OAI.CAT0Fillings.Conformal.averageProfile line 73
3. def OAI.CAT0Fillings.Conformal.averageProfileDeriv line 75
4. lemma OAI.CAT0Fillings.Conformal.avg_pow_bound line 77
5. lemma OAI.CAT0Fillings.Conformal.avg_integrand_bound line 80
6. lemma OAI.CAT0Fillings.Conformal.avg_deriv_bound line 87
7. lemma OAI.CAT0Fillings.Conformal.averageProfile_hasDerivAt line 94
8. lemma OAI.CAT0Fillings.Conformal.averageProfile_contDiff line 118
9. lemma OAI.CAT0Fillings.Conformal.averageProfile_nonneg line 137