Scalar components of genuine smooth velocity and vorticity fields, their exact elliptic identity, and a fixed coordinate operator bound.

noncomputable def EulerOrdinarySobolev.componentField (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (j : Fin 3) : EulerLpTranslation.SmoothL2Field ℝ

Component field, given by mapField (EuclideanSpace.proj j) A.

Equations

• EulerOrdinarySobolev.componentField A j = EulerLpTranslation.SmoothL2Field.mapField (EuclideanSpace.proj j) A

@[simp]

theorem EulerOrdinarySobolev.componentField_apply (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (j : Fin 3) (x : EulerSmoothLimit.Space) : (componentField A j).field x = (A.field x).ofLp j

theorem EulerOrdinarySobolev.componentField_toLp_norm (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (j : Fin 3) : ‖(componentField A j).toLp‖ ≤ ‖A.toLp‖

theorem EulerOrdinarySobolev.componentField_jetLp_norm (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (j : Fin 3) (n : ℕ) : ‖(componentField A j).jetLp n‖ ≤ ‖A.jetLp n‖

theorem EulerOrdinarySobolev.componentField_partial (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (j i : Fin 3) (x : EulerSmoothLimit.Space) : EulerVectorCalculus.partialDerivative (componentField A j).field i x = ((fderiv ℝ A.field x) (axis i)).ofLp j

theorem EulerOrdinarySobolev.componentField_laplacian (A : EulerLpTranslation.SmoothL2Field EulerSmoothLimit.Space) (hdiv : ∀ (x : EulerSmoothLimit.Space), EulerSmoothLimit.divergence A.field x = 0) (j : Fin 3) (x : EulerSmoothLimit.Space) : Laplacian.laplacian (componentField A j).field x = EulerVectorCalculus.partialDerivative (componentField (vorticityField A) (j + 1)).field (j + 2) x - EulerVectorCalculus.partialDerivative (componentField (vorticityField A) (j + 2)).field (j + 1) x

theorem EulerOrdinarySobolev.operator_norm_le_of_entries (L : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (K : ℝ) (hK : 0 ≤ K) (hentries : ∀ (i j : Fin 3), ‖(L (axis i)).ofLp j‖ ≤ K) : ‖L‖ ≤ 9 * K