High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Corrector.PushforwardGaugeTranslation

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

The real-vector gauge conjugation

An integer translation of the physical sample becomes, in the normalized gauge, a translation by the real vector L⁻¹ z. This is the identity the translated-gradient identification engine has to be fed at, and it is the piece that was not otherwise available: the integer conjugation requires the matrix to carry ℤ^d into ℤ^d, which the normalized root does not.

The route is elementary once the pieces are separated: the recentring and the rescaling commute with the integer translation (both already available), and the affine change of variables converts a translation by w on the physical side into a translation by L⁻¹ w on the normalized side, pointwise.

Rescaling commutes with the integer translation

theorem HCPolySupport.HighContrast.Root.translateCoeff_positiveScale_comm {d : ℕ} (z : Fin d → ℤ) (a : CoeffSpace d) (c : ℝ) (hc : 0 < c) : translateCoeff z (CoeffSpace.positiveScale c hc a) = CoeffSpace.positiveScale c hc (translateCoeff z a)

Positive scalar multiplication commutes with integer translation.

theorem HCPolySupport.HighContrast.Root.translateCoeff_normalizedCenteredCoeff {d : ℕ} [NeZero d] (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (z : Fin d → ℤ) : normalizedCenteredCoeff (translateCoeff z a) abar hS = translateCoeff z (normalizedCenteredCoeff a abar hS)

The normalized recentring commutes with the integer translation.

The affine change of variables converts the translation

theorem HCPolySupport.HighContrast.Root.affineCoefficient_translate_apply {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (c : CoeffField d) (w y : Vec d) : affineCoefficient (gaugeRoot abar) ⋯ (fun (x : Vec d) => c (x + w)) y = affineCoefficient (gaugeRoot abar) ⋯ c (y + matVecMul (gaugeRoot abar)⁻¹ w)

P3, pointwise. Translating the argument of a coefficient field by w before the affine pullback is translating the pullback by L⁻¹ w.

The gauge conjugation

theorem HCPolySupport.HighContrast.Root.gaugeCoeff_translateCoeff_ae {d : ℕ} [NeZero d] (a : CoeffSpace d) (abar : Mat d) (hS : Matrix.PosDef (symmPart abar)) (z : Fin d → ℤ) : gaugeCoeff (translateCoeff z a) abar hS =ᵐ[MeasureTheory.volume] fun (y : Vec d) => gaugeCoeff a abar hS (y + matVecMul (gaugeRoot abar)⁻¹ (Source.AKL.intTranslation z))

The real-vector gauge conjugation. An integer translation of the physical sample is, in the normalized gauge, the translation by matVecMul (gaugeRoot abar)⁻¹ (Source.AKL.intTranslation z) — a real vector, which is exactly what the identification engine's free translation binder accepts.