High-contrast homogenization: Provider.PolynomialHomogenization.Root.Duality.NegSobolevTranslation

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

Translation invariance of the normalized fractional norms

The gauge image of an adapted-cell witness is a triadic cube translated by an arbitrary real vector, so the cube-side estimate has to be moved by a translation that is not a lattice translation. Every norm entering the negative fractional dual is translation invariant; this file records that, for hsNormSq, fracSeminormSq, the dual pairing, and negSobolevNorm.

theorem HCPolySupport.HighContrast.RowSupply.fracSeminormSq_translateSet {d : ℕ} (z : Vec d) (V : Set (Vec d)) (s : ℝ) (F : Vec d → Vec d) : (fracSeminormSq (translateSet z V) s fun (x : Vec d) => F (x - z)) = fracSeminormSq V s F

The fractional seminorm square is translation invariant.

theorem HCPolySupport.HighContrast.RowSupply.hsNormSq_translateSet {d : ℕ} (z : Vec d) (V : Set (Vec d)) (s : ℝ) (F : Vec d → Vec d) : (hsNormSq (translateSet z V) s fun (x : Vec d) => F (x - z)) = hsNormSq V s F

The normalized H^s norm square is translation invariant.

theorem HCPolySupport.HighContrast.RowSupply.IsLocalVecTest.translate {d : ℕ} {V : Set (Vec d)} {psi : Vec d → Vec d} (h : IsLocalVecTest V psi) (z : Vec d) : IsLocalVecTest (translateSet z V) fun (x : Vec d) => psi (x - z)

A local vector test translates.

theorem HCPolySupport.HighContrast.RowSupply.dualPairing_translateSet {d : ℕ} (z : Vec d) (V : Set (Vec d)) (F psi : Vec d → Vec d) : (dualPairing (translateSet z V) (fun (x : Vec d) => F (x - z)) fun (x : Vec d) => psi (x - z)) = dualPairing V F psi

The dual pairing is translation invariant.

theorem HCPolySupport.HighContrast.RowSupply.negSobolevNorm_translateSet_le {d : ℕ} (z : Vec d) (V : Set (Vec d)) (s : ℝ) (F : Vec d → Vec d) : (negSobolevNorm (translateSet z V) s fun (x : Vec d) => F (x - z)) ≤ negSobolevNorm V s F

One direction of the translation invariance of the dual fractional norm.

theorem HCPolySupport.HighContrast.RowSupply.negSobolevNorm_translateSet {d : ℕ} (z : Vec d) (V : Set (Vec d)) (s : ℝ) (F : Vec d → Vec d) : (negSobolevNorm (translateSet z V) s fun (x : Vec d) => F (x - z)) = negSobolevNorm V s F

The dual fractional norm is translation invariant.