PrincipalResponseGauge

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

Provider: the constant-skew gauge shear and its coarse block covariance

Source displays in ABK26:

• e.Gh.def defines, for a matrix h, the doubled shear bfG_h = [[Id, 0], [h, Id]];
• e.Gh.additive records bfG_{h1 + h2} = bfG_{h1} bfG_{h2}, hence bfG_h^{-1} = bfG_{-h};
• e.bfA.LDLt writes the doubled matrix as bfA = bfG_{-kappa}^t diag(sigma, sigma^{-1}) bfG_{-kappa}, so that a shift of the coupling matrix kappa is a conjugation by a shear.

The one place in Section 3.4 where these are used at full strength is the first equality of Step 3 of l.approximate.recurrence.formula: with hbar the average of the fresh shell k_m - k_{m-h} over the localization cube z + cu_n,

P_z . bfA_m(z + cu_n) P_z
  = bfG_{-hbar} P_z . bfA(z + cu_n; a_m - hbar) bfG_{-hbar} P_z .

What this module proves, and at which carrier

The manuscript's identity is read here at the coarse matrix package carrier Homogenization.Book.Ch02.CoarseMatrices, i.e. at the triple (sigma, sigmaStarInv, kappa) out of which Homogenization.Book.Ch02.blockMatrixOfCoarseMatrices assembles bfA. At that carrier the statement is an unconditional algebraic identity (blockVecDot_blockMatrixOfCoarseMatrices_gaugeShift): shifting kappa by -h and shearing the load by bfG_{-h} leaves the doubled quadratic form unchanged. Skew-symmetry of h is not needed for it and is therefore not assumed.

What this module does NOT prove

It does not prove the manuscript's identity at the coefficient field carrier, because that requires the coarse-graining to intertwine with a constant skew shift of the field, namely

Homogenization.Book.Ch02.coarseMatrices U (a - hbar)
  = gaugeShiftCoarseMatrices hbar (Homogenization.Book.Ch02.coarseMatrices U a)

for constant skew hbar -- equivalently sigmaCoarse and sigmaStarInvCoarse are unchanged and kappaCoarse drops by hbar. That statement is about the variational definition of the coarse matrices, not about block algebra. Nothing here asserts it, and no declaration in this file takes it as a hypothesis.

Update: that obligation is now discharged. The sentence above originally said the statement "is not available in this tree", which is no longer true. ApproximateRecurrence.CoarseGaugeCoarseMatrices proves it unconditionally, for every Domain and CoeffOn of CoarseGraining's Chapter 2 carrier and every constant skew hbar, as coarseMatrices_sub_const_skew and its hypothesis-free form coarseMatrices_perturbConstCoeffOn. The coefficient-field reading is blockVecDot_coarseBlockMatrix_sub_const_skew there. This file remains the block-algebra half only.

The doubled shear bfG_h

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.blockGauge {d : ℕ} (h : HCPolySupport.Mat d) : HCPolySupport.BlockMat d

e.Gh.def: the doubled shear bfG_h = [[Id, 0], [h, Id]].

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.blockGauge h = { upperLeft := 1, upperRight := 0, lowerLeft := h, lowerRight := 1 }

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.blockMatVecMul_blockGauge {d : ℕ} (h : HCPolySupport.Mat d) (X : HCPolySupport.BlockVec d) : HCPolySupport.blockMatVecMul (blockGauge h) X = (X.1, HCPolySupport.matVecMul h X.1 + X.2)

The shear acts on a doubled load by adding h applied to the first slot into the second slot.

The coarse quadratic form and its shift covariance

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.gaugeShiftCoarseMatrices {d : ℕ} (h : HCPolySupport.Mat d) (M : HCPolySupport.Book.Ch02.CoarseMatrices d) : HCPolySupport.Book.Ch02.CoarseMatrices d

The coarse package obtained by dropping the coupling matrix kappa by h, leaving sigma and sigmaStarInv untouched.

This is the coarse-matrix shadow of the field shift a |-> a - h used: for a constant skew h the manuscript's bfA(U; a - h) is assembled from the same sigma and sigmaStar and from kappa - h.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.gaugeShiftCoarseMatrices h M = { sigma := M.sigma, sigmaStarInv := M.sigmaStarInv, kappa := M.kappa - h }

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.blockVecDot_blockMatrixOfCoarseMatrices_gaugeShift {d : ℕ} (h : HCPolySupport.Mat d) (M : HCPolySupport.Book.Ch02.CoarseMatrices d) (X : HCPolySupport.BlockVec d) : HCPolySupport.blockVecDot (HCPolySupport.blockMatVecMul (blockGauge (-h)) X) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.blockMatrixOfCoarseMatrices (gaugeShiftCoarseMatrices h M)) (HCPolySupport.blockMatVecMul (blockGauge (-h)) X)) = HCPolySupport.blockVecDot X (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.blockMatrixOfCoarseMatrices M) X)

Gauge covariance of the doubled coarse quadratic form, in the direction and shape of the first equality: shearing the load by bfG_{-h} exactly compensates dropping the coupling matrix by h.

Unconditional: no skew-symmetry, symmetry, or invertibility hypothesis is used. This is the block-algebra half only; see the module docstring for the coarse-graining half, which is not proved here.