High-contrast homogenization: Provider.Response.EnergyMap

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

The coarse energy map on the doubled response space

The second half of the deterministic input to the weak-norm estimate for the optimizer state is the coarse energy-map estimate. The paper derives it by combining the doubled splitting [Armstrong–Kuusi, (2.17)], the row-swap identity [Armstrong–Kuusi, (2.18)], and the doubled variational formula [Armstrong–Kuusi, (2.20)], then putting the first load equal to zero: ½Q·𝐀_*^{-1}(V)Q = max_{Z ∈ 𝒮(V;a)} ⨍_V(-½Z·𝐀Z + Q·Z). Evaluating at a fixed Y ∈ 𝒮(V;a) and taking the supremum over Q gives the energy bound for the dual block, ½y·𝐀_*(V)y ≤ ½⨍_V Y·𝐀Y with y = (Y)_V, and its metric form follows by comparing M_0 with 𝐀_*(V).

All three steps are carried out here on an arbitrary Chapter 2 domain. The supremum over Q is taken at the single admissible choice Q = 𝐀_*(V)y, which is what makes the argument finite; the two inverse clauses of BlockCoarseMatrixTheory supply 𝐀_*^{-1}𝐀_* = I.

The Loewner encoding of the matrix norms is the one fixed by Setup/Moments: |M_0^{-1/2}HM_0^{-1/2}| ≤ c is read as H ≤ cM_0, so the metric form is stated with that hypothesis rather than with a spectral norm.

The doubled zero load

@[simp]

theorem HCPolySupport.HighContrast.Response.blockVecDot_zero_left {d : ℕ} (X : BlockVec d) : blockVecDot 0 X = 0

Pairing against the zero doubled vector.

Averages of a doubled field against a fixed load

theorem HCPolySupport.HighContrast.Response.average_add {d : ℕ} {U : Book.Ch02.Domain d} {f g : Vec d → ℝ} (hf : MeasureTheory.IntegrableOn f U.carrier MeasureTheory.volume) (hg : MeasureTheory.IntegrableOn g U.carrier MeasureTheory.volume) : (Book.Ch02.average U fun (x : Vec d) => f x + g x) = Book.Ch02.average U f + Book.Ch02.average U g

The normalized average of a scalar sum splits, given integrability.

theorem HCPolySupport.HighContrast.Response.integrableOn_component {d : ℕ} {U : Book.Ch02.Domain d} {F : Vec d → Vec d} (hF : MemVectorL2 U.carrier F) (i : Fin d) : MeasureTheory.IntegrableOn (fun (x : Vec d) => F x i) U.carrier MeasureTheory.volume

A component of a square-integrable vector field is integrable on a Chapter 2 domain.

theorem HCPolySupport.HighContrast.Response.average_vecDot_const {d : ℕ} {U : Book.Ch02.Domain d} (c : Vec d) {F : Vec d → Vec d} (hF : MemVectorL2 U.carrier F) : (Book.Ch02.average U fun (x : Vec d) => vecDot c (F x)) = vecDot c (Book.Ch02.averageVec U F)

The average commutes with pairing against a fixed vector: (c·F)_U = c·(F)_U for the volume average over a domain.

theorem HCPolySupport.HighContrast.Response.average_blockVecDot_const {d : ℕ} {U : Book.Ch02.Domain d} (Q : BlockVec d) (Y : Book.Ch02.DoubledField d) (hp : MemVectorL2 U.carrier Y.potential) (hf : MemVectorL2 U.carrier Y.flux) : (Book.Ch02.average U fun (x : Vec d) => blockVecDot Q (Y.eval x)) = blockVecDot Q (Book.Ch02.averageVec U Y.potential, Book.Ch02.averageVec U Y.flux)

The average of a doubled field against a fixed load: (Q·Y)_U = Q·(Y)_U, the step that turns the doubled response value into a function of the cell average (Y)_U alone.

The doubled response at zero primal load

theorem HCPolySupport.HighContrast.Response.doubledResponseJ_zero_left {d : ℕ} {U : Book.Ch02.Domain d} (a : Book.Ch02.CoeffOn U) (Q : BlockVec d) : Book.Ch02.doubledResponseJ U a 0 Q = 1 / 2 * blockVecDot Q (blockMatVecMul (Book.Ch02.coarseStarredBlockMatrixInv U a) Q)

The doubled variational formula at zero first load ([Armstrong–Kuusi, (2.17)], [Armstrong–Kuusi, (2.20)]): 𝐉(V,0,Q;a) = ½Q·𝐀_*^{-1}(V)Q.

theorem HCPolySupport.HighContrast.Response.doubledResponseValue_le {d : ℕ} {U : Book.Ch02.Domain d} (a : Book.Ch02.CoeffOn U) (Q : BlockVec d) {Y : Book.Ch02.DoubledField d} (hY : Book.Ch02.IsDoubledResponseField U a Y) : Book.Ch02.doubledResponseValue U a 0 Q Y ≤ 1 / 2 * blockVecDot Q (blockMatVecMul (Book.Ch02.coarseStarredBlockMatrixInv U a) Q)

Every element of the response space is dominated by the doubled formula: for Y ∈ 𝒮(V;a), the value ⨍_V(-½Y·𝐀Y + Q·Y) is at most ½Q·𝐀_*^{-1}(V)Q. The maximizer supplied by DoubledResponseTheory makes the supremum a greatest element, so no boundedness argument is needed.

theorem HCPolySupport.HighContrast.Response.doubledResponseValue_zero_left_eq {d : ℕ} {U : Book.Ch02.Domain d} {lam Lam : ℝ} (a : Book.Ch02.CoeffOn U) (hEll : IsEllipticFieldOn lam Lam U.carrier a.toCoeffField) (Q : BlockVec d) {Y : Book.Ch02.DoubledField d} (hY : Book.Ch02.IsDoubledResponseField U a Y) : Book.Ch02.doubledResponseValue U a 0 Q Y = blockVecDot Q (Book.Ch02.averageVec U Y.potential, Book.Ch02.averageVec U Y.flux) - 1 / 2 * Book.Ch02.average U fun (x : Vec d) => blockVecDot (Y.eval x) (blockMatVecMul (Book.Ch02.blockMatrixField a x) (Y.eval x))

The doubled response value at zero first load, expanded: the value of a response field Y is Q·(Y)_V - ½⨍_V Y·𝐀Y, the form in which the supremum over Q is taken in the energy bound for the dual block.

The energy map

theorem HCPolySupport.HighContrast.Response.energy_map_le {d : ℕ} {U : Book.Ch02.Domain d} {lam Lam : ℝ} (a : Book.Ch02.CoeffOn U) (hEll : IsEllipticFieldOn lam Lam U.carrier a.toCoeffField) {Y : Book.Ch02.DoubledField d} (hY : Book.Ch02.IsDoubledResponseField U a Y) : 1 / 2 * blockVecDot (Book.Ch02.averageVec U Y.potential, Book.Ch02.averageVec U Y.flux) (blockMatVecMul (Book.Ch02.coarseStarredBlockMatrix U a) (Book.Ch02.averageVec U Y.potential, Book.Ch02.averageVec U Y.flux)) ≤ 1 / 2 * Book.Ch02.average U fun (x : Vec d) => blockVecDot (Y.eval x) (blockMatVecMul (Book.Ch02.blockMatrixField a x) (Y.eval x))

The coarse energy-map estimate, the energy bound for the dual block: for every field Y in the doubled response space 𝒮(V;a) with cell average y = (Y)_V, ½y·𝐀_*(V)y ≤ ½⨍_V Y·𝐀Y. The supremum over Q is realized at Q = 𝐀_*(V)y.

theorem HCPolySupport.HighContrast.Response.energy_map_metric_le {d : ℕ} {U : Book.Ch02.Domain d} {lam Lam : ℝ} (a : Book.Ch02.CoeffOn U) (hEll : IsEllipticFieldOn lam Lam U.carrier a.toCoeffField) {Y : Book.Ch02.DoubledField d} (hY : Book.Ch02.IsDoubledResponseField U a Y) (m : Mat d) {c : ℝ} (hc : 0 ≤ c) (hcmp : BlockMatLoewnerLE (Book.Ch02.blockDiag m m⁻¹) (blockScale c (Book.Ch02.coarseStarredBlockMatrix U a))) : 1 / 2 * blockVecDot (Book.Ch02.averageVec U Y.potential, Book.Ch02.averageVec U Y.flux) (blockMatVecMul (Book.Ch02.blockDiag m m⁻¹) (Book.Ch02.averageVec U Y.potential, Book.Ch02.averageVec U Y.flux)) ≤ c * (1 / 2 * Book.Ch02.average U fun (x : Vec d) => blockVecDot (Y.eval x) (blockMatVecMul (Book.Ch02.blockMatrixField a x) (Y.eval x)))

The metric form of the energy map: once the diagonal metric is dominated by the starred coarse block, M_0 ≤ c𝐀_*(V), the metric size of the cell average is controlled by the cell energy, |M_0^{1/2}(Y)_V|² ≤ c⨍_V Y·𝐀Y. The hypothesis is the Loewner encoding of the comparison coefficient |M_0^{1/2}𝐀_*^{-1}(V)M_0^{1/2}| displayed.