OAI/Geometry/SmoothYau/Limits/CubicConstantNonneg.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.YauCounterexamples.cubicConstant_nonneg line 33
2. lemma OAI.YauCounterexamples.quinticConstant_nonneg line 35
3. lemma OAI.YauCounterexamples.factor_limit_algebra line 39
4. lemma OAI.YauCounterexamples.norm_le_of_sub_bound line 56
5. lemma OAI.YauCounterexamples.factor_bound_transfer line 64
6. theorem OAI.YauCounterexamples.CompactMetricAtlas.eventually_positive_factor line 82