OAI/MathematicalPhysics/NavierStokes/VelocityDetection/CompactTails.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VelocityDetection.TailSpace.ofCompact line 15
  2. theorem OAI.VelocityDetection.TailSpace.ofCompact_apply line 21
  3. theorem OAI.VelocityDetection.TailSpace.ext_fun line 25
  4. theorem OAI.VelocityDetection.TailSpace.norm_le_of_support line 34
  5. def OAI.VelocityDetection.TailSpace.LocalHorizontalSupport line 63
  6. theorem OAI.VelocityDetection.TailSpace.LocalHorizontalSupport.slice line 67
  7. theorem OAI.VelocityDetection.TailSpace.continuous_intersection_of_support line 75
  8. theorem OAI.VelocityDetection.TailSpace.continuous_ofCompact_curve line 118
  9. theorem OAI.VelocityDetection.TailSpace.LocalHorizontalSupport.dAlong line 126
  10. theorem OAI.VelocityDetection.TailSpace.LocalHorizontalSupport.spatialD line 145
  11. theorem OAI.VelocityDetection.TailSpace.hasDerivAt_intersection line 153
  12. theorem OAI.VelocityDetection.TailSpace.c1Tails_of_smooth_support line 179
  13. theorem OAI.VelocityDetection.TailSpace.spatial_c1Tails_of_smooth_support line 199
  14. theorem OAI.VelocityDetection.TailSpace.second_continuousTails_of_smooth_support line 209