OAI/Geometry/CAT0Fillings/Powers/Truncated.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CAT0Fillings.ClosedCalculus.truncatedPower line 14
2. lemma OAI.CAT0Fillings.ClosedCalculus.truncatedPower_nonneg line 17
3. lemma OAI.CAT0Fillings.ClosedCalculus.truncatedPower_of_nonneg line 20
4. lemma OAI.CAT0Fillings.ClosedCalculus.truncatedPower_of_le line 24
5. lemma OAI.CAT0Fillings.ClosedCalculus.truncatedPower_of_ge line 35
6. lemma OAI.CAT0Fillings.ClosedCalculus.truncatedPower_lipschitz line 39
7. lemma OAI.CAT0Fillings.ClosedCalculus.truncatedPower_hasDerivAt_low line 76
8. lemma OAI.CAT0Fillings.ClosedCalculus.truncatedPower_hasDerivAt_high line 83
9. lemma OAI.CAT0Fillings.ClosedCalculus.truncatedPower_hasDerivAt_neg line 90
10. lemma OAI.CAT0Fillings.ClosedCalculus.truncatedPower_differentiable line 97
11. def OAI.CAT0Fillings.ClosedCalculus.truncatedPowerSlope line 115
12. lemma OAI.CAT0Fillings.ClosedCalculus.truncatedPower_deriv_smul line 117
13. lemma OAI.CAT0Fillings.ChartGeometry.truncated_deriv_ae line 139
14. lemma OAI.CAT0Fillings.ChartGeometry.closed_truncated_power line 150