High-contrast homogenization: Provider.Response.VariationalIdentities

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

The variational identities in block form

The weak-norm estimate for the optimizer state reads the Chapter 2 variational layer through a handful of displayed identities, all written on the doubled block state X(V) = (∇v, a∇v) of the maximizer and on the coarse block 𝐀(V;a). This file transcribes them.

• the self-duality of the diagonal metric M_0 = diag(m_0, m_0^{-1}): R M_0 R = M_0^{-1}, read here both multiplicatively and on the quadratic form, which is the only way the proof uses it.
• the average of the optimizer state, (X(V))_V = (R𝐀(V;a) + I_{2d})P of [Armstrong–Kuusi, (2.32)] in the normalization used by the paper, together with its difference form.
• the exact identity behind the comparison of the optimizer averages of two cells.
• the energy identity for the optimizer, J(V,p,q;a) = ½‖σ^{1/2}∇v‖²_{L_underlined²(V)} of [Armstrong–Kuusi, (2.30)], and
• the pointwise energy of the optimizer state, the substitution X_t·𝐀X_t = 2∇v_t·σ∇v_t into the block of [Armstrong–Kuusi, (2.8)], with its averaged form ‖𝐀^{1/2}X_t‖²_{L_underlined²} = 2ℰ_t², and
• the expansion of the response functional around its maximizer, the per-cell half of the exact factor-two response identity.

Everything is proved on an arbitrary Chapter 2 domain, which is where the Chapter 2 layer states it, and then specialized to the parent cell U_t = q□_t and to an aligned cell U_k(z) = z + q□_k through the bridge of HCPoly.Provider.Response.DomainBridge.

Elementary block arithmetic used by the identities

@[simp]

theorem HCPolySupport.HighContrast.Response.blockMatVecMul_blockR {d : ℕ} (X : BlockVec d) : blockMatVecMul (Book.Ch02.blockR d) X = (X.2, X.1)

The swap matrix R of s.scale.selection exchanges the two slots of a doubled vector.

theorem HCPolySupport.HighContrast.Response.blockReflect_blockDiag {d : ℕ} (A B : Mat d) : blockReflect (Book.Ch02.blockDiag A B) = Book.Ch02.blockDiag B A

The block reflection A ↦ RAR of the ambient layer exchanges the two diagonal entries of a block diagonal matrix.

theorem HCPolySupport.HighContrast.Response.blockMatMul_blockDiag {d : ℕ} (A B C E : Mat d) : Book.Ch02.blockMatMul (Book.Ch02.blockDiag A B) (Book.Ch02.blockDiag C E) = Book.Ch02.blockDiag (A * C) (B * E)

Block diagonal matrices multiply entrywise.

theorem HCPolySupport.HighContrast.Response.blockMatVecMul_blockSub {d : ℕ} (A B : BlockMat d) (X : BlockVec d) : blockMatVecMul (blockSub A B) X = blockMatVecMul A X - blockMatVecMul B X

The doubled matrix-vector product is additive in the matrix, in the difference form the defect 𝐀(V) - 𝐀(W) is written in.

theorem HCPolySupport.HighContrast.Response.blockVecDot_blockMatVecMul_blockReflect {d : ℕ} (A : BlockMat d) (X : BlockVec d) : blockVecDot X (blockMatVecMul (blockReflect A) X) = blockVecDot (blockMatVecMul (Book.Ch02.blockR d) X) (blockMatVecMul A (blockMatVecMul (Book.Ch02.blockR d) X))

The quadratic form of a block reflection is the quadratic form of the original at the reflected vector: X·(RAR)X = (RX)·A(RX).

The self-dual diagonal metric

theorem HCPolySupport.HighContrast.Response.blockMatMul_metric_blockReflect {d : ℕ} {m : Mat d} (hm : IsUnit (Matrix.det m)) : Book.Ch02.blockMatMul (Book.Ch02.blockDiag m m⁻¹) (blockReflect (Book.Ch02.blockDiag m m⁻¹)) = Book.Ch02.blockIdentity d

R M_0 R = M_0^{-1}, multiplicative form. The diagonal metric M_0 = diag(m_0, m_0^{-1}) and its block reflection are inverse to one another.

theorem HCPolySupport.HighContrast.Response.blockMatInv_metric_eq_blockReflect {d : ℕ} {m : Mat d} (hm : IsUnit (Matrix.det m)) : Book.Ch02.blockMatInv (Book.Ch02.blockDiag m m⁻¹) = blockReflect (Book.Ch02.blockDiag m m⁻¹)

R M_0 R = M_0^{-1}: the inverse of the diagonal metric is its block reflection.

theorem HCPolySupport.HighContrast.Response.metric_quadratic_blockR {d : ℕ} (m : Mat d) (Z : BlockVec d) : blockVecDot (blockMatVecMul (Book.Ch02.blockR d) Z) (blockMatVecMul (Book.Ch02.blockDiag m m⁻¹) (blockMatVecMul (Book.Ch02.blockR d) Z)) = blockVecDot Z (blockMatVecMul (blockReflect (Book.Ch02.blockDiag m m⁻¹)) Z)

M_0^{1/2} = R M_0^{-1/2} R on the quadratic form, which is the only reading the weak-norm estimate uses: |M_0^{1/2}(RZ)|² = |M_0^{-1/2}Z|², the right side being the quadratic form of M_0^{-1} = R M_0 R.

The optimizer average

theorem HCPolySupport.HighContrast.Response.blockAverage_eq {d : ℕ} {U : Book.Ch02.Domain d} (a : Book.Ch02.CoeffOn U) {p q : Vec d} {v : Book.Ch02.Solution U a} (hv : Book.Ch02.IsResponseMaximizer U a p q v) : (Book.Ch02.averageGradient U a v, Book.Ch02.averageFlux U a v) = blockMatVecMul (Book.Ch02.blockR d) (blockMatVecMul (Book.Ch02.coarseBlockMatrix U a) (-p, q)) + (-p, q)

The average identity (X(V))_V = (R𝐀(V;a) + I_{2d})P ([Armstrong–Kuusi, (2.32)]). Here X(V) = (∇v, a∇v) is the doubled state of the response maximizer, P is the load vector (-p, q), and the right side is written as R(𝐀P) + P because R acts by exchanging the two slots.

theorem HCPolySupport.HighContrast.Response.blockAverage_sub_eq {d : ℕ} {U W : Book.Ch02.Domain d} (a : Book.Ch02.CoeffOn U) (b : Book.Ch02.CoeffOn W) {p q : Vec d} {v : Book.Ch02.Solution U a} {w : Book.Ch02.Solution W b} (hv : Book.Ch02.IsResponseMaximizer U a p q v) (hw : Book.Ch02.IsResponseMaximizer W b p q w) : (Book.Ch02.averageGradient U a v, Book.Ch02.averageFlux U a v) - (Book.Ch02.averageGradient W b w, Book.Ch02.averageFlux W b w) = blockMatVecMul (Book.Ch02.blockR d) (blockMatVecMul (blockSub (Book.Ch02.coarseBlockMatrix U a) (Book.Ch02.coarseBlockMatrix W b)) (-p, q))

The difference of two optimizer averages: subtracting two instances of the average identity at the same load leaves R applied to the block defect.

theorem HCPolySupport.HighContrast.Response.metricNormSq_blockAverage_sub {d : ℕ} {U W : Book.Ch02.Domain d} (a : Book.Ch02.CoeffOn U) (b : Book.Ch02.CoeffOn W) {p q : Vec d} {v : Book.Ch02.Solution U a} {w : Book.Ch02.Solution W b} (m : Mat d) (hv : Book.Ch02.IsResponseMaximizer U a p q v) (hw : Book.Ch02.IsResponseMaximizer W b p q w) : blockVecDot ((Book.Ch02.averageGradient U a v, Book.Ch02.averageFlux U a v) - (Book.Ch02.averageGradient W b w, Book.Ch02.averageFlux W b w)) (blockMatVecMul (Book.Ch02.blockDiag m m⁻¹) ((Book.Ch02.averageGradient U a v, Book.Ch02.averageFlux U a v) - (Book.Ch02.averageGradient W b w, Book.Ch02.averageFlux W b w))) = blockVecDot (blockMatVecMul (blockSub (Book.Ch02.coarseBlockMatrix U a) (Book.Ch02.coarseBlockMatrix W b)) (-p, q)) (blockMatVecMul (blockReflect (Book.Ch02.blockDiag m m⁻¹)) (blockMatVecMul (blockSub (Book.Ch02.coarseBlockMatrix U a) (Book.Ch02.coarseBlockMatrix W b)) (-p, q)))

The exact comparison identity for the optimizer averages of two cells: |M_0^{1/2}((X(V))_V - (X(W))_W)|² = P·(𝐀(V) - 𝐀(W))M_0^{-1}(𝐀(V) - 𝐀(W))P, the right side being read through the self-duality M_0^{-1} = R M_0 R.

The two energy identities

theorem HCPolySupport.HighContrast.Response.responseJ_eq_energy {d : ℕ} {U : Book.Ch02.Domain d} (a : Book.Ch02.CoeffOn U) {p q : Vec d} {v : Book.Ch02.Solution U a} (hv : Book.Ch02.IsResponseMaximizer U a p q v) : Book.Ch02.responseJ U a p q = 1 / 2 * Book.Ch02.variationEnergyValue U a v

The maximizer energy identity ([Armstrong–Kuusi, (2.30)]): J(V,p,q;a) = ½‖σ^{1/2}∇v(·,V,p,q;a)‖²_{L_underlined²(V)}, the norm being the normalized one and variationEnergyValue being its square.

theorem HCPolySupport.HighContrast.Response.blockEnergy_gradient_flux_of_isUnit {d : ℕ} {A : Mat d} (hdet : IsUnit (Matrix.det (symmPart A))) (g : Vec d) : blockVecDot (g, matVecMul A g) (blockMatVecMul (blockMatrixOfCoeff A) (g, matVecMul A g)) = 2 * vecDot g (matVecMul (symmPart A) g)

The pointwise block energy of a gradient-flux pair, at a single point where the symmetric part of the coefficient is invertible: substituting X = (ξ, Aξ) into the pointwise block of [Armstrong–Kuusi, (2.8)] gives 2ξ·σξ. This is the algebraic core of the pointwise energy of the optimizer state.

theorem HCPolySupport.HighContrast.Response.pointwise_block_energy {d : ℕ} {U : Book.Ch02.Domain d} (a : Book.Ch02.CoeffOn U) (g : Vec d → Vec d) : ∀ᵐ (x : Vec d) ∂volumeMeasureOn U.carrier, blockVecDot (g x, matVecMul (a.toCoeffField x) (g x)) (blockMatVecMul (Book.Ch02.blockMatrixField a x) (g x, matVecMul (a.toCoeffField x) (g x))) = 2 * vecDot (g x) (matVecMul (symmPart (a.toCoeffField x)) (g x))

The pointwise energy substitution, the first of the two pointwise energy identities: X_t·𝐀X_t = 2∇v_t·σ∇v_t almost everywhere on the domain, for the doubled state X_t = (∇v_t, a∇v_t) of any field g and the pointwise block of [Armstrong–Kuusi, (2.8)].

theorem HCPolySupport.HighContrast.Response.average_block_energy_eq {d : ℕ} {U : Book.Ch02.Domain d} (a : Book.Ch02.CoeffOn U) (v : Book.Ch02.Solution U a) : (Book.Ch02.average U fun (x : Vec d) => blockVecDot (v.toH1.grad x, matVecMul (a.toCoeffField x) (v.toH1.grad x)) (blockMatVecMul (Book.Ch02.blockMatrixField a x) (v.toH1.grad x, matVecMul (a.toCoeffField x) (v.toH1.grad x)))) = 2 * Book.Ch02.variationEnergyValue U a v

The averaged energy identity, the second of the two pointwise energy identities: ‖𝐀^{1/2}X_t‖²_{L_underlined²(U_t)} = 2ℰ_t², with ℰ_t² = ‖σ^{1/2}∇v_t‖²_{L_underlined²(U_t)} the variationEnergyValue of the maximizer.

theorem HCPolySupport.HighContrast.Response.average_block_energy_sub_eq {d : ℕ} {U : Book.Ch02.Domain d} (a : Book.Ch02.CoeffOn U) {p q : Vec d} {v : Book.Ch02.Solution U a} (hv : Book.Ch02.IsResponseMaximizer U a p q v) (w : Book.Ch02.Solution U a) : (Book.Ch02.average U fun (x : Vec d) => blockVecDot (v.toH1.grad x - w.toH1.grad x, matVecMul (a.toCoeffField x) (v.toH1.grad x - w.toH1.grad x)) (blockMatVecMul (Book.Ch02.blockMatrixField a x) (v.toH1.grad x - w.toH1.grad x, matVecMul (a.toCoeffField x) (v.toH1.grad x - w.toH1.grad x)))) = 4 * (Book.Ch02.responseJ U a p q - Book.Ch02.responseValue U a p q w)

The expansion of the response functional around its maximizer, in block form: for every admissible competitor w,

⨍_V ‖𝐀^{1/2}(X(V) - X_w)‖² = 4(J(V,p,q;a) - ⨍_V(-½∇w·σ∇w - p·a∇w + q·∇w)),

the printed identity together with the remark that its right side "is one quarter of the corresponding block energy", because the difference of two primal optimizer fields has the form (∇φ, a∇φ) and the pointwise energy identity applies to it. This is the per-cell half of the exact factor-two response identity; the averaging over the aligned subdivision is the exact-partition step.