Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Section5.OperatorSplit

Exact algebraic splitting of the Section 5 advection-diffusion operator.

theorem AVenhance.Infra.Section5.advDiffOp_split {b₀ b₁ : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {t : ℝ} {x : Homogenization.Vec 2} :
advDiffOp b₁ κ u t x = deriv (fun (s : ℝ) => u s x) t + Homogenization.vecDot (b₀ t x) (spaceGrad (u t) x) + (-κ * spaceLap (u t) x + Homogenization.vecDot (b₁ t x - b₀ t x) (spaceGrad (u t) x))

Split the new-scale operator into old-scale transport and the velocity increment.