Literal spatial advection of smooth continuous cylinder paths, with unchanged word radius.

A literal product with one mixed cylinder derivative consumes exactly one shift.

noncomputable def EulerCylinderPathProduct.scalarDerivativeProductPath (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (L : EulerSmoothLimit.Space →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (i : Fin 4) : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))

The continuous L² path for one factor times an actual spatial or angular derivative.

Equations

• EulerCylinderPathProduct.scalarDerivativeProductPath P L hL p q hp hq i = EulerCylinderPathProduct.scalarProductPath P L hL p (EulerCylinderSmoothOrbit.derivativePath P q i) hp ⋯

theorem EulerCylinderPathProduct.scalarDerivativeProductPath_orbit (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (L : EulerSmoothLimit.Space →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (i : Fin 4) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (scalarDerivativeProductPath P L hL p q hp hq i)

theorem EulerCylinderPathProduct.pointField_scalarDerivativeProductPath (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (L : EulerSmoothLimit.Space →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (i : Fin 4) (t : K) (x : EulerLiftedGradientSpace.LiftDomain P) : EulerCylinderSmoothOrbit.pointField P (scalarDerivativeProductPath P L hL p q hp hq i) ⋯ t x = L (EulerCylinderSmoothOrbit.pointField P p hp t x) • (EulerLiftedWeakDerivative.fieldFDeriv P (EulerCylinderSmoothOrbit.pointField P q hq t) x) (EulerCylinderSobolev.standardDirection i)

theorem EulerCylinderPathProduct.scalarDerivativeProductPath_majorant (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (L : EulerSmoothLimit.Space →L[ℝ] ℝ) (hL : ‖L‖ ≤ 1) (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (i : Fin 4) (R A C : ℝ) (hR : 0 ≤ R) (hA : 0 ≤ A) (hC : 0 ≤ C) (d e : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) (hb : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6 (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) p) n a ≤ A * EulerGevrey.majorant R d n) (hc : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6 (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) q) n a ≤ C * EulerGevrey.majorant R e n) (n : ℕ) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6 (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) (scalarDerivativeProductPath P L hL p q hp hq i)) n a ≤ 3 * productBlockConstant P * A * C * EulerGevrey.majorant R (d + e + 1) n

Fixed-H6 external word bounds preserve the same radius, with one derivative shift.

theorem EulerCylinderPathProduct.sum_spatial_components (u : EulerSmoothLimit.Space) : ∑ i : Fin 3, (component i) u • EulerCylinderSobolev.standardDirection i.succ = (u, 0)

theorem EulerCylinderPathProduct.spatial_advection_components (D : EulerLiftedGradientSpace.LiftTangent →L[ℝ] EulerSmoothLimit.Space) (u : EulerSmoothLimit.Space) : ∑ i : Fin 3, (component i) u • D (EulerCylinderSobolev.standardDirection i.succ) = D (u, 0)

noncomputable def EulerCylinderPathProduct.advectionPath (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))

The actual path representing p·∇q, where the derivative is spatial and the angle is retained.

Equations

• EulerCylinderPathProduct.advectionPath P p q hp hq = ∑ i : Fin 3, EulerCylinderPathProduct.scalarDerivativeProductPath P (EulerCylinderPathProduct.component i) ⋯ p q hp hq i.succ

theorem EulerCylinderPathProduct.advectionPath_orbit (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) (advectionPath P p q hp hq)

theorem EulerCylinderPathProduct.advectionPath_ae (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (t : K) : ↑↑((advectionPath P p q hp hq) t) =ᵐ[EulerLiftedGradientSpace.liftMeasure P] fun (x : EulerLiftedGradientSpace.LiftDomain P) => (EulerLiftedWeakDerivative.fieldFDeriv P (EulerCylinderSmoothOrbit.pointField P q hq t) x) (EulerCylinderSmoothOrbit.pointField P p hp t x, 0)

theorem EulerCylinderPathProduct.pointField_advectionPath (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (t : K) (x : EulerLiftedGradientSpace.LiftDomain P) : EulerCylinderSmoothOrbit.pointField P (advectionPath P p q hp hq) ⋯ t x = (EulerLiftedWeakDerivative.fieldFDeriv P (EulerCylinderSmoothOrbit.pointField P q hq t) x) (EulerCylinderSmoothOrbit.pointField P p hp t x, 0)

theorem EulerCylinderPathProduct.advectionPath_majorant (P : ℝ) [Fact (0 < P)] {K : Type u_1} [TopologicalSpace K] [CompactSpace K] (p q : C(K, ↥(EulerLiftedGradientSpace.LiftL2 P))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (hq : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) q) (R A C : ℝ) (hR : 0 ≤ R) (hA : 0 ≤ A) (hC : 0 ≤ C) (d e : ℕ) (a : EulerLiftedGradientSpace.LiftTangent) (hb : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6 (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) p) n a ≤ A * EulerGevrey.majorant R d n) (hc : ∀ (n : ℕ), EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6 (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) q) n a ≤ C * EulerGevrey.majorant R e n) (n : ℕ) : EulerParameterWordGevrey.block EulerCylinderSobolev.standardDirection 6 (fun (b : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P b) (advectionPath P p q hp hq)) n a ≤ 9 * productBlockConstant P * A * C * EulerGevrey.majorant R (d + e + 1) n

Actual H6 word blocks for spatial advection consume just one derivative shift.