OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Detector/CylinderLocalIntegration.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Integration of first derivatives in the horizontal directions and over one vertical period. Only C¹ regularity is needed.

  1. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.plane_integral_derivative_zero line 14
  2. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.vertical_integral_derivative_zero line 30
  3. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.atHeight_smooth line 40
  4. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.scalarSpatialD_horizontal_support line 45
  5. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.scalarSpatialD_cylinder_integrable line 57
  6. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.integral_horizontal_scalarD_zero line 68
  7. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.integral_vertical_scalarD_zero line 94