The exact fast/slow splitting of the packet curl. The angular term is the ordinary cross product with F⁻ᵀ m₀; the angular primitive then produces the literal pair A + κ C. Its weighted pullback is realized in the actual lifted divergence-free L² space.

The curl Piola identity on the actual periodic cylinder. The Jacobian acts only on the three label variables. Its derivative cancels in the lifted curl by symmetry of the genuine second derivative; the angular component passes through unchanged. This supplies an actual element of the closed lifted divergence-free L² space from a compact smooth packet potential.

Curl in the constant lifted directions (κ eᵢ, m₀ᵢ) on the actual periodic cylinder. Mixed covering derivatives commute, so its lifted divergence vanishes. Compact smooth potentials also produce members of the existing closed divergence-free Bochner L² space.

theorem EulerPacketPiola.liftedDirection_coordinate (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (i : Fin 3) : (EulerGraphPullback.liftedDirection κ m) (EuclideanSpace.single i 1) = EulerMetricTransport.coordinateDirection κ m i

noncomputable def EulerPacketPiola.liftedCurl (period κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (Q : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerLiftedGradientSpace.Vector3

Lifted curl, given by curlMatrix ((fieldFDeriv period Q x).comp (EulerGraphPullback.liftedDirection κ m)).

Equations

• EulerPacketPiola.liftedCurl period κ m Q x = EulerMeanBoundary.curlMatrix (EulerLiftedWeakDerivative.fieldFDeriv period Q x ∘SL EulerGraphPullback.liftedDirection κ m)

theorem EulerPacketPiola.liftedCurl_component (period κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (Q : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (x : EulerLiftedGradientSpace.LiftDomain period) (i : Fin 3) : (liftedCurl period κ m Q x).ofLp i = (EulerTransportDerivatives.fieldDerivative period (EulerMetricTransport.coordinateDirection κ m (i + 1)) Q x).ofLp (i + 2) - (EulerTransportDerivatives.fieldDerivative period (EulerMetricTransport.coordinateDirection κ m (i + 2)) Q x).ofLp (i + 1)

theorem EulerPacketPiola.component_smooth (period : ℝ) (Q : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hQ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period Q x)) (i : Fin 3) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (fun (y : EulerLiftedGradientSpace.LiftDomain period) => (Q y).ofLp i) x)

theorem EulerPacketPiola.liftedCurl_component_scalar (period κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (Q : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hQ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period Q x)) (x : EulerLiftedGradientSpace.LiftDomain period) (i : Fin 3) : (liftedCurl period κ m Q x).ofLp i = EulerTransportDerivatives.fieldDerivative period (EulerMetricTransport.coordinateDirection κ m (i + 1)) (fun (y : EulerLiftedGradientSpace.LiftDomain period) => (Q y).ofLp (i + 2)) x - EulerTransportDerivatives.fieldDerivative period (EulerMetricTransport.coordinateDirection κ m (i + 2)) (fun (y : EulerLiftedGradientSpace.LiftDomain period) => (Q y).ofLp (i + 1)) x

theorem EulerPacketPiola.liftedCurl_eq_tests (period κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (Q : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hQ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period Q x)) : liftedCurl period κ m Q = fun (x : EulerLiftedGradientSpace.LiftDomain period) => EulerLiftedCurl.curlTest period κ m 0 1 (fun (y : EulerLiftedGradientSpace.LiftDomain period) => (Q y).ofLp 2) x + EulerLiftedCurl.curlTest period κ m 1 2 (fun (y : EulerLiftedGradientSpace.LiftDomain period) => (Q y).ofLp 0) x + EulerLiftedCurl.curlTest period κ m 2 0 (fun (y : EulerLiftedGradientSpace.LiftDomain period) => (Q y).ofLp 1) x

The full lifted curl is a finite sum of the existing antisymmetric scalar curl tests.

theorem EulerPacketPiola.liftedCurl_smooth (period κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (Q : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hQ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period Q x)) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (liftedCurl period κ m Q) x)

theorem EulerPacketPiola.scalar_fieldDerivative_sub (period : ℝ) (a : EulerLiftedGradientSpace.LiftTangent) (f g : EulerLiftedGradientSpace.LiftDomain period → ℝ) (hf : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period f x)) (hg : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period g x)) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerTransportDerivatives.fieldDerivative period a (fun (y : EulerLiftedGradientSpace.LiftDomain period) => f y - g y) x = EulerTransportDerivatives.fieldDerivative period a f x - EulerTransportDerivatives.fieldDerivative period a g x

theorem EulerPacketPiola.fieldDerivative_liftedCurl_component (period κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (Q : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hQ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period Q x)) (a : EulerLiftedGradientSpace.LiftTangent) (x : EulerLiftedGradientSpace.LiftDomain period) (i : Fin 3) : (EulerTransportDerivatives.fieldDerivative period a (liftedCurl period κ m Q) x).ofLp i = EulerTransportDerivatives.fieldDerivative period a (EulerTransportDerivatives.fieldDerivative period (EulerMetricTransport.coordinateDirection κ m (i + 1)) fun (y : EulerLiftedGradientSpace.LiftDomain period) => (Q y).ofLp (i + 2)) x - EulerTransportDerivatives.fieldDerivative period a (EulerTransportDerivatives.fieldDerivative period (EulerMetricTransport.coordinateDirection κ m (i + 2)) fun (y : EulerLiftedGradientSpace.LiftDomain period) => (Q y).ofLp (i + 1)) x

theorem EulerPacketPiola.lifted_divergence_curl (period κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (Q : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hQ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period Q x)) (x : EulerLiftedGradientSpace.LiftDomain period) : ∑ i : Fin 3, (EulerTransportDerivatives.fieldDerivative period (EulerMetricTransport.coordinateDirection κ m i) (liftedCurl period κ m Q) x).ofLp i = 0

The constant lifted divergence of an actual lifted curl vanishes pointwise.

theorem EulerPacketPiola.component_compact (period : ℝ) (Q : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hQ : HasCompactSupport Q) (i : Fin 3) : HasCompactSupport fun (x : EulerLiftedGradientSpace.LiftDomain period) => (Q x).ofLp i

noncomputable def EulerPacketPiola.liftedCurlLp (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (Q : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hc : HasCompactSupport Q) (hQ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period Q x)) : ↥(EulerLiftedGradientSpace.LiftL2 period)

Lifted curl Lᵖ, constructed using curlTestLp.

Equations

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

theorem EulerPacketPiola.liftedCurlLp_ae (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (Q : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hc : HasCompactSupport Q) (hQ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period Q x)) : ↑↑(liftedCurlLp period κ m Q hc hQ) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] liftedCurl period κ m Q

theorem EulerPacketPiola.liftedCurlLp_mem (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerLiftedGradientSpace.Vector3) (Q : EulerLiftedGradientSpace.LiftDomain period → EulerLiftedGradientSpace.Vector3) (hc : HasCompactSupport Q) (hQ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period Q x)) : liftedCurlLp period κ m Q hc hQ ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m

Compact lifted curls belong to the actual closed constraint space used by the correction.

The actual curl Piola identity for a determinant-one coordinate map. The derivative of the Jacobian cancels by symmetry of the genuine second Fréchet derivative. No curl identity or commutation relation is assumed.

@[instance_reducible]

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

Cache the standard NormedAddCommGroup (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerPacketPiola.instPacketPiola1 = inferInstance

@[instance_reducible]

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

Cache the standard NormedSpace ℝ (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerPacketPiola.instPacketPiola2 = inferInstance

theorem EulerPacketPiola.adjoint_apply_coordinate (A : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (q : EulerSmoothLimit.Space) (i : Fin 3) : ((ContinuousLinearMap.adjoint A) q).ofLp i = inner ℝ (A (EuclideanSpace.single i 1)) q

noncomputable def EulerPacketPiola.pullbackCovector (Ξ Q : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Pull back a Euclidean covector field by the actual derivative of the coordinate map.

Equations

• EulerPacketPiola.pullbackCovector Ξ Q x = (ContinuousLinearMap.adjoint (fderiv ℝ Ξ x)) (Q x)

theorem EulerPacketPiola.curl_pullbackCovector (Ξ Q : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hΞ : ContDiff ℝ 2 Ξ) (x : EulerSmoothLimit.Space) (hQ : DifferentiableAt ℝ Q x) : EulerMeanCutoffCurl.vectorCurl (pullbackCovector Ξ Q) x = EulerMeanBoundary.curlMatrix (ContinuousLinearMap.adjoint (fderiv ℝ Ξ x) ∘SL fderiv ℝ Q x)

Symmetric second derivatives remove the entire derivative-of-Jacobian term from curl.

noncomputable def EulerPacketPiola.transformedCurl (F : EulerSmoothLimit.Space → EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (Q : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

The source's slow transformed curl d × Q, with d=F⁻ᵀ ∇.

Equations

• EulerPacketPiola.transformedCurl F Q x = EulerMeanBoundary.curlMatrix (fderiv ℝ Q x ∘SL ↑(F x).symm)

theorem EulerPacketPiola.piola_curl (Ξ Q : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hΞ : ContDiff ℝ 2 Ξ) (F : EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) (hF : fderiv ℝ Ξ x = ↑F) (hdet : Matrix.det (operatorMatrix ↑F) = 1) (hQ : DifferentiableAt ℝ Q x) : F.symm (EulerMeanBoundary.curlMatrix (fderiv ℝ Q x ∘SL ↑F.symm)) = EulerMeanCutoffCurl.vectorCurl (pullbackCovector Ξ Q) x

For the actual Jacobian and unit determinant, F⁻¹(d×Q)=curl(FᵀQ).

theorem EulerPacketPiola.pullbackCovector_smooth (Ξ Q : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hΞ : ContDiff ℝ (↑⊤) Ξ) (hQ : ContDiff ℝ (↑⊤) Q) : ContDiff ℝ (↑⊤) (pullbackCovector Ξ Q)

theorem EulerPacketPiola.divergence_piola_curl (Ξ Q : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hΞ : ContDiff ℝ (↑⊤) Ξ) (hQ : ContDiff ℝ (↑⊤) Q) (F : EulerSmoothLimit.Space → EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (hF : ∀ (x : EulerSmoothLimit.Space), fderiv ℝ Ξ x = ↑(F x)) (hdet : ∀ (x : EulerSmoothLimit.Space), Matrix.det (operatorMatrix ↑(F x)) = 1) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.divergence (fun (y : EulerSmoothLimit.Space) => (F y).symm (transformedCurl F Q y)) x = 0

The transformed curl produces an actually divergence-free label velocity.

@[instance_reducible]

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

Cache the standard NormedAddCommGroup (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerPacketPiola.instPacketLiftedPiola1 = inferInstance

@[instance_reducible]

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

Cache the standard NormedSpace ℝ (Space →L[ℝ] Space) instance to shorten typeclass synthesis.

Equations

• EulerPacketPiola.instPacketLiftedPiola2 = inferInstance

theorem EulerPacketPiola.realAdjoint_apply (A : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : EulerTransverseGramInverse.realAdjoint A = ContinuousLinearMap.adjoint A

noncomputable def EulerPacketPiola.coveringCurl (κ : ℝ) (m : EulerSmoothLimit.Space) (q : EulerLiftedGradientSpace.LiftTangent → EulerSmoothLimit.Space) (z : EulerLiftedGradientSpace.LiftTangent) : EulerSmoothLimit.Space

Covering curl, given by curlMatrix ((fderiv ℝ q z).comp (EulerGraphPullback.liftedDirection κ m)).

Equations

• EulerPacketPiola.coveringCurl κ m q z = EulerMeanBoundary.curlMatrix (fderiv ℝ q z ∘SL EulerGraphPullback.liftedDirection κ m)

noncomputable def EulerPacketPiola.coveringPullbackCovector (Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (q : EulerLiftedGradientSpace.LiftTangent → EulerSmoothLimit.Space) (z : EulerLiftedGradientSpace.LiftTangent) : EulerSmoothLimit.Space

Covering pullback covector, given by (fderiv ℝ Ξ z.1).adjoint (q z).

Equations

• EulerPacketPiola.coveringPullbackCovector Ξ q z = (ContinuousLinearMap.adjoint (fderiv ℝ Ξ z.1)) (q z)

theorem EulerPacketPiola.coveringCurl_pullback (κ : ℝ) (m : EulerSmoothLimit.Space) (Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (q : EulerLiftedGradientSpace.LiftTangent → EulerSmoothLimit.Space) (hΞ : ContDiff ℝ 2 Ξ) (z : EulerLiftedGradientSpace.LiftTangent) (hq : DifferentiableAt ℝ q z) : coveringCurl κ m (coveringPullbackCovector Ξ q) z = EulerMeanBoundary.curlMatrix (ContinuousLinearMap.adjoint (fderiv ℝ Ξ z.1) ∘SL fderiv ℝ q z ∘SL EulerGraphPullback.liftedDirection κ m)

Cancellation of the actual Hessian in all constant lifted directions.

theorem EulerPacketPiola.covering_piola_curl (κ : ℝ) (m : EulerSmoothLimit.Space) (Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (q : EulerLiftedGradientSpace.LiftTangent → EulerSmoothLimit.Space) (hΞ : ContDiff ℝ 2 Ξ) (z : EulerLiftedGradientSpace.LiftTangent) (F : EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (hF : fderiv ℝ Ξ z.1 = ↑F) (hdet : Matrix.det (operatorMatrix ↑F) = 1) (hq : DifferentiableAt ℝ q z) : F.symm (EulerMeanBoundary.curlMatrix (fderiv ℝ q z ∘SL EulerGraphPullback.liftedDirection κ m ∘SL ↑F.symm)) = coveringCurl κ m (coveringPullbackCovector Ξ q) z

Unit determinant transforms the full slow-plus-angular curl by the inverse Jacobian.

noncomputable def EulerPacketPiola.liftedPullbackCovector (period : ℝ) (Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (Q : EulerLiftedGradientSpace.LiftDomain period → EulerSmoothLimit.Space) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerSmoothLimit.Space

Lifted pullback covector, given by (fderiv ℝ Ξ x.1).adjoint (Q x).

Equations

• EulerPacketPiola.liftedPullbackCovector period Ξ Q x = (ContinuousLinearMap.adjoint (fderiv ℝ Ξ x.1)) (Q x)

noncomputable def EulerPacketPiola.transformedLiftedCurl (period κ : ℝ) (m : EulerSmoothLimit.Space) (F : EulerSmoothLimit.Space → EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (Q : EulerLiftedGradientSpace.LiftDomain period → EulerSmoothLimit.Space) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerSmoothLimit.Space

Transformed lifted curl, given by curlMatrix ((fieldFDeriv period Q x).comp ((EulerGraphPullback.liftedDirection κ m).comp (F x.1).symm.toContinuousLinearMap)).

Equations

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

theorem EulerPacketPiola.localFieldLift_pullbackCovector (period : ℝ) (Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (Q : EulerLiftedGradientSpace.LiftDomain period → EulerSmoothLimit.Space) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerMetricTransport.localFieldLift period (liftedPullbackCovector period Ξ Q) x = coveringPullbackCovector (fun (y : EulerSmoothLimit.Space) => Ξ (x.1 + y)) (EulerMetricTransport.localFieldLift period Q x)

The actual local chart of the pulled-back potential.

theorem EulerPacketPiola.lifted_piola_curl (period κ : ℝ) (m : EulerSmoothLimit.Space) (Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (Q : EulerLiftedGradientSpace.LiftDomain period → EulerSmoothLimit.Space) (hΞ : ContDiff ℝ 2 Ξ) (F : EulerSmoothLimit.Space → EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (hF : ∀ (y : EulerSmoothLimit.Space), fderiv ℝ Ξ y = ↑(F y)) (hdet : ∀ (y : EulerSmoothLimit.Space), Matrix.det (operatorMatrix ↑(F y)) = 1) (hQ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period Q x)) (x : EulerLiftedGradientSpace.LiftDomain period) : (F x.1).symm (transformedLiftedCurl period κ m F Q x) = liftedCurl period κ m (liftedPullbackCovector period Ξ Q) x

The Piola curl identity for the periodic packet, with the actual scaled lifted directions.

theorem EulerPacketPiola.liftedPullbackCovector_smooth (period : ℝ) (Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (Q : EulerLiftedGradientSpace.LiftDomain period → EulerSmoothLimit.Space) (hΞ : ContDiff ℝ (↑⊤) Ξ) (hQ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period Q x)) (x : EulerLiftedGradientSpace.LiftDomain period) : ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period (liftedPullbackCovector period Ξ Q) x)

theorem EulerPacketPiola.liftedPullbackCovector_compact (period : ℝ) (Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (Q : EulerLiftedGradientSpace.LiftDomain period → EulerSmoothLimit.Space) (hc : HasCompactSupport Q) : HasCompactSupport (liftedPullbackCovector period Ξ Q)

theorem EulerPacketPiola.lifted_divergence_piola_curl (period κ : ℝ) (m : EulerSmoothLimit.Space) (Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (Q : EulerLiftedGradientSpace.LiftDomain period → EulerSmoothLimit.Space) (hΞ : ContDiff ℝ (↑⊤) Ξ) (F : EulerSmoothLimit.Space → EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (hF : ∀ (y : EulerSmoothLimit.Space), fderiv ℝ Ξ y = ↑(F y)) (hdet : ∀ (y : EulerSmoothLimit.Space), Matrix.det (operatorMatrix ↑(F y)) = 1) (hQ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period Q x)) (x : EulerLiftedGradientSpace.LiftDomain period) : ∑ i : Fin 3, (EulerTransportDerivatives.fieldDerivative period (EulerMetricTransport.coordinateDirection κ m i) (fun (y : EulerLiftedGradientSpace.LiftDomain period) => (F y.1).symm (transformedLiftedCurl period κ m F Q y)) x).ofLp i = 0

Actual pointwise lifted divergence vanishes for the transformed packet curl.

noncomputable def EulerPacketPiola.piolaLiftedCurlLp (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerSmoothLimit.Space) (Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (Q : EulerLiftedGradientSpace.LiftDomain period → EulerSmoothLimit.Space) (hΞ : ContDiff ℝ (↑⊤) Ξ) (hc : HasCompactSupport Q) (hQ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period Q x)) : ↥(EulerLiftedGradientSpace.LiftL2 period)

A genuine Bochner L² realization of the pulled-back packet curl.

Equations

• EulerPacketPiola.piolaLiftedCurlLp period κ m Ξ Q hΞ hc hQ = EulerPacketPiola.liftedCurlLp period κ m (EulerPacketPiola.liftedPullbackCovector period Ξ Q) ⋯ ⋯

theorem EulerPacketPiola.piolaLiftedCurlLp_ae (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerSmoothLimit.Space) (Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (Q : EulerLiftedGradientSpace.LiftDomain period → EulerSmoothLimit.Space) (hΞ : ContDiff ℝ (↑⊤) Ξ) (hc : HasCompactSupport Q) (hQ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period Q x)) (F : EulerSmoothLimit.Space → EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (hF : ∀ (y : EulerSmoothLimit.Space), fderiv ℝ Ξ y = ↑(F y)) (hdet : ∀ (y : EulerSmoothLimit.Space), Matrix.det (operatorMatrix ↑(F y)) = 1) : ↑↑(piolaLiftedCurlLp period κ m Ξ Q hΞ hc hQ) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] fun (x : EulerLiftedGradientSpace.LiftDomain period) => (F x.1).symm (transformedLiftedCurl period κ m F Q x)

theorem EulerPacketPiola.piolaLiftedCurlLp_mem (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m : EulerSmoothLimit.Space) (Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (Q : EulerLiftedGradientSpace.LiftDomain period → EulerSmoothLimit.Space) (hΞ : ContDiff ℝ (↑⊤) Ξ) (hc : HasCompactSupport Q) (hQ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period Q x)) : piolaLiftedCurlLp period κ m Ξ Q hΞ hc hQ ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m

The pulled-back packet satisfies the exact closed constraint used by correction assembly.

theorem EulerPacketPiola.curlMatrix_rankOne (a b : EulerSmoothLimit.Space) : EulerMeanBoundary.curlMatrix (((InnerProductSpace.rankOne ℝ) a) b) = EulerPacketCrossProduct.cross b a

theorem EulerPacketPiola.curl_lifted_split (κ : ℝ) (m : EulerSmoothLimit.Space) (L : EulerLiftedGradientSpace.LiftTangent →L[ℝ] EulerSmoothLimit.Space) (G : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : EulerMeanBoundary.curlMatrix (L ∘SL EulerGraphPullback.liftedDirection κ m ∘SL G) = κ • EulerMeanBoundary.curlMatrix (L ∘SL ContinuousLinearMap.inl ℝ EulerSmoothLimit.Space ℝ ∘SL G) + EulerPacketCrossProduct.cross ((ContinuousLinearMap.adjoint G) m) (L (0, 1))

The actual four-dimensional derivative splits into its slow and angular parts.

noncomputable def EulerPacketPiola.coveringSlowCurl (G : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (q : EulerLiftedGradientSpace.LiftTangent → EulerSmoothLimit.Space) (z : EulerLiftedGradientSpace.LiftTangent) : EulerSmoothLimit.Space

Covering slow curl, given by curlMatrix ((fderiv ℝ q z).comp ((ContinuousLinearMap.inl ℝ Space ℝ).comp G)).

Equations

• EulerPacketPiola.coveringSlowCurl G q z = EulerMeanBoundary.curlMatrix (fderiv ℝ q z ∘SL ContinuousLinearMap.inl ℝ EulerSmoothLimit.Space ℝ ∘SL G)

noncomputable def EulerPacketPiola.coveringPotential (P : ℝ) (m : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (A : EulerLiftedGradientSpace.LiftTangent → EulerSmoothLimit.Space) (z : EulerLiftedGradientSpace.LiftTangent) : EulerSmoothLimit.Space

The same angular primitive as in the source, at each ordinary label.

Equations

• EulerPacketPiola.coveringPotential P m A z = EulerPacketAngularPotential.potential P (m z.1) (fun (θ : ℝ) => A (z.1, θ)) z.2

theorem EulerPacketPiola.coveringPotential_angle_derivative (P : ℝ) (m : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (A : EulerLiftedGradientSpace.LiftTangent → EulerSmoothLimit.Space) (z : EulerLiftedGradientSpace.LiftTangent) (hA : Continuous fun (θ : ℝ) => A (z.1, θ)) (hq : DifferentiableAt ℝ (coveringPotential P m A) z) : (fderiv ℝ (coveringPotential P m A) z) (0, 1) = (EulerPacketCrossProduct.potentialMultiplier (m z.1)) (A z)

The derivative in the angle direction is proved from the actual primitive.

theorem EulerPacketPiola.coveringPotential_pair_piola (P κ : ℝ) (m₀ : EulerSmoothLimit.Space) (Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (A : EulerLiftedGradientSpace.LiftTangent → EulerSmoothLimit.Space) (hΞ : ContDiff ℝ 2 Ξ) (F : EulerSmoothLimit.Space → EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (z : EulerLiftedGradientSpace.LiftTangent) (hF : fderiv ℝ Ξ z.1 = ↑(F z.1)) (hdet : Matrix.det (operatorMatrix ↑(F z.1)) = 1) (hm : (ContinuousLinearMap.adjoint ↑(F z.1).symm) m₀ ≠ 0) (htan : inner ℝ ((ContinuousLinearMap.adjoint ↑(F z.1).symm) m₀) (A z) = 0) (hA : Continuous fun (θ : ℝ) => A (z.1, θ)) (hq : DifferentiableAt ℝ (coveringPotential P (fun (y : EulerSmoothLimit.Space) => (ContinuousLinearMap.adjoint ↑(F y).symm) m₀) A) z) : (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

A literal source pair is a Piola curl for the actual constructed angular primitive.

noncomputable def EulerPacketPiola.liftedSlowCurl (period : ℝ) (F : EulerSmoothLimit.Space → EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (Q : EulerLiftedGradientSpace.LiftDomain period → EulerSmoothLimit.Space) (x : EulerLiftedGradientSpace.LiftDomain period) : EulerSmoothLimit.Space

Lifted slow curl, given by curlMatrix ((fieldFDeriv period Q x).comp ((ContinuousLinearMap.inl ℝ Space ℝ).comp (F x.1).symm.toContinuousLinearMap)).

Equations

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

theorem EulerPacketPiola.transformedLiftedCurl_split (period κ : ℝ) (m₀ : EulerSmoothLimit.Space) (F : EulerSmoothLimit.Space → EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (Q : EulerLiftedGradientSpace.LiftDomain period → EulerSmoothLimit.Space) (x : EulerLiftedGradientSpace.LiftDomain period) : transformedLiftedCurl period κ m₀ F Q x = κ • liftedSlowCurl period F Q x + EulerPacketCrossProduct.cross ((ContinuousLinearMap.adjoint ↑(F x.1).symm) m₀) (EulerTransportDerivatives.fieldDerivative period (0, 1) Q x)

theorem EulerPacketPiola.lifted_pair_piola (period κ : ℝ) (m₀ : EulerSmoothLimit.Space) (Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (A Q : EulerLiftedGradientSpace.LiftDomain period → EulerSmoothLimit.Space) (hΞ : ContDiff ℝ 2 Ξ) (F : EulerSmoothLimit.Space → EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (hF : ∀ (y : EulerSmoothLimit.Space), fderiv ℝ Ξ y = ↑(F y)) (hdet : ∀ (y : EulerSmoothLimit.Space), Matrix.det (operatorMatrix ↑(F y)) = 1) (hQ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period Q x)) (x : EulerLiftedGradientSpace.LiftDomain period) (hm : (ContinuousLinearMap.adjoint ↑(F x.1).symm) m₀ ≠ 0) (htan : inner ℝ ((ContinuousLinearMap.adjoint ↑(F x.1).symm) m₀) (A x) = 0) (hangle : EulerTransportDerivatives.fieldDerivative period (0, 1) Q x = (EulerPacketCrossProduct.potentialMultiplier ((ContinuousLinearMap.adjoint ↑(F x.1).symm) m₀)) (A x)) : (F x.1).symm (A x + κ • liftedSlowCurl period F Q x) = liftedCurl period κ m₀ (liftedPullbackCovector period Ξ Q) x

Only the actual angular derivative formula for Q is needed to identify the source pair.

theorem EulerPacketPiola.weighted_lifted_pair_piola (period κ : ℝ) (m₀ : EulerSmoothLimit.Space) (Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (A Q : EulerLiftedGradientSpace.LiftDomain period → EulerSmoothLimit.Space) (hΞ : ContDiff ℝ 2 Ξ) (F : EulerSmoothLimit.Space → EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (hF : ∀ (y : EulerSmoothLimit.Space), fderiv ℝ Ξ y = ↑(F y)) (hdet : ∀ (y : EulerSmoothLimit.Space), Matrix.det (operatorMatrix ↑(F y)) = 1) (hQ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period Q x)) (x : EulerLiftedGradientSpace.LiftDomain period) (hm : (ContinuousLinearMap.adjoint ↑(F x.1).symm) m₀ ≠ 0) (htan : inner ℝ ((ContinuousLinearMap.adjoint ↑(F x.1).symm) m₀) (A x) = 0) (hangle : EulerTransportDerivatives.fieldDerivative period (0, 1) Q x = (EulerPacketCrossProduct.potentialMultiplier ((ContinuousLinearMap.adjoint ↑(F x.1).symm) m₀)) (A x)) (p : ℕ) : (F x.1).symm (κ ^ p • A x + κ ^ (p + 1) • liftedSlowCurl period F Q x) = κ ^ p • liftedCurl period κ m₀ (liftedPullbackCovector period Ξ Q) x

The exact powers in source (13), without discarding the terminal corrector.

noncomputable def EulerPacketPiola.piolaPairLp (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m₀ : EulerSmoothLimit.Space) (Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (Q : EulerLiftedGradientSpace.LiftDomain period → EulerSmoothLimit.Space) (hΞ : ContDiff ℝ (↑⊤) Ξ) (hc : HasCompactSupport Q) (hQ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period Q x)) (p : ℕ) : ↥(EulerLiftedGradientSpace.LiftL2 period)

Piola pair Lᵖ, given by κ ^ p • piolaLiftedCurlLp period κ m₀ Ξ Q hΞ hc hQ.

Equations

• EulerPacketPiola.piolaPairLp period κ m₀ Ξ Q hΞ hc hQ p = κ ^ p • EulerPacketPiola.piolaLiftedCurlLp period κ m₀ Ξ Q hΞ hc hQ

theorem EulerPacketPiola.piolaPairLp_mem (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m₀ : EulerSmoothLimit.Space) (Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (Q : EulerLiftedGradientSpace.LiftDomain period → EulerSmoothLimit.Space) (hΞ : ContDiff ℝ (↑⊤) Ξ) (hc : HasCompactSupport Q) (hQ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period Q x)) (p : ℕ) : piolaPairLp period κ m₀ Ξ Q hΞ hc hQ p ∈ EulerLiftedGradientSpace.divergenceFreeSpace period κ m₀

theorem EulerPacketPiola.piolaPairLp_ae (period : ℝ) [Fact (0 < period)] (κ : ℝ) (m₀ : EulerSmoothLimit.Space) (Ξ : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (A Q : EulerLiftedGradientSpace.LiftDomain period → EulerSmoothLimit.Space) (hΞ : ContDiff ℝ (↑⊤) Ξ) (hc : HasCompactSupport Q) (hQ : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), ContDiff ℝ (↑⊤) (EulerMetricTransport.localFieldLift period Q x)) (F : EulerSmoothLimit.Space → EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (hF : ∀ (y : EulerSmoothLimit.Space), fderiv ℝ Ξ y = ↑(F y)) (hdet : ∀ (y : EulerSmoothLimit.Space), Matrix.det (operatorMatrix ↑(F y)) = 1) (hm : ∀ (x : EulerSmoothLimit.Space), (ContinuousLinearMap.adjoint ↑(F x).symm) m₀ ≠ 0) (htan : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), inner ℝ ((ContinuousLinearMap.adjoint ↑(F x.1).symm) m₀) (A x) = 0) (hangle : ∀ (x : EulerLiftedGradientSpace.LiftDomain period), EulerTransportDerivatives.fieldDerivative period (0, 1) Q x = (EulerPacketCrossProduct.potentialMultiplier ((ContinuousLinearMap.adjoint ↑(F x.1).symm) m₀)) (A x)) (p : ℕ) : ↑↑(piolaPairLp period κ m₀ Ξ Q hΞ hc hQ p) =ᵐ[EulerLiftedGradientSpace.liftMeasure period] fun (x : EulerLiftedGradientSpace.LiftDomain period) => (F x.1).symm (κ ^ p • A x + κ ^ (p + 1) • liftedSlowCurl period F Q x)