The physical Euclidean curl #
All derivatives in this file are genuine Fréchet derivatives on the Euclidean
space used in ProblemStatement. In particular, mixed-partial symmetry is
proved from C² regularity, rather than assumed for formal derivative symbols.
The (j,i) entry of a spatial derivative.
Equations
Instances For
The usual antisymmetric part of a Jacobian, identified with a vector.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Curl of a potential on physical Euclidean three-space.
Equations
Instances For
Curl taken only in space, with the physical time held fixed.
Equations
- NavierStokes.SpatialCurl.spatialCurl A z = NavierStokes.SpatialCurl.curl (fun (y : NavierStokes.ProblemStatement.Space) => A (z.1, y)) z.2
Instances For
Actual mixed-partial symmetry, obtained from Schwarz's theorem.
Differentiating the curl is applying a fixed continuous linear map to the actual second derivative of its potential.
Divergence of curl is zero for every C² potential at the point in question.
The divergence in the actual PDE target vanishes on every C² spatial slice, including the time-zero slice when its spatial regularity is given.
One derivative of regularity is sufficient for taking the curl.
Joint spacetime smoothness is preserved, with loss of one derivative.
Relative spacetime regularity suffices even at the endpoint of a time interval, since the spatial derivative is taken on all of space.
Equality of potentials on a neighborhood gives equality of their curls.
A periodic potential gives a periodic curl; the identity also holds for the totalized derivative at points without differentiability.
Taking a curl cannot enlarge closed spatial support.
Multiplying the potential by a spatial cutoff and then taking its curl gives a genuinely divergence-free field.
A cutoff equal to one near a point preserves the original curl there.