Taylor control for the second spatial derivative of the field.

def AVenhance.Infra.Flow.ThirdFieldTaylor.thirdTaylorDirections2 (h k : Homogenization.Vec 2) : Fin 2 → ℝ × Homogenization.Vec 2

Two spatial directions embedded into time-space for the field Taylor expansion.

Equations

• AVenhance.Infra.Flow.ThirdFieldTaylor.thirdTaylorDirections2 h k i = if i = 0 then (0, h) else (0, k)

theorem AVenhance.Infra.Flow.ThirdFieldTaylor.fderiv_spatialSecondDerivativeEval_apply {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) (t : ℝ) (x h k v : Homogenization.Vec 2) : (fderiv ℝ (fun (z : Homogenization.Vec 2) => spatialSecondDerivativeEval b t z h k) x) v = spatialThirdDerivativeEval b t x v h k

theorem AVenhance.Infra.Flow.exists_global_spatialSecondDerivativeEval_taylor_remainder {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : SmoothPeriodicField b) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (t : ℝ) (x y h k : Homogenization.Vec 2), ‖spatialSecondDerivativeEval b t y h k - spatialSecondDerivativeEval b t x h k - spatialThirdDerivativeEval b t x (y - x) h k‖ ≤ C * ‖h‖ * ‖k‖ * ‖y - x‖ * ‖y - x‖

The field Hessian has a quadratic Taylor remainder whose linear term is its third spatial derivative.