OAI/Geometry/SmoothYau/Estimates/RealValueCubic.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.YauCounterexamples.BoundedAlgebra.power line 17
2. lemma OAI.YauCounterexamples.BoundedAlgebra.norm_power line 20
3. lemma OAI.YauCounterexamples.BoundedAlgebra.power_difference line 34
4. lemma OAI.YauCounterexamples.BoundedAlgebra.power_difference_small line 68
5. def OAI.YauCounterexamples.BoundedAlgebra.remainder line 86
6. def OAI.YauCounterexamples.BoundedAlgebra.remainderConstant line 90
7. lemma OAI.YauCounterexamples.BoundedAlgebra.remainder_zero line 93
8. lemma OAI.YauCounterexamples.BoundedAlgebra.remainder_lipschitz line 99
9. def OAI.YauCounterexamples.BoundedAlgebra.polynomial line 147
10. lemma OAI.YauCounterexamples.BoundedAlgebra.polynomial_zero_bound line 150
11. lemma OAI.YauCounterexamples.BoundedAlgebra.polynomial_lipschitz line 161
12. theorem OAI.YauCounterexamples.BoundedAlgebra.solve line 193
13. lemma OAI.YauCounterexamples.CompactMetricAtlas.realValue_norm_bound line 274
14. lemma OAI.YauCounterexamples.CompactMetricAtlas.realValue_power line 280
15. lemma OAI.YauCounterexamples.CompactMetricAtlas.realValue_polynomial line 293
16. theorem OAI.YauCounterexamples.CompactMetricAtlas.exists_positive_factor_of_bounds line 329
17. def OAI.YauCounterexamples.BoundedAlgebra.cubicPerturbation line 429
18. lemma OAI.YauCounterexamples.BoundedAlgebra.cubicPerturbation_bound line 432
19. lemma OAI.YauCounterexamples.CompactMetricAtlas.realValue_cubic line 497
20. lemma OAI.YauCounterexamples.CompactMetricAtlas.realDivergence_norm_bound line 506