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

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The two divergence computations used for the viscous part of the localized cylinder energy identity.

  1. def OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.diffusionFlux line 15
  2. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.diffusionFlux_regular line 18
  3. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.diffusionFlux_continuous line 24
  4. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.diffusionFlux_periodic line 31
  5. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.density_gradient_pairing line 38
  6. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.diffusionFlux_divergence line 50
  7. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.diffusion_boundary_pairing line 55
  8. theorem OAI.ForcedComputation.VelocityDetector.CylinderLocalCalculus.viscosity_pairing line 97