High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.C1WeightedEnergyTriangle

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

Triangle inequalities for normalized coefficient energy

On a centered cube, the public weighted gradient norm is the real square root of the positive symmetric coefficient form. This gives the triangle and sign identities needed to combine two comparison errors.

theorem HCPolySupport.HighContrast.Root.weightedGradNorm_sub_comm_h1 {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (q : ℤ) (u v : H1Function (openCubeSet (originCube d q))) : (weightedGradNorm (a.coeffOn (originCube d q)).toCoeffField (openCubeSet (originCube d q)) fun (x : Vec d) => u.grad x - v.grad x) = weightedGradNorm (a.coeffOn (originCube d q)).toCoeffField (openCubeSet (originCube d q)) fun (x : Vec d) => v.grad x - u.grad x

The normalized coefficient-energy norm of one difference is invariant under reversing the two fields.

theorem HCPolySupport.HighContrast.Root.weightedGradNorm_sub_le_add_sub_h1 {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (q : ℤ) (u v w : H1Function (openCubeSet (originCube d q))) : (weightedGradNorm (a.coeffOn (originCube d q)).toCoeffField (openCubeSet (originCube d q)) fun (x : Vec d) => u.grad x - w.grad x) ≤ (weightedGradNorm (a.coeffOn (originCube d q)).toCoeffField (openCubeSet (originCube d q)) fun (x : Vec d) => u.grad x - v.grad x) + weightedGradNorm (a.coeffOn (originCube d q)).toCoeffField (openCubeSet (originCube d q)) fun (x : Vec d) => v.grad x - w.grad x

The normalized coefficient-energy norm obeys the triangle inequality along three local Sobolev fields.