High-contrast homogenization: Provider.Response.WeakNormCellAverage

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

The cell average under the metric root and the centering

The concrete scale-average seminorm is evaluated in the weak-norm estimate for the optimizer state on the field

F = M_0^{1/2}(X_t - (X_t)_{U_t}),

so its cell averages are M_0^{1/2}((X_t)_{U_k(z)} - (X_t)_{U_t}). Getting there is two applications of linearity of the cell average, recorded here: a fixed matrix passes through the average, and a constant subtracted from the field is subtracted from the average. Both carry the square-integrability of the field on the cell as a hypothesis, which is what a Chapter 2 solution supplies, and the second also carries the finiteness and nondegeneracy of the cell volume, which every adapted cell has.

Together with the quadratic form identity for the root diag(m_0^{1/2}, m_0^{-1/2}) of the diagonal metric, this turns each cell contribution of the seminorm into metricBlockNormSq m_0 of a difference of cell averages, which is the shape the variational comparison of the optimizer averages is stated in. The root enters only through the hypotheses S^t = S and S^2 = m_0, which the printed positivity of the spatial metric supplies.

The last section records the scalar form of the block lift: on a field carried by the gradient slot alone the doubled seminorm is the scale-average seminorm of an ℝ^d-valued field with the ordinary Euclidean length.

The cell average through a fixed linear map

theorem HCPolySupport.HighContrast.Response.averageVec_matVecMul {d : ℕ} {U : Book.Ch02.Domain d} (A : Mat d) {F : Vec d → Vec d} (hF : MemVectorL2 U.carrier F) : (Book.Ch02.averageVec U fun (x : Vec d) => matVecMul A (F x)) = matVecMul A (Book.Ch02.averageVec U F)

The vector average commutes with a fixed matrix.

theorem HCPolySupport.HighContrast.Response.blockCellAverage_blockDiag {d : ℕ} {U : Book.Ch02.Domain d} (A B : Mat d) {F : Vec d → BlockVec d} (h1 : MemVectorL2 U.carrier fun (x : Vec d) => (F x).1) (h2 : MemVectorL2 U.carrier fun (x : Vec d) => (F x).2) : (blockCellAverage U.carrier fun (x : Vec d) => blockMatVecMul (Book.Ch02.blockDiag A B) (F x)) = blockMatVecMul (Book.Ch02.blockDiag A B) (blockCellAverage U.carrier F)

The cell average commutes with a block diagonal matrix: the step that moves the metric root M_0^{1/2} = diag(m_0^{1/2}, m_0^{-1/2}) of the diagonal metric outside the cell average of the scale-average seminorm.

theorem HCPolySupport.HighContrast.Response.memVectorL2_mono {d : ℕ} {U V : Set (Vec d)} (hVU : V ⊆ U) {F : Vec d → Vec d} (hF : MemVectorL2 U F) : MemVectorL2 V F

Square integrability passes to a subcell, which is how the parent optimizer is measured on every aligned child.

theorem HCPolySupport.HighContrast.Response.memVectorL2_sub_const {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {F : Vec d → Vec d} (hF : MemVectorL2 U F) (c : Vec d) : MemVectorL2 U fun (x : Vec d) => F x - c

Square integrability survives subtracting a constant on a cell of finite volume, which is what the centering X_t - (X_t)_{U_t} of the weak-norm estimate does to the optimizer state.

theorem HCPolySupport.HighContrast.Response.blockCellAverage_sub_const {d : ℕ} {U : Book.Ch02.Domain d} (c : BlockVec d) {F : Vec d → BlockVec d} (hne : MeasureTheory.volume U.carrier ≠ 0) (htop : MeasureTheory.volume U.carrier ≠ ⊤) (h1 : MemVectorL2 U.carrier fun (x : Vec d) => (F x).1) (h2 : MemVectorL2 U.carrier fun (x : Vec d) => (F x).2) : (blockCellAverage U.carrier fun (x : Vec d) => F x - c) = blockCellAverage U.carrier F - c

The cell average of a centered field: subtracting a constant from a field subtracts it from every cell average, which is what turns X_t - (X_t)_{U_t} into (X_t)_{U_k(z)} - (X_t)_{U_t} inside the seminorm.

The metric root

theorem HCPolySupport.HighContrast.Response.blockVecDot_self_blockDiag_root {d : ℕ} {m S : Mat d} (hsymm : matTranspose S = S) (hsq : S * S = m) (v : BlockVec d) : blockVecDot (blockMatVecMul (Book.Ch02.blockDiag S S⁻¹) v) (blockMatVecMul (Book.Ch02.blockDiag S S⁻¹) v) = metricBlockNormSq m v

The metric quadratic form is the squared length of the metric root's image: for a symmetric S with S^2 = m the map diag(S, S^{-1}) is the root M_0^{1/2} of the diagonal metric, and its squared image length is the quadratic form. This is the identity that lets the printed field M_0^{1/2}(X_t - (X_t)_{U_t}) be measured without ever constructing a root.

The block lift and its scalar form