CoarseGaugeCoeffField

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Provider: constant skew shifts of a coefficient field

Step 3 of l.approximate.recurrence.formula (ABK26) shifts the coefficient field by the constant matrix hbar, the average of the fresh shell k_m - k_{m-h} over the localization cube, and compensates by the doubled shear bfG_{-hbar} of e.Gh.def. The matrix hbar is skew because it is an average of skew matrices.

This module supplies the pointwise half of that shift, at the carrier of Homogenization.Ambient.CoefficientField:

• the two elementary consequences of skewness, x . h x = 0 and x . h y = - (h x) . y;
• invariance of the symmetric part, symmPart (A - h) = symmPart A, together with its additive form.

Only linear algebra occurs here: neither the ellipticity transfer for the shifted matrix nor the packaging of a - hbar as an object of Homogenization.Book.Ch02.CoeffOn is carried out in this module.

Elementary consequences of skewness

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.vecDot_matVecMul_swap_of_transpose_eq_neg {d : ℕ} {H : HCPolySupport.Mat d} (hH : HCPolySupport.matTranspose H = -H) (x y : HCPolySupport.Vec d) : HCPolySupport.vecDot x (HCPolySupport.matVecMul H y) = -HCPolySupport.vecDot (HCPolySupport.matVecMul H x) y

Pairing across a skew matrix is antisymmetric.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.vecDot_matVecMul_self_eq_zero_of_transpose_eq_neg {d : ℕ} {H : HCPolySupport.Mat d} (hH : HCPolySupport.matTranspose H = -H) (x : HCPolySupport.Vec d) : HCPolySupport.vecDot x (HCPolySupport.matVecMul H x) = 0

The quadratic form of a skew matrix vanishes.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.vecDot_sub_left {d : ℕ} (x y z : HCPolySupport.Vec d) : HCPolySupport.vecDot (x - y) z = HCPolySupport.vecDot x z - HCPolySupport.vecDot y z

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.vecDot_sub_right {d : ℕ} (x y z : HCPolySupport.Vec d) : HCPolySupport.vecDot x (y - z) = HCPolySupport.vecDot x y - HCPolySupport.vecDot x z

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.matTranspose_neg {d : ℕ} (H : HCPolySupport.Mat d) : HCPolySupport.matTranspose (-H) = -HCPolySupport.matTranspose H

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.symmPart_add_of_transpose_eq_neg {d : ℕ} {H : HCPolySupport.Mat d} (hH : HCPolySupport.matTranspose H = -H) (A : HCPolySupport.Mat d) : HCPolySupport.symmPart (A + H) = HCPolySupport.symmPart A

A constant skew summand does not change the symmetric part.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.symmPart_sub_of_transpose_eq_neg {d : ℕ} {H : HCPolySupport.Mat d} (hH : HCPolySupport.matTranspose H = -H) (A : HCPolySupport.Mat d) : HCPolySupport.symmPart (A - H) = HCPolySupport.symmPart A

A constant skew subtrahend does not change the symmetric part.