High-contrast homogenization: Entry.Response.Core.OptimizerMeanIdentity

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

The optimizer-mean identity

This file proves the optimizer-mean identity for adapted cells: the cell average of the doubled optimizer field equals the block response mean. It develops the shear-state congruence that carries the coarse block matrix to its skew-corrected form, the corresponding identities for the sheared block-matrix-vector product and the block energy density, and shows the shear preserves the admissible class of Radon measures. It also shows that multiplying a skew matrix into a vector field produces a solenoidal field with zero normal trace, which is what lets the shear be absorbed into the cell average without changing it. This is the pathwise optimizer-mean identity and skew-shear congruence used in the proof of p.response.transfer.

HC bridge I, part 3 of 4: the optimizer-mean identity, STEPs 1-3

theorem HCPolySupport.HighContrast.Multiscale.vecDot_matVecMul_swap_aux {d : ℕ} (M N : Mat d) (hMN : ∀ (i j : Fin d), M i j = N j i) (x y : Vec d) : vecDot x (matVecMul M y) = vecDot y (matVecMul N x)

AUX (helper, NEW). Transposed-pair bilinear swap.

theorem HCPolySupport.HighContrast.Multiscale.blockMatVecMul_blockSwap_fst {d : ℕ} (Y : BlockVec d) : (blockMatVecMul (blockSwap d) Y).1 = Y.2

AUX (helper, NEW).

theorem HCPolySupport.HighContrast.Multiscale.blockMatVecMul_blockSwap_snd {d : ℕ} (Y : BlockVec d) : (blockMatVecMul (blockSwap d) Y).2 = Y.1

AUX (helper, NEW).

theorem HCPolySupport.HighContrast.Multiscale.cellAverage_optimizerField_eq_blockResponseMean {d : ℕ} [NeZero d] (q : Mat d) (hq : IsUnit q) (t : ℤ) {lam Lam : ℝ} {b : CoeffField d} (hb : IsEllipticFieldOn lam Lam (adaptedCell q t) b) (p r : Vec d) (u : AHarmonicFunction b (adaptedCell q t)) (hu : IsResponseMaximizer (adaptedCell q t) p r b u) : cellAverage (adaptedCell q t) (optimizerField b u) = blockResponseMean (coarseBlockMatrix (adaptedCell q t) b) (-p, r)

Pathwise (2.32) on an adapted cell, for any elliptic coefficient field b and any response maximizer u: the cell average of the doubled optimizer field is x + R A(U) x, x = (-p, r), with A(U) the set-level coarse block matrix.

theorem HCPolySupport.HighContrast.Multiscale.blockCongr_shear {d : ℕ} (c : Mat d) (B : BlockMat d) : blockCongr { upperLeft := 1, upperRight := 0, lowerLeft := c, lowerRight := 1 } B = { upperLeft := B.upperLeft + matTranspose c * B.lowerLeft + B.upperRight * c + matTranspose c * B.lowerRight * c, upperRight := B.upperRight + matTranspose c * B.lowerRight, lowerLeft := B.lowerLeft + B.lowerRight * c, lowerRight := B.lowerRight }

STEP 1: the pointwise matrix identity

theorem HCPolySupport.HighContrast.Multiscale.symmPart_sub_skew {d : ℕ} {g : Mat d} (hg : matTranspose g = -g) (A : Mat d) : symmPart (A - g) = symmPart A

theorem HCPolySupport.HighContrast.Multiscale.skewPart_sub_skew {d : ℕ} {g : Mat d} (hg : matTranspose g = -g) (A : Mat d) : skewPart (A - g) = skewPart A - g

theorem HCPolySupport.HighContrast.Multiscale.blockMatrixOfCoeff_sub_skew {d : ℕ} {g : Mat d} (hg : matTranspose g = -g) (A : Mat d) : blockMatrixOfCoeff (A - g) = blockCongr { upperLeft := 1, upperRight := 0, lowerLeft := g, lowerRight := 1 } (blockMatrixOfCoeff A)

STEP 1. Subtracting a constant skew matrix from the coefficient is the shear congruence of the pointwise block matrix.

STEP 2: the analytic input

theorem HCPolySupport.HighContrast.Multiscale.memVectorL2_matVecMul_const {d : ℕ} {U : Set (Vec d)} (g : Mat d) {w : Vec d → Vec d} (hw : MemVectorL2 U w) : MemVectorL2 U fun (x : Vec d) => matVecMul g (w x)

L² closure under a constant matrix.

theorem HCPolySupport.HighContrast.Multiscale.isSolenoidalZeroNormalTraceOn_matVecMul_of_skew {d : ℕ} {U : Set (Vec d)} {g : Mat d} (hg : matTranspose g = -g) {w : Vec d → Vec d} (hw : IsPotentialZeroTraceOn U w) : IsSolenoidalZeroNormalTraceOn U fun (x : Vec d) => matVecMul g (w x)

g ∇u is divergence free with vanishing normal trace whenever g is a constant skew matrix and u ∈ H¹₀(U). For u ∈ C_c^∞(U) and any φ ∈ H¹(U) one has ∫_U g ∇u · ∇φ = -∫_U (Σ_{i,j} g_{ij} ∂_i∂_j u) φ = 0 because the Hessian is symmetric and g is skew; the general u ∈ H¹₀(U) follows by density. This is needed for the admissible-class shear of STEP 3 (the flux correction of a sheared state acquires the term g·(X.potential − P.1), which must itself be solenoidal with zero normal trace), and it is the ONLY genuinely analytic input of the admissible-class shear: every other step is matrix algebra, sInf congruence, or linearity of the integral.

STEP 3: the admissible-class shear

theorem HCPolySupport.HighContrast.Multiscale.blockMatVecMul_shear {d : ℕ} (g : Mat d) (P : BlockVec d) : blockMatVecMul { upperLeft := 1, upperRight := 0, lowerLeft := g, lowerRight := 1 } P = (P.1, matVecMul g P.1 + P.2)

theorem HCPolySupport.HighContrast.Multiscale.blockMatVecMul_shear_neg {d : ℕ} (g : Mat d) (P : BlockVec d) : blockMatVecMul { upperLeft := 1, upperRight := 0, lowerLeft := -g, lowerRight := 1 } (blockMatVecMul { upperLeft := 1, upperRight := 0, lowerLeft := g, lowerRight := 1 } P) = P

def HCPolySupport.HighContrast.Multiscale.shearState {d : ℕ} (g : Mat d) (X : BlockState d) : BlockState d

The state shear: the potential slot is untouched, the flux acquires g · potential.

Equations

• HCPolySupport.HighContrast.Multiscale.shearState g X = { potential := X.potential, flux := fun (x : HCPolySupport.Vec d) => HCPolySupport.matVecMul g (X.potential x) + X.flux x }

@[simp]

theorem HCPolySupport.HighContrast.Multiscale.shearState_eval {d : ℕ} (g : Mat d) (X : BlockState d) (x : Vec d) : (shearState g X).eval x = blockMatVecMul { upperLeft := 1, upperRight := 0, lowerLeft := g, lowerRight := 1 } (X.eval x)

theorem HCPolySupport.HighContrast.Multiscale.shearState_neg_shearState {d : ℕ} (g : Mat d) (X : BlockState d) : shearState (-g) (shearState g X) = X

theorem HCPolySupport.HighContrast.Multiscale.blockEnergyDensity_sub_skew {d : ℕ} {g : Mat d} (hg : matTranspose g = -g) (a : CoeffField d) (X : BlockState d) (x : Vec d) : blockEnergyDensity (fun (y : Vec d) => a y - g) X x = blockEnergyDensity a (shearState g X) x

STEP 1, transported to the energy density.

theorem HCPolySupport.HighContrast.Multiscale.isBlockMuAdmissible_shearState {d : ℕ} {g : Mat d} (hg : matTranspose g = -g) {U : Set (Vec d)} {P : BlockVec d} {X : BlockState d} (hX : IsBlockMuAdmissible U P X) : IsBlockMuAdmissible U (blockMatVecMul { upperLeft := 1, upperRight := 0, lowerLeft := g, lowerRight := 1 } P) (shearState g X)

theorem HCPolySupport.HighContrast.Multiscale.muValueSet_sub_skew {d : ℕ} {g : Mat d} (hg : matTranspose g = -g) (U : Set (Vec d)) (P : BlockVec d) (a : CoeffField d) : (muValueSet U P fun (x : Vec d) => a x - g) = muValueSet U (blockMatVecMul { upperLeft := 1, upperRight := 0, lowerLeft := g, lowerRight := 1 } P) a

STEP 3. The shear bijection on admissible states identifies the two mu-value sets.

theorem HCPolySupport.HighContrast.Multiscale.Mu_sub_skew {d : ℕ} {g : Mat d} (hg : matTranspose g = -g) (U : Set (Vec d)) (P : BlockVec d) (a : CoeffField d) : (Mu U P fun (x : Vec d) => a x - g) = Mu U (blockMatVecMul { upperLeft := 1, upperRight := 0, lowerLeft := g, lowerRight := 1 } P) a

STEP 3, conclusion: the shear identity for Mu.

STEP 4: the block-level shear