High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Duality.GaugeCubeTranslationReduction

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

Moving the gauge-cube Hodge hypothesis off the translation

The gauge image of an adapted-cell witness is a triadic cube translated by an arbitrary real vector. Every ingredient of the Hodge hypothesis — the two Hodge predicates, vector L² membership, and the negative fractional norm — is translation invariant, so the hypothesis at the translated cube follows from the same hypothesis at the cube itself, with the same constant.

theorem HCPolySupport.HighContrast.RowSupply.memVectorL2_translateSet {d : ℕ} {S : Set (Vec d)} {F : Vec d → Vec d} (z : Vec d) (hF : MemVectorL2 (translateSet z S) F) : MemVectorL2 S fun (y : Vec d) => F (y + z)

Vector L² membership pulls back along a translation.

theorem HCPolySupport.HighContrast.RowSupply.gaugeHodgeHypothesis_translateSet {d : ℕ} (z : Vec d) (S : Set (Vec d)) (A : Mat d) {s C : ℝ} (hbase : ∀ (w F : Vec d → Vec d), MemVectorL2 S F → IsPotentialZeroTraceOn S w → (IsSolenoidalOn S fun (y : Vec d) => matVecMul A (w y) + F y) → negSobolevNorm S s w ≤ ENNReal.ofReal C * negSobolevNorm S s F) (w F : Vec d → Vec d) : MemVectorL2 (translateSet z S) F → IsPotentialZeroTraceOn (translateSet z S) w → (IsSolenoidalOn (translateSet z S) fun (y : Vec d) => matVecMul A (w y) + F y) → negSobolevNorm (translateSet z S) s w ≤ ENNReal.ofReal C * negSobolevNorm (translateSet z S) s F

The gauge-cube Hodge hypothesis moves off an arbitrary translation.