The literal slow curl as a continuous cylinder L² path with same-radius bounds.

Coordinate realization of the actual slow curl and its bounded coefficients.

@[instance_reducible]

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

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

Equations

• EulerPacketPiola.instPacketCurlCoordinates1 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerPacketPiola.instPacketCurlCoordinates2 = inferInstance

noncomputable def EulerPacketPiola.curlCoefficient (i : Fin 3) : (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) →L[ℝ] EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

The coefficient of one genuine spatial derivative in the slow curl.

Equations

• EulerPacketPiola.curlCoefficient i = EulerPacketCrossProduct.crossOperator ∘SL (ContinuousLinearMap.apply ℝ EulerSmoothLimit.Space) (EuclideanSpace.single i 1) ∘SL ↑↑ContinuousLinearMap.adjoint

@[simp]

theorem EulerPacketPiola.curlCoefficient_apply (i : Fin 3) (G : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : (curlCoefficient i) G = EulerPacketCrossProduct.crossLeft ((ContinuousLinearMap.adjoint G) (EuclideanSpace.single i 1))

theorem EulerPacketPiola.curlCoefficient_norm (i : Fin 3) : ‖curlCoefficient i‖ ≤ 1

theorem EulerPacketPiola.slowDerivative_coordinates (D : EulerLiftedGradientSpace.LiftTangent →L[ℝ] EulerSmoothLimit.Space) (G : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : D ∘SL ContinuousLinearMap.inl ℝ EulerSmoothLimit.Space ℝ ∘SL G = ∑ i : Fin 3, ((InnerProductSpace.rankOne ℝ) (D (EulerCylinderSobolev.standardDirection i.succ))) ((ContinuousLinearMap.adjoint G) (EuclideanSpace.single i 1))

theorem EulerPacketPiola.curlMatrix_coordinates (D : EulerLiftedGradientSpace.LiftTangent →L[ℝ] EulerSmoothLimit.Space) (G : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) : EulerMeanBoundary.curlMatrix (D ∘SL ContinuousLinearMap.inl ℝ EulerSmoothLimit.Space ℝ ∘SL G) = ∑ i : Fin 3, ((curlCoefficient i) G) (D (EulerCylinderSobolev.standardDirection i.succ))

The literal slow curl is a sum of three rectangular coefficient products.

@[instance_reducible]

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

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

Equations

• EulerPacketPiola.instPacketCurlCoordinates3 = inferInstance

@[instance_reducible]

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

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

Equations

• EulerPacketPiola.instPacketCurlCoordinates4 = inferInstance

noncomputable def EulerPacketPiola.curlCoefficientPath {K : Type u_1} [TopologicalSpace K] (i : Fin 3) : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)) →L[ℝ] C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

Curl coefficient path, given by ((curlCoefficient i).compLeftContinuousBounded Space).compLeftContinuous ℝ K.

Equations

• EulerPacketPiola.curlCoefficientPath i = ContinuousLinearMap.compLeftContinuous ℝ K (ContinuousLinearMap.compLeftContinuousBounded EulerSmoothLimit.Space (EulerPacketPiola.curlCoefficient i))

@[simp]

theorem EulerPacketPiola.curlCoefficientPath_apply {K : Type u_1} [TopologicalSpace K] (i : Fin 3) (G : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (t : K) (y : EulerSmoothLimit.Space) : (((curlCoefficientPath i) G) t) y = (curlCoefficient i) ((G t) y)

theorem EulerPacketPiola.curlCoefficientPath_norm {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (i : Fin 3) : ‖curlCoefficientPath i‖ ≤ 1

theorem EulerPacketPiola.curlCoefficientPath_translation {K : Type u_1} [TopologicalSpace K] (i : Fin 3) (G : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (a : EulerSmoothLimit.Space) : EulerMeanCoefficients.translateCoefficientPath ((curlCoefficientPath i) G) a = (curlCoefficientPath i) (EulerMeanCoefficients.translateCoefficientPath G a)

theorem EulerPacketPiola.curlCoefficientPath_orbit {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (i : Fin 3) (G : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hG : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath G)) : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath ((curlCoefficientPath i) G))

theorem EulerPacketPiola.curlCoefficientPath_bound {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (i : Fin 3) (G : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hG : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath G)) (n : ℕ) (C : ℝ) (hb : ∀ (a : EulerSmoothLimit.Space), ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath G) a‖ ≤ C) (a : EulerSmoothLimit.Space) : ‖iteratedFDeriv ℝ n (EulerMeanCoefficients.translateCoefficientPath ((curlCoefficientPath i) G)) a‖ ≤ C

@[instance_reducible]

noncomputable def EulerCylinderSlowCurl.instCylinderSlowCurl1 : NormedAddCommGroup (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurl1 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSlowCurl.instCylinderSlowCurl2 : NormedSpace ℝ (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurl2 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSlowCurl.instCylinderSlowCurl3 : NormedAddCommGroup (EulerLiftedGradientSpace.LiftTangent →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurl3 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSlowCurl.instCylinderSlowCurl4 : NormedSpace ℝ (EulerLiftedGradientSpace.LiftTangent →L[ℝ] EulerSmoothLimit.Space)

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

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurl4 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSlowCurl.instCylinderSlowCurl5 : NormedAddCommGroup (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurl5 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSlowCurl.instCylinderSlowCurl6 : NormedSpace ℝ (BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurl6 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSlowCurl.instCylinderSlowCurl7 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurl7 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSlowCurl.instCylinderSlowCurl8 {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))

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

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurl8 = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSlowCurl.instCylinderSlowCurl9 (P : ℝ) [Fact (0 < P)] : NormedAddCommGroup ↥(EulerLiftedGradientSpace.LiftL2 P)

Cache the standard NormedAddCommGroup (LiftL2 P) instance to shorten typeclass synthesis.

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurl9 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSlowCurl.instCylinderSlowCurl10 (P : ℝ) [Fact (0 < P)] : NormedSpace ℝ ↥(EulerLiftedGradientSpace.LiftL2 P)

Cache the standard NormedSpace ℝ (LiftL2 P) instance to shorten typeclass synthesis.

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurl10 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSlowCurl.instCylinderSlowCurl11 (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedAddCommGroup C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))

Cache the standard NormedAddCommGroup C(K,LiftL2 P) instance to shorten typeclass synthesis.

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurl11 P = inferInstance

@[instance_reducible]

noncomputable def EulerCylinderSlowCurl.instCylinderSlowCurl12 (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] : NormedSpace ℝ C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))

Cache the standard NormedSpace ℝ C(K,LiftL2 P) instance to shorten typeclass synthesis.

Equations

• EulerCylinderSlowCurl.instCylinderSlowCurl12 P = inferInstance

noncomputable def EulerCylinderSlowCurl.term (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (G : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (i : Fin 3) : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))

Term, given by fullMultiplierMap P (curlCoefficientPath i G) (derivativePath P p i.succ).

Equations

• EulerCylinderSlowCurl.term P G p i = ((EulerLpCylinderRectangular.fullMultiplierMap P) ((EulerPacketPiola.curlCoefficientPath i) G)) (EulerCylinderSmoothOrbit.derivativePath P p i.succ)

theorem EulerCylinderSlowCurl.term_orbit (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (G : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hG : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath G)) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (i : Fin 3) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (term P G p i)

noncomputable def EulerCylinderSlowCurl.path (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (G : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))

Path, given by ∑ i : Fin 3, term P G p i.

Equations

• EulerCylinderSlowCurl.path P G p = ∑ i : Fin 3, EulerCylinderSlowCurl.term P G p i

theorem EulerCylinderSlowCurl.path_orbit (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (G : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hG : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath G)) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (path P G p)

theorem EulerCylinderSlowCurl.term_ae (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (G : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (i : Fin 3) (t : K) : ↑↑((term P G p i) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] fun (x : EulerLiftedGradientSpace.LiftDomain P) => ((EulerPacketPiola.curlCoefficient i) ((G t) x.1)) ((EulerLiftedWeakDerivative.fieldFDeriv P (EulerCylinderSmoothOrbit.pointField P p hp t) x) (EulerCylinderSobolev.standardDirection i.succ))

theorem EulerCylinderSlowCurl.path_ae (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (G : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (t : K) : ↑↑((path P G p) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] fun (x : EulerLiftedGradientSpace.LiftDomain P) => EulerMeanBoundary.curlMatrix (EulerLiftedWeakDerivative.fieldFDeriv P (EulerCylinderSmoothOrbit.pointField P p hp t) x ∘SL ContinuousLinearMap.inl ℝ EulerSmoothLimit.Space ℝ ∘SL (G t) x.1)

noncomputable def EulerCylinderSlowCurl.field (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (G : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hG : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath G)) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (t : K) : EulerLiftedGradientSpace.LiftDomain P → EulerSmoothLimit.Space

Field, given by pointField P (path P G p) (path_orbit P G hG p hp) t.

Equations

• EulerCylinderSlowCurl.field P G hG p hp t = EulerCylinderSmoothOrbit.pointField P (EulerCylinderSlowCurl.path P G p) ⋯ t

theorem EulerCylinderSlowCurl.field_formula (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (G : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hG : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath G)) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (t : K) (x : EulerLiftedGradientSpace.LiftDomain P) : field P G hG p hp t x = EulerMeanBoundary.curlMatrix (EulerLiftedWeakDerivative.fieldFDeriv P (EulerCylinderSmoothOrbit.pointField P p hp t) x ∘SL ContinuousLinearMap.inl ℝ EulerSmoothLimit.Space ℝ ∘SL (G t) x.1)

The reconstructed L² path is exactly the classical curl used in the packet.

theorem EulerCylinderSlowCurl.field_eq_liftedSlowCurl (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (G : C(K, BoundedContinuousFunction EulerSmoothLimit.Space (EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space))) (hG : ContDiff ℝ (↑⊤) (EulerMeanCoefficients.translateCoefficientPath G)) (p : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (F : K → EulerSmoothLimit.Space → EulerSmoothLimit.Space ≃L[ℝ] EulerSmoothLimit.Space) (hF : ∀ (t : K) (y : EulerSmoothLimit.Space), (G t) y = ↑(F t y).symm) (t : K) : field P G hG p hp t = EulerPacketPiola.liftedSlowCurl P (F t) (EulerCylinderSmoothOrbit.pointField P p hp t)