OAI/Geometry/CAT0Fillings/Powers/Slope.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.ClosedCalculus.truncatedPower_le_power line 13
2. lemma OAI.CAT0Fillings.ClosedCalculus.truncatedPower_le_linear line 23
3. lemma OAI.CAT0Fillings.ClosedCalculus.truncatedPower_product line 28
4. lemma OAI.CAT0Fillings.ClosedCalculus.truncatedPower_rhs line 36
5. lemma OAI.CAT0Fillings.ClosedCalculus.power_ratio_pos line 49
6. lemma OAI.CAT0Fillings.ClosedCalculus.power_ratio_le_one line 52
7. lemma OAI.CAT0Fillings.ClosedCalculus.truncatedPowerSlope_nonneg line 66
8. lemma OAI.CAT0Fillings.ClosedCalculus.truncatedPowerSlope_le line 73
9. lemma OAI.CAT0Fillings.ClosedCalculus.truncatedPowerSlope_ratio line 82
10. lemma OAI.CAT0Fillings.ClosedCalculus.truncatedPower_tendsto line 94
11. lemma OAI.CAT0Fillings.ClosedCalculus.truncatedPowerSlope_tendsto line 100