The spatial Hessian is C¹ in target time and position on forward strips.

noncomputable def AVenhance.Infra.Flow.HessianJointC1.flowHessianCoordinates : (Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) ≃L[ℝ] Fin 2 → Fin 2 → Homogenization.Vec 2

Continuous linear identification of nested Hessians with their coordinate values.

Equations

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

theorem AVenhance.Infra.Flow.HessianJointC1.flowHessianCoordinates_apply (H : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2) (i j : Fin 2) : flowHessianCoordinates H i j = (H ((Pi.basisFun ℝ (Fin 2)) i)) ((Pi.basisFun ℝ (Fin 2)) j)

theorem AVenhance.Infra.Flow.HessianJointC1.spatialSecondDerivativeEval_jointContinuous {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) : Continuous fun (p : ℝ × Homogenization.Vec 2 × Homogenization.Vec 2 × Homogenization.Vec 2) => spatialSecondDerivativeEval b p.1 p.2.1 p.2.2.1 p.2.2.2

theorem AVenhance.Infra.Flow.HessianJointC1.flowSecondSpatialDerivative_apply_hasDerivAt_of_lt {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (x h k : Homogenization.Vec 2) (s t : ℝ) (hst : s < t) : HasDerivAt (fun (r : ℝ) => ((flowSecondSpatialDerivative X r x s) h) k) ((jointSpatialFDeriv b t (X t x s)) (((flowSecondSpatialDerivative X t x s) h) k) + spatialSecondDerivativeEval b t (X t x s) ((fderiv ℝ (fun (y : Homogenization.Vec 2) => X t y s) x) h) ((fderiv ℝ (fun (y : Homogenization.Vec 2) => X t y s) x) k)) t

theorem AVenhance.Infra.Flow.HessianJointC1.flowHessianCoordinate_contDiffOn_one_of_le {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s T : ℝ) (h k : Homogenization.Vec 2) : ContDiffOn ℝ 1 (fun (p : ℝ × Homogenization.Vec 2) => ((flowSecondSpatialDerivative X p.1 p.2 s) h) k) (Set.Ioo s T ×ˢ Set.univ)

theorem AVenhance.Infra.Flow.flowSecondSpatialDerivative_contDiffOn_one_of_le {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (s T : ℝ) : ContDiffOn ℝ 1 (fun (p : ℝ × Homogenization.Vec 2) => flowSecondSpatialDerivative X p.1 p.2 s) (Set.Ioo s T ×ˢ Set.univ)

The spatial Hessian is jointly C¹ in target time and initial position on forward open strips for fixed start time.