The literal spatial gradient of an actual scalar cylinder path is an actual vector path.

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

Gradient component, given by (toSpanSingleton ℝ (basisVector i)).comp scalarProject.

Equations

• EulerPacketCylinderField.gradientComponent i = ContinuousLinearMap.toSpanSingleton ℝ (EulerCylinderPathProduct.basisVector i) ∘SL EulerCylinderScalarPrimitive.scalarProject

theorem EulerPacketCylinderField.gradientComponent_norm (i : Fin 3) : ‖gradientComponent i‖ ≤ 1

theorem EulerPacketCylinderField.gradient_eq_sum (D : EulerLiftedGradientSpace.LiftTangent →L[ℝ] ℝ) : (InnerProductSpace.toDual ℝ EulerSmoothLimit.Space).symm (D ∘SL ContinuousLinearMap.inl ℝ EulerSmoothLimit.Space ℝ) = ∑ i : Fin 3, D (EulerCylinderSobolev.standardDirection i.succ) • EulerCylinderPathProduct.basisVector i

noncomputable def EulerPacketCylinderField.scalarEmbeddingField {P T : ℝ} [Fact (0 < P)] (raw : EulerPacketProfileRecursion.ScalarField) (p : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (he : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, x, θ) = EulerCylinderScalarPrimitive.scalarPointField P p hp t (x, ↑θ)) : Field P T fun (z : EulerPacketPointJets.Domain) => EulerCylinderScalarPrimitive.scalarEmbed (raw z)

A norm-one scalar embedding retains the actual continuous L² path.

Equations

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

theorem EulerPacketCylinderField.scalarRaw_smooth {P T : ℝ} [Fact (0 < P)] (raw : EulerPacketProfileRecursion.ScalarField) (p : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (he : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, x, θ) = EulerCylinderScalarPrimitive.scalarPointField P p hp t (x, ↑θ)) (t : ↑(Set.Icc 0 T)) : ContDiff ℝ ↑⊤ fun (y : EulerLiftedGradientSpace.LiftTangent) => raw (↑t, y)

noncomputable def EulerPacketCylinderField.scalarGradientField {P T : ℝ} [Fact (0 < P)] (raw : EulerPacketProfileRecursion.ScalarField) (p : C(↑(Set.Icc 0 T), ↥(EulerLpCylinderTranslation.CylinderL2 P ℝ))) (hp : ContDiff ℝ ↑⊤ fun (a : EulerLiftedGradientSpace.LiftTangent) => (EulerLpCylinderTranslation.pathTranslate P a) p) (he : ∀ (t : ↑(Set.Icc 0 T)) (x : EulerSmoothLimit.Space) (θ : ℝ), raw (↑t, x, θ) = EulerCylinderScalarPrimitive.scalarPointField P p hp t (x, ↑θ)) : Field P T (pressureGradient raw)

This witness is the spatial gradient used by pressureJet; it needs no time derivative.

Equations

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