Spatial smoothness of the source vector potential, derived from its literal integral.

noncomputable def EulerPacketPiola.curlLinear : (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) →ₗ[ℝ] EulerSmoothLimit.Space

Curl linear, bundling toFun, map_add, map_smul.

Equations

• EulerPacketPiola.curlLinear = { toFun := EulerMeanBoundary.curlMatrix, map_add' := EulerMeanBoundary.curlMatrix_add, map_smul' := EulerMeanBoundary.curlMatrix_smul }

noncomputable def EulerPacketPiola.curlOperator : (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) →L[ℝ] EulerSmoothLimit.Space

Curl operator, given by curlLinear.toContinuousLinearMap.

Equations

• EulerPacketPiola.curlOperator = LinearMap.toContinuousLinearMap EulerPacketPiola.curlLinear

@[simp]

theorem EulerPacketPiola.curlOperator_apply (A : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : curlOperator A = EulerMeanBoundary.curlMatrix A

theorem EulerPacketPiola.coveringPotential_contDiff (P : ℝ) (hP : 0 ≤ P) (m : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (A : EulerLiftedGradientSpace.LiftTangent → EulerSmoothLimit.Space) (hm : ContDiff ℝ (↑⊤) m) (hnz : ∀ (y : EulerSmoothLimit.Space), m y ≠ 0) (hA : ContDiff ℝ (↑⊤) A) : ContDiff ℝ (↑⊤) (coveringPotential P m A)

theorem EulerPacketPiola.coveringSlowCurl_contDiff (P : ℝ) (hP : 0 ≤ P) (m : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (A : EulerLiftedGradientSpace.LiftTangent → EulerSmoothLimit.Space) (G : EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hm : ContDiff ℝ (↑⊤) m) (hnz : ∀ (y : EulerSmoothLimit.Space), m y ≠ 0) (hA : ContDiff ℝ (↑⊤) A) (hG : ContDiff ℝ (↑⊤) G) : ContDiff ℝ ↑⊤ fun (z : EulerLiftedGradientSpace.LiftTangent) => coveringSlowCurl (G z.1) (coveringPotential P m A) z

The curl is the actual first spatial derivative of the constructed potential.

theorem EulerPacketPiola.smooth_coveringPotential_pair_piola (P κ : ℝ) (hP : 0 ≤ P) (m₀ : EulerSmoothLimit.Space) (Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (A : EulerLiftedGradientSpace.LiftTangent → EulerSmoothLimit.Space) (hΞ : ContDiff ℝ 2 Ξ) (F : EulerSmoothLimit.Space → EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (hNormal : ContDiff ℝ ↑⊤ fun (y : EulerSmoothLimit.Space) => (ContinuousLinearMap.adjoint ↑(F y).symm) m₀) (hm : ∀ (y : EulerSmoothLimit.Space), (ContinuousLinearMap.adjoint ↑(F y).symm) m₀ ≠ 0) (hA : ContDiff ℝ (↑⊤) A) (z : EulerLiftedGradientSpace.LiftTangent) (hF : fderiv ℝ Ξ z.1 = ↑(F z.1)) (hdet : Matrix.det (operatorMatrix ↑(F z.1)) = 1) (htan : inner ℝ ((ContinuousLinearMap.adjoint ↑(F z.1).symm) m₀) (A z) = 0) : (F z.1).symm (A z + κ • coveringSlowCurl (↑(F z.1).symm) (coveringPotential P (fun (y : EulerSmoothLimit.Space) => (ContinuousLinearMap.adjoint ↑(F y).symm) m₀) A) z) = coveringCurl κ m₀ (coveringPullbackCovector Ξ (coveringPotential P (fun (y : EulerSmoothLimit.Space) => (ContinuousLinearMap.adjoint ↑(F y).symm) m₀) A)) z

The Piola identity now needs regularity only for the input fields, not for Q.