OAI/Geometry/SmoothYau/DifferentialEq/TransferAcross.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.YauCounterexamples.CompactMetricAtlas.transferAcross line 20
2. lemma OAI.YauCounterexamples.CompactMetricAtlas.transferAcross_representative line 27
3. def OAI.YauCounterexamples.CompactMetricAtlas.power line 39
4. lemma OAI.YauCounterexamples.CompactMetricAtlas.power_representative line 45
5. def OAI.YauCounterexamples.CompactMetricAtlas.polynomial line 59
6. lemma OAI.YauCounterexamples.CompactMetricAtlas.polynomial_representative line 64
7. theorem OAI.YauCounterexamples.CompactMetricAtlas.semilinear_regularity_step line 72
8. theorem OAI.YauCounterexamples.CompactMetricAtlas.represented_semilinear_solution_smooth line 100