OAI/Geometry/SmoothYau/Estimates/RadialSpeedPositiveAnnulus.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.YauCounterexamples.radialSquaredBase_zero_of_norm line 22
  2. theorem OAI.YauCounterexamples.radial_periodic_second line 35
  3. def OAI.YauCounterexamples.periodicRadialOffset line 66
  4. def OAI.YauCounterexamples.periodicRadialFunction line 70
  5. def OAI.YauCounterexamples.periodicRadialSpeed line 73
  6. def OAI.YauCounterexamples.periodicAngularSecond line 77
  7. def OAI.YauCounterexamples.periodicRadialSecond line 81
  8. theorem OAI.YauCounterexamples.periodicRadialFunction_first line 85
  9. theorem OAI.YauCounterexamples.periodicRadialFunction_second line 106
  10. lemma OAI.YauCounterexamples.norm_planeRadialCovector_le line 136
  11. theorem OAI.YauCounterexamples.radial_speed_positive_annulus line 164
  12. lemma OAI.YauCounterexamples.periodicRadialOffset_eq line 190
  13. lemma OAI.YauCounterexamples.plane_norm_le_radius line 207
  14. theorem OAI.YauCounterexamples.periodicRadialSpeed_annular_lower line 216