Public statement.
noncomputable def
AVenhance.vecDiv
(V : Homogenization.Vec 2 → Homogenization.Vec 2)
(x : Homogenization.Vec 2)
:
Classical divergence ∇ · V = ∑ᵢ ∂ᵢ Vᵢ of a vector field on ℝ² (∇· in e.Tm, e.Gm,
e.H.mr.def, e.dm). spaceGrad is the classical gradient.
Equations
- AVenhance.vecDiv V x = ∑ i : Fin 2, AVenhance.spaceGrad (fun (y : Homogenization.Vec 2) => V y i) x i