Local mixed-derivative commutation for the ordinary spatial curl.

theorem Euler.ComparatorBridge.fderiv_spatial_slice {u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space} {t : ℝ} {x : EulerSmoothLimit.Space} (hu : DifferentiableAt ℝ u (t, x)) : fderiv ℝ (fun (y : EulerSmoothLimit.Space) => u (t, y)) x = fderiv ℝ u (t, x) ∘SL ContinuousLinearMap.inr ℝ ℝ EulerSmoothLimit.Space

The ordinary derivative of a spatial slice is the spatial restriction of its joint derivative.

theorem Euler.ComparatorBridge.deriv_time_slice {u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space} {t : ℝ} {x : EulerSmoothLimit.Space} (hu : DifferentiableAt ℝ u (t, x)) : deriv (fun (r : ℝ) => u (r, x)) t = (fderiv ℝ u (t, x)) (1, 0)

The ordinary derivative of a time slice is the time direction of the joint derivative.

theorem Euler.ComparatorBridge.spatial_fderiv_hasDerivAt {u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space} {t : ℝ} {x : EulerSmoothLimit.Space} (hu : ContDiffAt ℝ 2 u (t, x)) : HasDerivAt (fun (r : ℝ) => fderiv ℝ (fun (y : EulerSmoothLimit.Space) => u (r, y)) x) (fderiv ℝ (fun (y : EulerSmoothLimit.Space) => deriv (fun (r : ℝ) => u (r, y)) t) x) t

Mixed differentiation commutes using only local joint C² regularity.

theorem Euler.ComparatorBridge.time_deriv_differentiableAt {u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space} {t : ℝ} {x : EulerSmoothLimit.Space} (hu : ContDiffAt ℝ 2 u (t, x)) : DifferentiableAt ℝ (fun (y : EulerSmoothLimit.Space) => deriv (fun (r : ℝ) => u (r, y)) t) x

The derivative in time is differentiable in space under local C² regularity.

noncomputable def Euler.ComparatorBridge.curlMatrixCLM : (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) →L[ℝ] EulerSmoothLimit.Space

The continuous linear coordinate antisymmetrization defining curl.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Euler.ComparatorBridge.curlMatrixCLM_apply (A : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : curlMatrixCLM A = EulerMeanBoundary.curlMatrix A

theorem Euler.ComparatorBridge.vectorCurl_hasDerivAt {u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space} {t : ℝ} {x : EulerSmoothLimit.Space} (hu : ContDiffAt ℝ 2 u (t, x)) : HasDerivAt (fun (r : ℝ) => EulerMeanCutoffCurl.vectorCurl (fun (y : EulerSmoothLimit.Space) => u (r, y)) x) (EulerMeanCutoffCurl.vectorCurl (fun (y : EulerSmoothLimit.Space) => deriv (fun (r : ℝ) => u (r, y)) t) x) t

Spatial curl commutes with ordinary time differentiation at each point of local joint C² regularity.

theorem Euler.ComparatorBridge.joint_vectorCurl_contDiffAt {u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space} {t : ℝ} {x : EulerSmoothLimit.Space} (hu : ContDiffAt ℝ (↑⊤) u (t, x)) : ContDiffAt ℝ (↑⊤) (fun (z : ℝ × EulerSmoothLimit.Space) => EulerMeanCutoffCurl.vectorCurl (fun (y : EulerSmoothLimit.Space) => u (z.1, y)) z.2) (t, x)

Joint spatial curl retains local joint smoothness.

theorem Euler.ComparatorBridge.joint_vectorCurl_fderiv_apply {u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space} {t : ℝ} {x : EulerSmoothLimit.Space} (hu : ContDiffAt ℝ (↑⊤) u (t, x)) (a : EulerSmoothLimit.Space) : (fderiv ℝ (fun (z : ℝ × EulerSmoothLimit.Space) => EulerMeanCutoffCurl.vectorCurl (fun (y : EulerSmoothLimit.Space) => u (z.1, y)) z.2) (t, x)) (1, a) = EulerMeanCutoffCurl.vectorCurl (fun (y : EulerSmoothLimit.Space) => deriv (fun (r : ℝ) => u (r, y)) t) x + (fderiv ℝ (EulerMeanCutoffCurl.vectorCurl fun (y : EulerSmoothLimit.Space) => u (t, y)) x) a

Joint differentiation along a spacetime direction splits into the curl of the time derivative and spatial transport of the curl.

theorem Euler.ComparatorBridge.joint_spatial_fderiv_contDiffOn {u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space} {S : Set ℝ} (hu : ContDiffOn ℝ (↑⊤) u (S ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (fun (z : ℝ × EulerSmoothLimit.Space) => fderiv ℝ (fun (y : EulerSmoothLimit.Space) => u (z.1, y)) z.2) (S ×ˢ Set.univ)

Spatial differentiation preserves joint smoothness on an arbitrary time set, including its boundary. The spatial domain is the entire Euclidean space.

theorem Euler.ComparatorBridge.joint_vectorCurl_contDiffOn {u : ℝ × EulerSmoothLimit.Space → EulerSmoothLimit.Space} {S : Set ℝ} (hu : ContDiffOn ℝ (↑⊤) u (S ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (fun (z : ℝ × EulerSmoothLimit.Space) => EulerMeanCutoffCurl.vectorCurl (fun (y : EulerSmoothLimit.Space) => u (z.1, y)) z.2) (S ×ˢ Set.univ)

Spatial curl preserves joint smoothness on a time set, including its boundary, because spatial differentiation is always on the full space.