Joint regularity of the spatial derivatives of a jointly C² function

For v jointly C² on [0,∞) × ℝ² the forcing advDiffOp b κ v is jointly continuous on (0,∞) × ℝ² (whenever the drift b is), and the spatial gradient of a jointly C¹ function is jointly continuous up to t = 0.

theorem AVenhance.Infra.Section5.Integration.Energy.fderiv_slice_eq_fderivWithin_one {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ 1 (Function.uncurry T) (Set.Ici 0 ×ˢ Set.univ)) {t : ℝ} (ht : 0 ≤ t) (x v : Homogenization.Vec 2) : (fderiv ℝ (T t) x) v = (fderivWithin ℝ (Function.uncurry T) (Set.Ici 0 ×ˢ Set.univ) (t, x)) (0, v)

The slice derivative of a jointly C¹ function is the within-derivative in the spatial direction.

theorem AVenhance.Infra.Section5.Integration.Energy.spaceGrad_continuousOn_one {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ 1 (Function.uncurry T) (Set.Ici 0 ×ˢ Set.univ)) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => spaceGrad (T p.1) p.2) (Set.Ici 0 ×ˢ Set.univ)

The joint spatial gradient of a jointly C¹ function is continuous up to t = 0.

theorem AVenhance.Infra.Section5.Integration.Energy.fderiv_slice_apply {A : ℝ × Homogenization.Vec 2 → ℝ} {s : ℝ} {x : Homogenization.Vec 2} (hA : DifferentiableAt ℝ A (s, x)) (w : Homogenization.Vec 2) : (fderiv ℝ (fun (y : Homogenization.Vec 2) => A (s, y)) x) w = (fderiv ℝ A (s, x)) (0, w)

Fréchet derivative of a spatial slice of a function differentiable at (s,x).

theorem AVenhance.Infra.Section5.Integration.Energy.continuousOn_advDiffOp {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hb : Continuous (Function.uncurry b)) (κ : ℝ) {v : ℝ → Homogenization.Vec 2 → ℝ} (hv : ContDiffOn ℝ 2 (Function.uncurry v) (Set.Ici 0 ×ˢ Set.univ)) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => advDiffOp b κ v p.1 p.2) Classical.classicalPositiveTimeDomain

The forcing advDiffOp b κ v is jointly continuous on (0,∞) × ℝ² when v is jointly C² and the drift is continuous.