High-contrast homogenization: Provider.Response.DiagonalWeakNormEnergy

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

Energy comparison for the diagonal weak estimate

The energy map is used with a self-dual diagonal metric. Two successive relative-size comparisons, reversed by the sharp involution, give the precise coefficient multiplying the starred coarse response.

theorem HCPolySupport.HighContrast.Response.diagonalMetric_le_scaled_blockSharp {d : ℕ} [NeZero d] {m : Mat d} (hm : Matrix.PosDef m) {E A : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (hA : IsSymmetricBlockMat A) (hApd : Book.Ch02.BlockPosDef A) : BlockMatLoewnerLE (Book.Ch02.blockDiag m m⁻¹) (blockScale (diagonalWeakMetricFactor m E ^ 2 * blockSize A E) (blockSharp A))

The diagonal metric is bounded by the sharp response with coefficient K_{M,E}^2 |E^{-1/2}AE^{-1/2}|.

theorem HCPolySupport.HighContrast.Response.toFullBlockMat_coarseStarredBlockMatrix_eq_fullBlockSharp {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) : toFullBlockMat (Book.Ch02.coarseStarredBlockMatrix U a) = fullBlockSharp (toFullBlockMat (Book.Ch02.coarseBlockMatrix U a))

The starred Chapter 2 coarse response is the sharp of its ordinary coarse response on the flattened carrier.

theorem HCPolySupport.HighContrast.Response.diagonalMetric_le_scaled_coarseStarred_adaptedCellAt {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) (w : Fin d → ℤ) {a : CoeffSpace d} {c : Book.Ch02.CoeffOn (adaptedDomainAt hq k w)} (hc : Book.Ch02.coarseBlockMatrix (adaptedDomainAt hq k w) c = adaptedResponse q k w a) {m : Mat d} (hm : Matrix.PosDef m) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) : BlockMatLoewnerLE (Book.Ch02.blockDiag m m⁻¹) (blockScale (diagonalWeakMetricFactor m E ^ 2 * blockSize (adaptedResponse q k w a) E) (Book.Ch02.coarseStarredBlockMatrix (adaptedDomainAt hq k w) c))

The energy-map comparison coefficient on an aligned cell, expressed only through its response block and the deterministic reference.

theorem HCPolySupport.HighContrast.Response.metricBlockNormSq_average_le_adaptedCellAt {d : ℕ} [NeZero d] {q : Mat d} (hq : Matrix.PosDef q) (k : ℤ) (w : Fin d → ℤ) {a : CoeffSpace d} {c : Book.Ch02.CoeffOn (adaptedDomainAt hq k w)} (hc : Book.Ch02.coarseBlockMatrix (adaptedDomainAt hq k w) c = adaptedResponse q k w a) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (adaptedCellAt q k w) c.toCoeffField) {Y : Book.Ch02.DoubledField d} (hY : Book.Ch02.IsDoubledResponseField (adaptedDomainAt hq k w) c Y) {m : Mat d} (hm : Matrix.PosDef m) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) : metricBlockNormSq m (Book.Ch02.averageVec (adaptedDomainAt hq k w) Y.potential, Book.Ch02.averageVec (adaptedDomainAt hq k w) Y.flux) ≤ diagonalWeakMetricFactor m E ^ 2 * blockSize (adaptedResponse q k w a) E * Book.Ch02.average (adaptedDomainAt hq k w) fun (x : Vec d) => blockVecDot (Y.eval x) (blockMatVecMul (Book.Ch02.blockMatrixField c x) (Y.eval x))

The metric square of the average of a doubled response field on one aligned cell is controlled by its cell energy.