OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Programs/PullbackMass.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

For the detector, preservation of the transported bump's mass follows directly from its transport equation and periodic integration by parts.

  1. theorem OAI.ForcedComputation.VelocityDetector.scalar_spatial_fderiv_smooth line 14
  2. theorem OAI.ForcedComputation.VelocityDetector.pullbackScalar_mass line 22