The primary's literal velocity gradient at every spatial point. Its fast derivative is the source shear, and the slow derivative has an explicit inverse-frequency factor.
noncomputable def
EulerPacketPrimaryShear.slowGraphDerivative
(q : EulerLiftedGradientSpace.LiftTangent → EulerSmoothLimit.Space)
(k : ℝ)
(m : EulerSmoothLimit.Space)
(Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(J : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)
(x : EulerSmoothLimit.Space)
:
Slow graph derivative, given by k⁻¹ • ((fderiv ℝ q (graphMap k m (Y x))).comp (inl ℝ Space ℝ)).comp J.
Equations
- EulerPacketPrimaryShear.slowGraphDerivative q k m Y J x = k⁻¹ • (fderiv ℝ q ((EulerGraphPullback.graphMap k m) (Y x)) ∘SL ContinuousLinearMap.inl ℝ EulerSmoothLimit.Space ℝ) ∘SL J
Instances For
theorem
EulerPacketPrimaryShear.graph_vector_hasFDerivAt
(q : EulerLiftedGradientSpace.LiftTangent → EulerSmoothLimit.Space)
(k : ℝ)
(hk : k ≠ 0)
(m : EulerSmoothLimit.Space)
(Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(J : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)
(x : EulerSmoothLimit.Space)
(hY : HasFDerivAt Y J x)
(hq : DifferentiableAt ℝ q ((EulerGraphPullback.graphMap k m) (Y x)))
:
HasFDerivAt (fun (y : EulerSmoothLimit.Space) => k⁻¹ • q ((EulerGraphPullback.graphMap k m) (Y y)))
(((InnerProductSpace.rankOne ℝ) ((fderiv ℝ q ((EulerGraphPullback.graphMap k m) (Y x))) (0, 1)))
((ContinuousLinearMap.adjoint J) m) + slowGraphDerivative q k m Y J x)
x
theorem
EulerPacketPrimaryShear.slowGraphDerivative_norm_le
(q : EulerLiftedGradientSpace.LiftTangent → EulerSmoothLimit.Space)
(k : ℝ)
(m : EulerSmoothLimit.Space)
(Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space)
(J : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space)
(x : EulerSmoothLimit.Space)
:
theorem
EulerPacketPrimaryShear.scaled_terminal_angular_fderiv
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(hδ : 0 < δ)
(ξ : U)
(hs : tsupport EulerSpatialCutoffs.innerCutoff ⊆ D.support)
(a : ℝ)
(t : ↑(Set.Icc 0 D.T))
(z : EulerLiftedGradientSpace.LiftTangent)
:
(fderiv ℝ
(fun (y : EulerSmoothLimit.Space × ℝ) =>
EulerTransversePacketPrimary.vector τ hτ hτT B (EulerPacketTerminalDatum.initialData D δ hδ (a • ξ) hs) (↑t, y))
z)
(0, 1) = (a * deriv (EulerPeriodicProfile.profile δ) z.2) • EulerPacketPrimaryFactorization.canonicalVelocity τ hτ hτT B ξ hs (↑t) z.1
theorem
EulerPacketPrimaryShear.scaled_terminal_global_gradient
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(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⁻¹ • EulerTransversePacketPrimary.vector τ hτ hτT B (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 ℝ) (EulerPacketPrimaryFactorization.canonicalVelocity τ hτ hτT B ξ hs (↑t) (Y x)))
((D.normal.field t) (Y x)) + slowGraphDerivative
(fun (z : EulerLiftedGradientSpace.LiftTangent) =>
EulerTransversePacketPrimary.vector τ hτ hτT B (EulerPacketTerminalDatum.initialData D δ hδ (a • ξ) hs) (↑t, z))
k D.m₀ Y ((D.FInv.field t) (Y x)) x
theorem
EulerPacketPrimaryShear.scaled_terminal_global_gradient_bound
{U : Type u_1}
[NormedAddCommGroup U]
[InnerProductSpace ℝ U]
[CompleteSpace U]
{D : EulerTransversePacketProvider.Data U}
(τ : ℝ)
(hτ : 0 < τ)
(hτT : τ < D.T)
(B : EulerTransversePacketProvider.HistoryData (D.initial τ hτ ⋯))
(δ : ℝ)
(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 :
(EulerTransversePacketPrimary.vectorField τ hτ hτT B
(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⁻¹ • EulerTransversePacketPrimary.vector τ hτ hτT B (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 ℝ) (EulerPacketPrimaryFactorization.canonicalVelocity τ hτ hτT B ξ hs (↑t) (Y x)))
((D.normal.field t) (Y x))‖ ≤ ‖↑EulerCylinderCoordinates.coordinateEquiv.symm‖ * (EulerCylinderSobolevSpace.sobolevEmbeddingConstant EulerPacketTerminalDatum.period 3 * A * R) * C / k