Differentiating an actual oscillatory scalar pressure through the inverse flow. The principal Hessian is the angular second derivative times the square of the transported normal.

noncomputable def EulerPacketGraphHessian.spatialGradient (q : EulerLiftedGradientSpace.LiftTangent → ℝ) (z : EulerLiftedGradientSpace.LiftTangent) : EulerSmoothLimit.Space

Spatial gradient, given by (toDual ℝ Space).symm ((fderiv ℝ q z).comp (inl ℝ Space ℝ)).

Equations

• EulerPacketGraphHessian.spatialGradient q z = (InnerProductSpace.toDual ℝ EulerSmoothLimit.Space).symm (fderiv ℝ q z ∘SL ContinuousLinearMap.inl ℝ EulerSmoothLimit.Space ℝ)

noncomputable def EulerPacketGraphHessian.angularDerivative (q : EulerLiftedGradientSpace.LiftTangent → ℝ) (z : EulerLiftedGradientSpace.LiftTangent) : ℝ

Angular derivative, given by fderiv ℝ q z (0,1).

Equations

• EulerPacketGraphHessian.angularDerivative q z = (fderiv ℝ q z) (0, 1)

theorem EulerPacketGraphHessian.spatialGradient_contDiff {q : EulerLiftedGradientSpace.LiftTangent → ℝ} (hq : ContDiff ℝ (↑⊤) q) : ContDiff ℝ (↑⊤) (spatialGradient q)

theorem EulerPacketGraphHessian.angularDerivative_contDiff {q : EulerLiftedGradientSpace.LiftTangent → ℝ} (hq : ContDiff ℝ (↑⊤) q) : ContDiff ℝ (↑⊤) (angularDerivative q)

theorem EulerPacketGraphHessian.angularDerivative_eq_deriv {q : EulerLiftedGradientSpace.LiftTangent → ℝ} {z : EulerLiftedGradientSpace.LiftTangent} (hq : DifferentiableAt ℝ q z) : angularDerivative q z = deriv (fun (θ : ℝ) => q (z.1, θ)) z.2

theorem EulerPacketGraphHessian.angularSecond_eq_deriv {q : EulerLiftedGradientSpace.LiftTangent → ℝ} (hq : ContDiff ℝ (↑⊤) q) (z : EulerLiftedGradientSpace.LiftTangent) : angularDerivative (angularDerivative q) z = deriv (deriv fun (θ : ℝ) => q (z.1, θ)) z.2

theorem EulerPacketGraphHessian.graph_decomposition (k : ℝ) (m v : EulerSmoothLimit.Space) : (EulerGraphPullback.graphMap k m) v = (v, 0) + (k * inner ℝ m v) • (0, 1)

theorem EulerPacketGraphHessian.gradient_graph {q : EulerLiftedGradientSpace.LiftTangent → ℝ} (k : ℝ) (m x : EulerSmoothLimit.Space) (hq : DifferentiableAt ℝ q ((EulerGraphPullback.graphMap k m) x)) : gradient (fun (y : EulerSmoothLimit.Space) => q ((EulerGraphPullback.graphMap k m) y)) x = spatialGradient q ((EulerGraphPullback.graphMap k m) x) + (k * angularDerivative q ((EulerGraphPullback.graphMap k m) x)) • m

theorem EulerPacketGraphHessian.gradient_physical {q : EulerLiftedGradientSpace.LiftTangent → ℝ} (k : ℝ) (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))) : gradient (fun (y : EulerSmoothLimit.Space) => k⁻¹ ^ 2 * q ((EulerGraphPullback.graphMap k m) (Y y))) x = k⁻¹ ^ 2 • (ContinuousLinearMap.adjoint J) (spatialGradient q ((EulerGraphPullback.graphMap k m) (Y x))) + (k⁻¹ ^ 2 * k * angularDerivative q ((EulerGraphPullback.graphMap k m) (Y x))) • (ContinuousLinearMap.adjoint J) m

noncomputable def EulerPacketGraphHessian.transportedNormal (m : EulerSmoothLimit.Space) (J : EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Transported normal, given by (J x).adjoint m.

Equations

• EulerPacketGraphHessian.transportedNormal m J x = (ContinuousLinearMap.adjoint (J x)) m

noncomputable def EulerPacketGraphHessian.slowForce (q : EulerLiftedGradientSpace.LiftTangent → ℝ) (k : ℝ) (m : EulerSmoothLimit.Space) (Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (J : EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space

Slow force, given by (J x).adjoint (spatialGradient q (graphMap k m (Y x))).

Equations

• EulerPacketGraphHessian.slowForce q k m Y J x = (ContinuousLinearMap.adjoint (J x)) (EulerPacketGraphHessian.spatialGradient q ((EulerGraphPullback.graphMap k m) (Y x)))

noncomputable def EulerPacketGraphHessian.lowerHessian (q : EulerLiftedGradientSpace.LiftTangent → ℝ) (k : ℝ) (m : EulerSmoothLimit.Space) (Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (J : EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space

Lower hessian as an element of Space →L[ℝ] Space.

Equations

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

theorem EulerPacketGraphHessian.hessian_physical {q : EulerLiftedGradientSpace.LiftTangent → ℝ} (hq : ContDiff ℝ (↑⊤) q) (k : ℝ) (hk : k ≠ 0) (m : EulerSmoothLimit.Space) (Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (J : EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (hY : ∀ (x : EulerSmoothLimit.Space), HasFDerivAt Y (J x) x) (x : EulerSmoothLimit.Space) (hJ : DifferentiableAt ℝ J x) : fderiv ℝ (gradient fun (y : EulerSmoothLimit.Space) => k⁻¹ ^ 2 * q ((EulerGraphPullback.graphMap k m) (Y y))) x = angularDerivative (angularDerivative q) ((EulerGraphPullback.graphMap k m) (Y x)) • ((InnerProductSpace.rankOne ℝ) (transportedNormal m J x)) (transportedNormal m J x) + lowerHessian q k m Y J x

theorem EulerPacketGraphHessian.lowerHessian_norm_le (q : EulerLiftedGradientSpace.LiftTangent → ℝ) (k : ℝ) (m : EulerSmoothLimit.Space) (Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (J : EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : ‖lowerHessian q k m Y J x‖ ≤ |k⁻¹| ^ 2 * ‖fderiv ℝ (slowForce q k m Y J) x‖ + |k⁻¹| * (|angularDerivative q ((EulerGraphPullback.graphMap k m) (Y x))| * ‖fderiv ℝ (transportedNormal m J) x‖ + ‖fderiv ℝ (angularDerivative q) ((EulerGraphPullback.graphMap k m) (Y x)) ∘SL ContinuousLinearMap.inl ℝ EulerSmoothLimit.Space ℝ‖ * ‖J x‖ * ‖transportedNormal m J x‖)