High-contrast homogenization:

Provider.PolynomialHomogenization.Root.RowSupply.RealTranslationCoeffSpace

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

Real translations of qualitative coefficient samples

The stochastic action uses integer translations, but deterministic response covariance also needs translation by an arbitrary vector. This module packages that deterministic operation without attaching any stationarity claim to it.

noncomputable def HCPolySupport.HighContrast.RowSupply.realTranslateCoeff {d : ℕ} (z : Vec d) (a : CoeffSpace d) : CoeffSpace d

Translation of a coefficient sample by an arbitrary vector.

Equations

• HCPolySupport.HighContrast.RowSupply.realTranslateCoeff z a = ⟨MeasureTheory.AEEqFun.compMeasurePreserving (↑a) (fun (x : HCPolySupport.Vec d) => x + z) ⋯, ⋯⟩

theorem HCPolySupport.HighContrast.RowSupply.realTranslateCoeff_ae {d : ℕ} (z : Vec d) (a : CoeffSpace d) : ↑↑(realTranslateCoeff z a) =ᵐ[MeasureTheory.volume] fun (x : Vec d) => ↑↑a (x + z)

The real translation has the expected representative almost everywhere.

theorem HCPolySupport.HighContrast.RowSupply.affineCoefficient_congr_ae_global {d : ℕ} (L : Mat d) (hL : IsUnit (Matrix.det L)) {a b : CoeffField d} (hab : a =ᵐ[MeasureTheory.volume] b) : affineCoefficient L hL a =ᵐ[MeasureTheory.volume] affineCoefficient L hL b

Affine pullback commutes with replacing a coefficient representative by an almost-everywhere equal one.

theorem HCPolySupport.HighContrast.RowSupply.affineTranslatedCenteredCoeff_congr_ae {d : ℕ} (L : Mat d) (hL : IsUnit (Matrix.det L)) (b : Mat d) {u v : CoeffField d} (huv : u =ᵐ[MeasureTheory.volume] v) (c : Vec d) (V : Set (Vec d)) : (fun (y : Vec d) => affineCoefficient L hL (fun (w : Vec d) => u w - b) (y + c)) =ᵐ[volumeMeasureOn V] fun (y : Vec d) => affineCoefficient L hL (fun (w : Vec d) => v w - b) (y + c)

Skew-centring, the affine gauge, and translation by a fixed vector all respect replacing a coefficient representative by an almost-everywhere equal one, on any set. Every residual-frame provider performs exactly this transport, so it is stated once here.