OAI/Geometry/CAT0Fillings/Calculus/Polynomial.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CAT0Fillings.ClosedCalculus.lowerCut line 12
2. def OAI.CAT0Fillings.ClosedCalculus.upperCut line 13
3. lemma OAI.CAT0Fillings.ClosedCalculus.lowerCut_pos line 14
4. lemma OAI.CAT0Fillings.ClosedCalculus.lowerCut_le_one line 15
5. lemma OAI.CAT0Fillings.ClosedCalculus.lowerCut_lt_upperCut line 19
6. lemma OAI.CAT0Fillings.ClosedCalculus.lowerCut_tendsto line 24
7. lemma OAI.CAT0Fillings.ClosedCalculus.upperCut_tendsto line 28
8. lemma OAI.CAT0Fillings.ClosedCalculus.cut_eventually line 30
9. lemma OAI.CAT0Fillings.ClosedCalculus.clamp_tendsto line 34
10. lemma OAI.CAT0Fillings.ClosedCalculus.clamp_pos line 44
11. lemma OAI.CAT0Fillings.ClosedCalculus.clamp_power_bound line 46
12. lemma OAI.CAT0Fillings.ChartGeometry.closed_positive_polynomial line 73