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

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Weighted divergence identity for the horizontal cutoffs in the cylinder energy calculation.

  1. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.integrable_space_function line 14
  2. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.divergence_continuous line 22
  3. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.weighted_integrable line 29
  4. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.weight_derivative_integrable line 37
  5. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.integral_weighted_divergence line 49