Ordinary smooth vector-calculus identities with the canonical Mathlib Laplacian.

noncomputable def EulerMeanVectorIdentities.vectorPartial (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (i : Fin 3) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Vector partial, given by fderiv ℝ f x (EuclideanSpace.single i 1).

Equations

• EulerMeanVectorIdentities.vectorPartial f i x = (fderiv ℝ f x) (EuclideanSpace.single i 1)

theorem EulerMeanVectorIdentities.vectorPartial_smooth (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : ContDiff ℝ (↑⊤) f) (i : Fin 3) : ContDiff ℝ (↑⊤) (vectorPartial f i)

theorem EulerMeanVectorIdentities.vectorPartial_compact (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hc : HasCompactSupport f) (i : Fin 3) : HasCompactSupport (vectorPartial f i)

theorem EulerMeanVectorIdentities.vectorPartial_apply (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : ContDiff ℝ (↑⊤) f) (i j : Fin 3) (x : EulerSmoothLimit.Space) : (vectorPartial f i x).ofLp j = EulerVectorCalculus.partialDerivative (fun (y : EulerSmoothLimit.Space) => (f y).ofLp j) i x

theorem EulerMeanVectorIdentities.vector_laplacian_coordinate (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : ContDiff ℝ (↑⊤) f) (x : EulerSmoothLimit.Space) (i : Fin 3) : (Laplacian.laplacian f x).ofLp i = Laplacian.laplacian (fun (y : EulerSmoothLimit.Space) => (f y).ofLp i) x

theorem EulerMeanVectorIdentities.vector_laplacian_eq_sum (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : ContDiff ℝ (↑⊤) f) : Laplacian.laplacian f = fun (x : EulerSmoothLimit.Space) => ∑ i : Fin 3, vectorPartial (vectorPartial f i) i x

theorem EulerMeanVectorIdentities.vector_laplacian_smooth (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (Laplacian.laplacian f)

theorem EulerMeanVectorIdentities.vector_laplacian_compact (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : ContDiff ℝ (↑⊤) f) (hc : HasCompactSupport f) : HasCompactSupport (Laplacian.laplacian f)

theorem EulerMeanVectorIdentities.vectorCurl_smooth (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (EulerMeanCutoffCurl.vectorCurl f)

theorem EulerMeanVectorIdentities.vectorCurl_support (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) : tsupport (EulerMeanCutoffCurl.vectorCurl f) ⊆ tsupport f

theorem EulerMeanVectorIdentities.vectorCurl_compact (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hc : HasCompactSupport f) : HasCompactSupport (EulerMeanCutoffCurl.vectorCurl f)

noncomputable def EulerMeanVectorIdentities.curlTest (f : EulerMeanGradientTest.Test) : EulerMeanGradientTest.Test

Curl test, given by ⟨vectorCurl (f : Space → Space), vectorCurl_smooth f f.smooth, vectorCurl_compact f f.compact⟩.

Equations

• EulerMeanVectorIdentities.curlTest f = ⟨EulerMeanCutoffCurl.vectorCurl ↑f, ⋯⟩

noncomputable def EulerMeanVectorIdentities.laplacianTest (f : EulerMeanGradientTest.Test) : EulerMeanGradientTest.Test

Laplacian test, given by ⟨Δ (f : Space → Space), vector_laplacian_smooth f f.smooth, vector_laplacian_compact f f.smooth f.compact⟩.

Equations

• EulerMeanVectorIdentities.laplacianTest f = ⟨Laplacian.laplacian ↑f, ⋯⟩

theorem EulerMeanVectorIdentities.divergence_coordinate_sum (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : ContDiff ℝ (↑⊤) f) : EulerSmoothLimit.divergence f = fun (x : EulerSmoothLimit.Space) => ∑ i : Fin 3, EulerVectorCalculus.partialDerivative (fun (y : EulerSmoothLimit.Space) => (f y).ofLp i) i x

theorem EulerMeanVectorIdentities.divergence_smooth (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : ContDiff ℝ (↑⊤) f) : ContDiff ℝ (↑⊤) (EulerSmoothLimit.divergence f)

theorem EulerMeanVectorIdentities.partialDerivative_sub (f g : EulerSmoothLimit.Space → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (i : Fin 3) (x : EulerSmoothLimit.Space) : EulerVectorCalculus.partialDerivative (fun (y : EulerSmoothLimit.Space) => f y - g y) i x = EulerVectorCalculus.partialDerivative f i x - EulerVectorCalculus.partialDerivative g i x

theorem EulerMeanVectorIdentities.vectorCurl_vectorCurl (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : ContDiff ℝ (↑⊤) f) : EulerMeanCutoffCurl.vectorCurl (EulerMeanCutoffCurl.vectorCurl f) = gradient (EulerSmoothLimit.divergence f) - Laplacian.laplacian f

The classical curl-curl identity, with genuine Fréchet derivatives and canonical Laplacian.

theorem EulerMeanVectorIdentities.divergence_compact (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : ContDiff ℝ (↑⊤) f) (hc : HasCompactSupport f) : HasCompactSupport (EulerSmoothLimit.divergence f)

theorem EulerMeanVectorIdentities.laplacian_vectorCurl (f : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hf : ContDiff ℝ (↑⊤) f) : Laplacian.laplacian (EulerMeanCutoffCurl.vectorCurl f) = EulerMeanCutoffCurl.vectorCurl (Laplacian.laplacian f)

The ordinary curl commutes with the canonical vector-valued Laplacian.