Literal shear and pressure Hessian of the primary starting at time zero. The leading tensors are derivatives of the actual constructed velocity and scalar pressure, with the slow terms retained exactly.

theorem EulerPacketForwardShear.angular_fderiv {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (a : ℝ) (t : ↑(Set.Icc 0 D.T)) (z : EulerLiftedGradientSpace.LiftTangent) : (fderiv ℝ (fun (y : EulerSmoothLimit.Space × ℝ) => EulerPacketForwardPrimary.vector D (EulerPacketTerminalDatum.initialData D δ hδ (a • ξ) hs) (↑t, y)) z) (0, 1) = (a * deriv (EulerPeriodicProfile.profile δ) z.2) • EulerPacketForwardFactorization.canonicalVelocity D ξ (↑t) z.1

theorem EulerPacketForwardShear.global_gradient {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (a k : ℝ) (hk : k ≠ 0) (t : ↑(Set.Icc 0 D.T)) (Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) (hY : HasFDerivAt Y ((D.FInv.field t) (Y x)) x) : fderiv ℝ (fun (y : EulerSmoothLimit.Space) => k⁻¹ • EulerPacketForwardPrimary.vector D (EulerPacketTerminalDatum.initialData D δ hδ (a • ξ) hs) (↑t, Y y, k * inner ℝ D.m₀ (Y y))) x = (a * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ D.m₀ (Y x))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketForwardFactorization.canonicalVelocity D ξ (↑t) (Y x))) ((D.normal.field t) (Y x)) + EulerPacketPrimaryShear.slowGraphDerivative (fun (z : EulerLiftedGradientSpace.LiftTangent) => EulerPacketForwardPrimary.vector D (EulerPacketTerminalDatum.initialData D δ hδ (a • ξ) hs) (↑t, z)) k D.m₀ Y ((D.FInv.field t) (Y x)) x

theorem EulerPacketForwardShear.global_gradient_bound {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (a k : ℝ) (hk : 0 < k) (R A C : ℝ) (hR : 0 ≤ R) (hA : 0 ≤ A) (_hC : 0 ≤ C) (hG : ((EulerPacketForwardPrimary.forcing D).vectorField (EulerPacketTerminalDatum.initialData D δ hδ (a • ξ) hs)).WordBound 6 R A 0) (t : ↑(Set.Icc 0 D.T)) (Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) (hY : HasFDerivAt Y ((D.FInv.field t) (Y x)) x) (hJ : ‖(D.FInv.field t) (Y x)‖ ≤ C) : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => k⁻¹ • EulerPacketForwardPrimary.vector D (EulerPacketTerminalDatum.initialData D δ hδ (a • ξ) hs) (↑t, Y y, k * inner ℝ D.m₀ (Y y))) x - (a * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ D.m₀ (Y x))) • ((InnerProductSpace.rankOne ℝ) (EulerPacketForwardFactorization.canonicalVelocity D ξ (↑t) (Y x))) ((D.normal.field t) (Y x))‖ ≤ ‖↑EulerCylinderCoordinates.coordinateEquiv.symm‖ * (EulerCylinderSobolevSpace.sobolevEmbeddingConstant EulerPacketTerminalDatum.period 3 * A * R) * C / k

noncomputable def EulerPacketForwardShear.pressureCoefficient {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (ξ : U) (a : ℝ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : ℝ

Pressure coefficient, given by -(2*a*⟪D.normal.field t x,D.M.field t x (canonicalVelocity D ξ t x)⟫_ℝ)/ ‖D.normal.field t x‖^2.

Equations

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

theorem EulerPacketForwardShear.scalar_hasDerivAt {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (a : ℝ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : HasDerivAt (fun (s : ℝ) => EulerPacketForwardPrimary.scalar D (EulerPacketTerminalDatum.initialData D δ hδ (a • ξ) hs) (↑t, x, s)) (pressureCoefficient D ξ a t x * EulerPeriodicProfile.profile δ θ) θ

theorem EulerPacketForwardShear.scalar_deriv {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (a : ℝ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : deriv (fun (s : ℝ) => EulerPacketForwardPrimary.scalar D (EulerPacketTerminalDatum.initialData D δ hδ (a • ξ) hs) (↑t, x, s)) θ = pressureCoefficient D ξ a t x * EulerPeriodicProfile.profile δ θ

theorem EulerPacketForwardShear.scalar_deriv_hasDerivAt {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (a : ℝ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : HasDerivAt (deriv fun (s : ℝ) => EulerPacketForwardPrimary.scalar D (EulerPacketTerminalDatum.initialData D δ hδ (a • ξ) hs) (↑t, x, s)) (pressureCoefficient D ξ a t x * deriv (EulerPeriodicProfile.profile δ) θ) θ

theorem EulerPacketForwardShear.scalar_second_deriv {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (a : ℝ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) (θ : ℝ) : deriv (deriv fun (s : ℝ) => EulerPacketForwardPrimary.scalar D (EulerPacketTerminalDatum.initialData D δ hδ (a • ξ) hs) (↑t, x, s)) θ = pressureCoefficient D ξ a t x * deriv (EulerPeriodicProfile.profile δ) θ

theorem EulerPacketForwardShear.scalar_second_deriv_zero {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (a : ℝ) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : deriv (deriv fun (s : ℝ) => EulerPacketForwardPrimary.scalar D (EulerPacketTerminalDatum.initialData D δ hδ (a • ξ) hs) (↑t, x, s)) 0 = pressureCoefficient D ξ a t x / δ

noncomputable def EulerPacketForwardShear.physicalPressure {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (a k : ℝ) (t : ↑(Set.Icc 0 D.T)) (Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : ℝ

Physical pressure, given by k⁻¹^2 * scalar D (initialData D δ hδ (a • ξ) hs) (t,(Y x,k*⟪D.m₀,Y x⟫_ℝ)).

Equations

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

noncomputable def EulerPacketForwardShear.hessianRemainder {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (a k : ℝ) (t : ↑(Set.Icc 0 D.T)) (Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

Hessian remainder, given by lowerHessian (fun z => scalar D (initialData D δ hδ (a • ξ) hs) (t,z)) k D.m₀ Y (fun y => D.FInv.field t (Y y)) x.

Equations

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

theorem EulerPacketForwardShear.physicalPressure_hessian {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (a k : ℝ) (hk : k ≠ 0) (t : ↑(Set.Icc 0 D.T)) (Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hY : ∀ (x : EulerSmoothLimit.Space), HasFDerivAt Y ((D.FInv.field t) (Y x)) x) (x : EulerSmoothLimit.Space) : fderiv ℝ (gradient (physicalPressure D δ hδ ξ hs a k t Y)) x = (pressureCoefficient D ξ a t (Y x) * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ D.m₀ (Y x))) • ((InnerProductSpace.rankOne ℝ) ((D.normal.field t) (Y x))) ((D.normal.field t) (Y x)) + hessianRemainder D δ hδ ξ hs a k t Y x

theorem EulerPacketForwardShear.physicalPressure_hessian_of_inverse {U : Type u_1} [NormedAddCommGroup U] [InnerProductSpace ℝ U] [CompleteSpace U] (D : EulerTransversePacketProvider.Data U) (δ : ℝ) (hδ : 0 < δ) (ξ : U) (hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support) (a k : ℝ) (hk : k ≠ 0) (X Y : ↑(Set.Icc 0 D.T) → EulerSmoothLimit.Space → EulerSmoothLimit.Space) (hX : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), HasFDerivAt (X t) ((D.F.field t) x) x) (hXY : ∀ (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space), X t (Y t x) = x) (hY : Continuous (Function.uncurry Y)) (t : ↑(Set.Icc 0 D.T)) (x : EulerSmoothLimit.Space) : fderiv ℝ (gradient (physicalPressure D δ hδ ξ hs a k t (Y t))) x = (pressureCoefficient D ξ a t (Y t x) * deriv (EulerPeriodicProfile.profile δ) (k * inner ℝ D.m₀ (Y t x))) • ((InnerProductSpace.rankOne ℝ) ((D.normal.field t) (Y t x))) ((D.normal.field t) (Y t x)) + hessianRemainder D δ hδ ξ hs a k t (Y t) x