OAI/MathematicalPhysics/NavierStokes/VelocityDetection/TailSpaceContDiffPartialDInfty.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.VelocityDetection.TailSpace.Jets.contDiff_partialD_infty line 17
  2. theorem OAI.VelocityDetection.TailSpace.Jets.contDiff_wordPartial line 24
  3. theorem OAI.VelocityDetection.TailSpace.Jets.compactSupport_wordPartial line 30
  4. def OAI.VelocityDetection.TailSpace.Jets.ofSmoothCompact line 39
  5. theorem OAI.VelocityDetection.TailSpace.Jets.value_ofSmoothCompact line 56
  6. theorem OAI.VelocityDetection.TailSpace.Jets.entry_ofSmoothCompact line 60
  7. theorem OAI.VelocityDetection.TailSpace.Jets.contDiff_uncurry_spatialD line 66
  8. theorem OAI.VelocityDetection.TailSpace.Jets.contDiff_uncurry_wordPartial line 74
  9. theorem OAI.VelocityDetection.TailSpace.Jets.localSupport_wordPartial line 83
  10. def OAI.VelocityDetection.TailSpace.Jets.ofSupportedCurve line 90
  11. theorem OAI.VelocityDetection.TailSpace.Jets.value_ofSupportedCurve line 95
  12. theorem OAI.VelocityDetection.TailSpace.Jets.continuous_ofSupportedCurve line 99
  13. theorem OAI.VelocityDetection.TailSpace.Jets.restrict_ofSupportedCurve line 109
  14. theorem OAI.VelocityDetection.TailSpace.Jets.restrictL_apply line 129
  15. theorem OAI.VelocityDetection.TailSpace.Jets.restrict_average line 132
  16. theorem OAI.VelocityDetection.TailSpace.Jets.restrict_heat line 139
  17. theorem OAI.VelocityDetection.TailSpace.Jets.restrict_heatGradient line 143
  18. theorem OAI.VelocityDetection.TailSpace.Jets.restrict_product line 153