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

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Published local energy identity, restricted to the exact cylinder and the expanding compact cutoffs used here.

F. Gancedo and A. Hidalgo-Torné, On the Cauchy problem for 3D Navier–Stokes helical vortex filament, Advances in Mathematics 471 (2025), 110268, proof of Theorem 5.6, equation (5.4), printed p.23 (arXiv:2311.15413). Only its integration-by-parts identity is retained. The helical uniqueness theorem is not used. The identity below assumes the strong classical class and does not assert uniqueness, a cutoff limit, or any detector property.

  1. def OAI.ForcedComputation.VelocityDetector.cylinderWeight line 22
  2. def OAI.ForcedComputation.VelocityDetector.cylinderDifference line 25
  3. def OAI.ForcedComputation.VelocityDetector.localizedDifferenceEnergy line 27
  4. def OAI.ForcedComputation.VelocityDetector.localizedDifferenceDissipation line 32
  5. def OAI.ForcedComputation.VelocityDetector.localizedDifferenceInteraction line 37
  6. def OAI.ForcedComputation.VelocityDetector.localizedDiffusionError line 43
  7. def OAI.ForcedComputation.VelocityDetector.localizedTransportError line 48
  8. def OAI.ForcedComputation.VelocityDetector.localizedPressureError line 54
  9. def OAI.ForcedComputation.VelocityDetector.CylinderLocalEnergyIdentity line 59