The leading angular pressure force gives its actual rank-one Hessian. Only first slow derivatives occur in the remainder.

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

Fast force, given by k⁻¹ • (a (graphMap k m (Y x)) • transportedNormal m J x).

Equations

• EulerPacketGraphHessian.fastForce a k m Y J x = k⁻¹ • a ((EulerGraphPullback.graphMap k m) (Y x)) • EulerPacketGraphHessian.transportedNormal m J x

noncomputable def EulerPacketGraphHessian.fastHessianRemainder (a : 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

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

Equations

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

theorem EulerPacketGraphHessian.fastForce_hasFDerivAt (a : EulerLiftedGradientSpace.LiftTangent → ℝ) (k : ℝ) (hk : k ≠ 0) (m : EulerSmoothLimit.Space) (Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (J : EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) (hY : HasFDerivAt Y (J x) x) (hJ : DifferentiableAt ℝ J x) (ha : DifferentiableAt ℝ a ((EulerGraphPullback.graphMap k m) (Y x))) : HasFDerivAt (fastForce a k m Y J) (angularDerivative a ((EulerGraphPullback.graphMap k m) (Y x)) • ((InnerProductSpace.rankOne ℝ) (transportedNormal m J x)) (transportedNormal m J x) + fastHessianRemainder a k m Y J x) x

theorem EulerPacketGraphHessian.fastHessianRemainder_norm_le (a : EulerLiftedGradientSpace.LiftTangent → ℝ) (k : ℝ) (m : EulerSmoothLimit.Space) (Y : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (J : EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) : ‖fastHessianRemainder a k m Y J x‖ ≤ |k⁻¹| * (|a ((EulerGraphPullback.graphMap k m) (Y x))| * ‖fderiv ℝ (transportedNormal m J) x‖ + ‖fderiv ℝ a ((EulerGraphPullback.graphMap k m) (Y x))‖ * ‖J x‖ * ‖transportedNormal m J x‖)

theorem EulerPacketGraphHessian.norm_fderiv_smul_unit (a : EulerLiftedGradientSpace.LiftTangent → ℝ) (m : EulerSmoothLimit.Space) (hm : ‖m‖ = 1) (z : EulerLiftedGradientSpace.LiftTangent) (ha : DifferentiableAt ℝ a z) : ‖fderiv ℝ (fun (y : EulerLiftedGradientSpace.LiftTangent) => a y • m) z‖ = ‖fderiv ℝ a z‖

theorem EulerPacketGraphHessian.norm_fderiv_clm_apply_le (A : EulerSmoothLimit.Space → EulerSmoothLimit.Space →L[ℝ] EulerSmoothLimit.Space) (u : EulerSmoothLimit.Space → EulerSmoothLimit.Space) (x : EulerSmoothLimit.Space) (hA : DifferentiableAt ℝ A x) (hu : DifferentiableAt ℝ u x) : ‖fderiv ℝ (fun (y : EulerSmoothLimit.Space) => (A y) (u y)) x‖ ≤ ‖A x‖ * ‖fderiv ℝ u x‖ + ‖fderiv ℝ A x‖ * ‖u x‖