The third spatial derivative on forward target-time strips.

noncomputable def AVenhance.Infra.Flow.flowThirdSpatialDerivative (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) (t : ℝ) (x : Homogenization.Vec 2) (s : ℝ) : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2

The third spatial derivative, viewed as the derivative of the Hessian.

Equations

• AVenhance.Infra.Flow.flowThirdSpatialDerivative X t x s = fderiv ℝ (fun (y : Homogenization.Vec 2) => AVenhance.Infra.Flow.flowSecondSpatialDerivative X t y s) x

theorem AVenhance.Infra.Flow.flowSecondSpatialDerivative_eq_flowSecondVariation_of_le {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (x : Homogenization.Vec 2) (s t : ℝ) (hst : s ≤ t) (h k : Homogenization.Vec 2) : ((flowSecondSpatialDerivative X t x s) h) k = flowSecondVariation hb hX x s ⋯ h k t 0 s

On forward times, the nested spatial Hessian agrees with the selected second variational flow.

theorem AVenhance.Infra.Flow.flowThirdSpatialDerivative_eval_eq_flowThirdVariation_of_le {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (x u h k : Homogenization.Vec 2) (s t : ℝ) (hst : s ≤ t) : (((flowThirdSpatialDerivative X t x s) u) h) k = flowThirdVariation hb hX x s ⋯ u h k t 0 s

On a forward strip, the derivative of the Hessian is the selected third variation.

theorem AVenhance.Infra.Flow.flowThirdSpatialDerivative_continuousOn_of_le {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (h k l : Homogenization.Vec 2) (s T : ℝ) (hst : s ≤ T) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => (((flowThirdSpatialDerivative X p.1 p.2 s) h) k) l) (Set.Icc s T ×ˢ Set.univ)

The third spatial derivative is jointly continuous in target time and initial position on every forward compact strip, with start time fixed.

theorem AVenhance.Infra.Flow.flowThirdSpatialDerivative_continuousOn_forwardHalf {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (h k l : Homogenization.Vec 2) (s : ℝ) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => (((flowThirdSpatialDerivative X p.1 p.2 s) h) k) l) (Set.Ici s ×ˢ Set.univ)

The third spatial derivative is continuous on the entire forward half space, with start time fixed.

theorem AVenhance.Infra.Flow.ThirdSpatialDerivativeJoint.flowSecondSpatialDerivative_reverseTime_eq (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) (t : ℝ) (x : Homogenization.Vec 2) (s : ℝ) : flowSecondSpatialDerivative (regularityReverseTimeFlow X) (-t) x (-s) = flowSecondSpatialDerivative X t x s

theorem AVenhance.Infra.Flow.ThirdSpatialDerivativeJoint.flowThirdSpatialDerivative_reverseTime_eq (X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2) (t : ℝ) (x : Homogenization.Vec 2) (s : ℝ) (h k l : Homogenization.Vec 2) : (((flowThirdSpatialDerivative (regularityReverseTimeFlow X) (-t) x (-s)) h) k) l = (((flowThirdSpatialDerivative X t x s) h) k) l

theorem AVenhance.Infra.Flow.ThirdSpatialDerivativeJoint.continuousOn_reverseTimeMap {s : ℝ} {f : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2} (hf : ContinuousOn f (Set.Ici (-s) ×ˢ Set.univ)) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => f (-p.1, p.2)) (Set.Iic s ×ˢ Set.univ)

theorem AVenhance.Infra.Flow.ThirdSpatialDerivativeJoint.flowThirdSpatialDerivative_reverseMap_continuousOn {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (h k l : Homogenization.Vec 2) (s : ℝ) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => (((flowThirdSpatialDerivative (regularityReverseTimeFlow X) (-p.1) p.2 (-s)) h) k) l) (Set.Iic s ×ˢ Set.univ)

theorem AVenhance.Infra.Flow.flowThirdSpatialDerivative_continuousOn_backwardHalf {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (h k l : Homogenization.Vec 2) (s : ℝ) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => (((flowThirdSpatialDerivative X p.1 p.2 s) h) k) l) (Set.Iic s ×ˢ Set.univ)

The third spatial derivative is continuous on the entire backward half space, with start time fixed.

theorem AVenhance.Infra.Flow.flowThirdSpatialDerivative_continuous_fixed_start {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) {X : ℝ → Homogenization.Vec 2 → ℝ → Homogenization.Vec 2} (hX : IsFlow b X) (h k l : Homogenization.Vec 2) (s : ℝ) : Continuous fun (p : ℝ × Homogenization.Vec 2) => (((flowThirdSpatialDerivative X p.1 p.2 s) h) k) l

The third spatial derivative is jointly continuous in target time and initial position for every target time, with start time fixed.