Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section5.ShearDiffusionOperator

The velocity increment turns the new-scale diffusion into divergence form.

theorem AVenhance.Infra.Section5.advDiffOp_shear_divergence_split {b₀ b₁ : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {ψ : Homogenization.Vec 2 → ℝ} {t : ℝ} {x : Homogenization.Vec 2} (hvelocity : b₁ t x - b₀ t x = sigmaMat.mulVec (spaceGrad ψ x)) (hψ : DifferentiableAt ℝ ψ x) (hu : ContDiffAt ℝ 2 (u t) x) :
advDiffOp b₁ κ u t x = deriv (fun (s : ℝ) => u s x) t + Homogenization.vecDot (b₀ t x) (spaceGrad (u t) x) - vecDiv (fun (y : Homogenization.Vec 2) => (κ • 1 + ψ y • sigmaMat).mulVec (spaceGrad (u t) y)) x

If the velocity increment is the perpendicular gradient of a scalar potential, the operator splits into old-scale transport and the exact divergence-form diffusion used in Section 5.1.