Divergence-form expansion of the shear diffusion and its induced drift.

theorem AVenhance.Infra.Section5.DiffusionDivergence.spaceGrad_hasFDerivAt_of_contDiffAt_two {f : Homogenization.Vec 2 → ℝ} {x : Homogenization.Vec 2} (hf : ContDiffAt ℝ 2 f x) : HasFDerivAt (spaceGrad f) (ContinuousLinearMap.pi fun (j : Fin 2) => (fderiv ℝ (fderiv ℝ f) x).flip (Homogenization.basisVec j)) x

theorem AVenhance.Infra.Section5.DiffusionDivergence.spaceLap_eq_diagonal_deriv {f : Homogenization.Vec 2 → ℝ} {x : Homogenization.Vec 2} {L : Homogenization.Vec 2 →L[ℝ] Homogenization.Vec 2} (hgrad : HasFDerivAt (spaceGrad f) L x) : spaceLap f x = ∑ i : Fin 2, L (Homogenization.basisVec i) i

theorem AVenhance.Infra.Section5.shear_diffusion_eq_negative_div {f ψ : Homogenization.Vec 2 → ℝ} {x : Homogenization.Vec 2} (κ : ℝ) (hψ : DifferentiableAt ℝ ψ x) (hf : ContDiffAt ℝ 2 f x) : -κ * spaceLap f x + Homogenization.vecDot (sigmaMat.mulVec (spaceGrad ψ x)) (spaceGrad f x) = -vecDiv (fun (y : Homogenization.Vec 2) => (κ • 1 + ψ y • sigmaMat).mulVec (spaceGrad f y)) x

The source shear drift turns the skew diffusion into divergence form. The spatial regularity hypotheses are precisely one derivative of ψ and two of f; symmetry of the Hessian is derived from the latter.