Statement file: gradMatrix (Section3).
This file contains exactly one declaration of the formalization's public statement surface.
noncomputable def
AVenhance.gradMatrix
(Χ : Homogenization.Vec 2 → Homogenization.Vec 2)
(x : Homogenization.Vec 2)
:
∇Χ for Χ = (χ_{e₁}, χ_{e₂}) (e.gradcorrmatrix, label 2819): the entry (i, j) is
∂_{x_i} χ_{e_j}.
Equations
- AVenhance.gradMatrix Χ x = Matrix.of fun (i j : Fin 2) => AVenhance.spaceGrad (fun (y : Homogenization.Vec 2) => Χ y j) x i