Coarse-graining support: Support.Probability.LocalEllipticitySlices.SymmetricL2 #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
theorem
HCPolySupport.IsAEEllipticFieldOn.memVectorL2_matVecMul_symmPart
{d : ℕ}
{lam Lam : ℝ}
{U : Set (Vec d)}
{a : CoeffField d}
(h : IsAEEllipticFieldOn lam Lam U a)
{f : Vec d → Vec d}
(hf : MemVectorL2 U f)
:
MemVectorL2 U fun (x : Vec d) => matVecMul (symmPart (a x)) (f x)
Spatial a.e. ellipticity sends L² vector fields to L² vector fields after
multiplication by the symmetric part of the coefficient matrix.