High-contrast homogenization: Provider.PolynomialHomogenization.Root.CorrectorDecay.NegOneTriangle

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

theorem HCPolySupport.HighContrast.negOneNorm_add_le_of_memVectorL2 {d : ℕ} {V : Set (Vec d)} (F G : Vec d → Vec d) (hF : MemVectorL2 V F) (hG : MemVectorL2 V G) : (negOneNorm V fun (x : Vec d) => F x + G x) ≤ negOneNorm V F + negOneNorm V G

The fail-closed normalized negative-one norm is subadditive on local square-integrable vector fields.

theorem HCPolySupport.HighContrast.localNegOneNorm_add_le {d : ℕ} {V : Set (Vec d)} (F G : ↥(HilbertVectorL2 V)) : localNegOneNorm V (F + G) ≤ localNegOneNorm V F + localNegOneNorm V G

Subadditivity descends to the quotient-safe local Hilbert-vector class.

theorem HCPolySupport.HighContrast.triadicScaledNegOneNorm_add_le {d : ℕ} (n : ℤ) (F G : ↥(HilbertVectorL2 (openCubeSet (originCube d n)))) : triadicScaledNegOneNorm n (F + G) ≤ triadicScaledNegOneNorm n F + triadicScaledNegOneNorm n G

The inverse-side-length normalized negative-one norm is subadditive.