PrincipalResponseSensitivityAlgebra

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

Provider: e.J.by.means.of.bfA on a gauge-sheared doubled load

Source displays in ABK26:

• e.J.by.means.of.bfA (label; display):

  J(U, p, q; a) = 1/2 (p; -q) . bfA(U; a) (p; -q) - p . q ,
  

• the opening two equalities of Step 3 of l.approximate.recurrence.formula: with hbar = (h)_{z+cu_n} the averaged fresh shell,

  P_z . bfA_m(z+cu_n) P_z 1_{Q_z}
    = bfG_{-hbar} P_z . bfA(z+cu_n; a_m - hbar) bfG_{-hbar} P_z 1_{Q_z}
    = ( 2 J(z+cu_n, -p_z, q_z - hbar p_z; a_m - hbar) - 2 p_z . q_z ) 1_{Q_z} .
  

The first equality is blockVecDot_coarseBlockMatrix_sub_const_skew of ApproximateRecurrence.CoarseGaugeCoarseMatrices, already proved. This module supplies the second one, and the composite of the two.

The second equality

With Y = bfG_{-hbar} P_z = (p_z; q_z - hbar p_z), e.J.by.means.of.bfA at the load (p, q) = (-p_z, q_z - hbar p_z) gives

J(U, -p_z, q_z - hbar p_z; c)
  = 1/2 Y . bfA(U; c) Y - (-p_z) . (q_z - hbar p_z)
  = 1/2 Y . bfA(U; c) Y + p_z . q_z ,

the last step because hbar is skew, so p_z . hbar p_z = 0. Hence

Y . bfA(U; c) Y = 2 J(U, -p_z, q_z - hbar p_z; c) - 2 p_z . q_z ,

which is the second equality above.

Carrier and hypotheses

Everything is stated for an arbitrary Homogenization.Book.Ch02.Domain and arbitrary CoeffOn objects; the localization cube, the fresh shell and the good event do not appear. The only hypotheses are the two source premises: hbar is a constant antisymmetric matrix (it is an average of antisymmetric shell increments -- see ApproximateRecurrence.PrincipalResponseShellAverage), and b represents the shifted field a - hbar. No proof step is carried as a hypothesis.

Consistency check

Composing blockVecDot_coarseBlockMatrix_eq_two_responseJ_sub_const_skew with responseJ_neg_sub_matVecMul_eq_of_sub_const_skew returns blockVecDot_coarseBlockMatrix_eq_two_responseJ_sub at the unshifted field: the gauge shear and the field shift cancel, exactly as they must.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.blockVecDot_coarseBlockMatrix_eq_two_responseJ_sub {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (c : HCPolySupport.Book.Ch02.CoeffOn U) (X : HCPolySupport.BlockVec d) : HCPolySupport.blockVecDot X (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.coarseBlockMatrix U c) X) = 2 * HCPolySupport.Book.Ch02.responseJ U c (-X.1) X.2 - 2 * HCPolySupport.vecDot X.1 X.2

e.J.by.means.of.bfA on a doubled load. For every coefficient object and every doubled load X,

X . bfA(U; c) X = 2 J(U, -X_1, X_2; c) - 2 X_1 . X_2 .

This is CoarseGraining's responseJ_eq_block_quadratic solved for the quadratic form.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.blockVecDot_coarseBlockMatrix_blockGauge_eq_two_responseJ_sub {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (c : HCPolySupport.Book.Ch02.CoeffOn U) {hbar : HCPolySupport.Mat d} (hskew : HCPolySupport.matTranspose hbar = -hbar) (X : HCPolySupport.BlockVec d) : HCPolySupport.blockVecDot (HCPolySupport.blockMatVecMul (blockGauge (-hbar)) X) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.coarseBlockMatrix U c) (HCPolySupport.blockMatVecMul (blockGauge (-hbar)) X)) = 2 * HCPolySupport.Book.Ch02.responseJ U c (-X.1) (X.2 - HCPolySupport.matVecMul hbar X.1) - 2 * HCPolySupport.vecDot X.1 X.2

ABK26 (see the module docstring). The doubled quadratic form at the gauge-sheared load bfG_{-hbar} X is twice the response at the sheared arguments, minus twice the unsheared pairing X_1 . X_2 -- the shear does not change the pairing because hbar is skew.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.blockVecDot_coarseBlockMatrix_eq_two_responseJ_sub_const_skew {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} {a b : HCPolySupport.Book.Ch02.CoeffOn U} {hbar : HCPolySupport.Mat d} (hskew : HCPolySupport.matTranspose hbar = -hbar) (hab : ∀ (x : HCPolySupport.Vec d), b.toCoeffField x = a.toCoeffField x - hbar) (X : HCPolySupport.BlockVec d) : HCPolySupport.blockVecDot X (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.coarseBlockMatrix U a) X) = 2 * HCPolySupport.Book.Ch02.responseJ U b (-X.1) (X.2 - HCPolySupport.matVecMul hbar X.1) - 2 * HCPolySupport.vecDot X.1 X.2

ABK26 in one line. The two opening equalities of Step 3, composed: the unsheared quadratic form of the unshifted field equals twice the response of the shifted field at the sheared arguments, minus twice the pairing.