High-contrast homogenization: Provider.Response.AdaptedWeakProductResponse

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

Weak-product control of the adapted response cutoff term

The reference gradient and flux defects are transported in their separate metric slots. Their reciprocal distortions are multiplied before the rounded grid estimate is applied, while the cutoff coefficient retains its inverse side-length gain. This gives the samplewise majorants used by the annealed primal and adjoint weak quantities.

theorem HCPolySupport.HighContrast.Response.ofReal_abs_adaptedResponseCutoff_le_weakRoot_sq {d : ℕ} [NeZero d] {l t : ℤ} {m0 : Mat d} (hm0 : Matrix.PosDef m0) (hgrid : IsRoundedGrid l (roundedGrid l m0)) (b : CoeffSpace d) (p r : Vec d) (center : BlockVec d) : have hq := ⋯; have W := ENNReal.ofReal (3 ^ (-(1 / 2) * ↑t)) * adaptedWeakSeminorm (roundedGrid l m0) t (1 / 2) fun (x : Vec d) => blockMatVecMul (Book.Ch02.blockDiag (matSqrt m0) (matSqrt m0)⁻¹) (diagonalWeakState hq t b p r x - center); have term := Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) => adaptedPreYoungCutoff (roundedGrid l m0) hq t x * (1 / 2 * vecDot ((centeredResponseOptimizer (adaptedDomain hq t) b p r).toH1.grad x - center.1) (matVecMul ((b.coeffOn (adaptedDomain hq t)).toCoeffField x) ((centeredResponseOptimizer (adaptedDomain hq t) b p r).toH1.grad x) - center.2)); ENNReal.ofReal |term| ≤ ENNReal.ofReal (1 + divCurlDimensionCoeff d * adaptedCutoffDerivativeCoeff d * (51 / 50 * ↑d ^ 2)) * W ^ 2

The adapted cutoff product for one physical response sample is controlled by the square of its normalized metric weak root. The harmless leading one keeps the dimension-only coefficient nonzero when the weak root is infinite.