OAI/Geometry/SmoothYau/Estimates/FixedRadialChoice.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.YauCounterexamples.exists_fixed_radial_constants line 13
2. structure OAI.YauCounterexamples.FixedRadialChoice line 45
3. theorem OAI.YauCounterexamples.fixedRadialChoice_nonempty line 79
4. def OAI.YauCounterexamples.fixedRadialChoice line 100
5. def OAI.YauCounterexamples.FixedRadialChoice.fraction line 102
6. lemma OAI.YauCounterexamples.FixedRadialChoice.fraction_pos line 104
7. lemma OAI.YauCounterexamples.FixedRadialChoice.fraction_le line 108