Joint forward-time continuity of the second spatial derivative.

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

The second spatial derivative, as a nested continuous linear map.

Equations

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

theorem AVenhance.Infra.Flow.flowSecondSpatialDerivative_jointContinuousOn_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 : ℝ) (hst : s ≤ T) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => flowSecondSpatialDerivative X p.1 p.2 s) (Set.Icc s T ×ˢ Set.univ)

On forward compact target-time intervals, the second spatial derivative varies jointly continuously with target time and initial point.

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

For fixed start time, the second spatial derivative is jointly continuous in target time and initial point across both time orientations.