High-contrast homogenization: Provider.Response.AffineResponseOptimizer

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

Affine covariance of canonical response optimizers

Affine pullback transports a physical response maximizer to a maximizer on the reference cube at the dual transformed loads. Gradient uniqueness then identifies the chosen reference maximizer almost everywhere. This is the natural strength for the raw Sobolev representatives, and it is sufficient to identify their cutoff product after integration.

theorem HCPolySupport.HighContrast.exists_affineResponseMaximizer {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) {a : Book.Ch02.CoeffOn (Response.adaptedDomain hq t)} {aRef : Book.Ch02.CoeffOn (Book.Ch02.cubeDomain (originCube d t))} (haRef : aRef.toCoeffField = affineCoefficient q ⋯ a.toCoeffField) (p r : Vec d) {u : Book.Ch02.Solution (Response.adaptedDomain hq t) a} (hu : Book.Ch02.IsResponseMaximizer (Response.adaptedDomain hq t) a p r u) : ∃ (uRef : Book.Ch02.Solution (Book.Ch02.cubeDomain (originCube d t)) aRef), (uRef.toH1.grad = fun (y : Vec d) => matVecMul (matTranspose q) (u.toH1.grad (matVecMul q y))) ∧ Book.Ch02.IsResponseMaximizer (Book.Ch02.cubeDomain (originCube d t)) aRef (matVecMul (matTranspose q) p) (matVecMul q⁻¹ r) uRef

Pulling a physical response maximizer to the reference cube preserves its maximizing property at the dual transformed loads.

theorem HCPolySupport.HighContrast.centeredResponseOptimizerDefects_affineAE {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) {aRef : Book.Ch02.CoeffOn (Book.Ch02.cubeDomain (originCube d t))} (haRef : aRef.toCoeffField = affineCoefficient q ⋯ (a.coeffOn (Response.adaptedDomain hq t)).toCoeffField) (p r p0 r0 : Vec d) : (Book.Ch05.Section53.JUpperBoundWeakNorms.canonicalMaximizerGradientDefectOnCube (originCube d t) aRef (matVecMul (matTranspose q) p) (matVecMul q⁻¹ r) (matVecMul (matTranspose q) p0) =ᵐ[volumeMeasureOn (cubeSet (originCube d t))] fun (y : Vec d) => matVecMul (matTranspose q) ((Response.centeredResponseOptimizer (Response.adaptedDomain hq t) a p r).toH1.grad (matVecMul q y) - p0)) ∧ Book.Ch05.Section53.JUpperBoundWeakNorms.canonicalMaximizerFluxDefectOnCube (originCube d t) aRef (matVecMul (matTranspose q) p) (matVecMul q⁻¹ r) (matVecMul q⁻¹ r0) =ᵐ[volumeMeasureOn (cubeSet (originCube d t))] fun (y : Vec d) => matVecMul q⁻¹ (matVecMul ((a.coeffOn (Response.adaptedDomain hq t)).toCoeffField (matVecMul q y)) ((Response.centeredResponseOptimizer (Response.adaptedDomain hq t) a p r).toH1.grad (matVecMul q y)) - r0)

The reference canonical gradient and flux defects are the dual affine pullbacks of the centered physical optimizer defects, almost everywhere on the closed reference cube.

theorem HCPolySupport.HighContrast.cutoffProductTermOnCube_affineResponseOptimizer {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (a : CoeffSpace d) {aRef : Book.Ch02.CoeffOn (Book.Ch02.cubeDomain (originCube d t))} (haRef : aRef.toCoeffField = affineCoefficient q ⋯ (a.coeffOn (Response.adaptedDomain hq t)).toCoeffField) (phi : Vec d → ℝ) (p r p0 r0 : Vec d) : Book.Ch05.Section53.JUpperBoundWeakNorms.cutoffProductTermOnCube (originCube d t) aRef (fun (y : Vec d) => phi (matVecMul q y)) (matVecMul (matTranspose q) p) (matVecMul q⁻¹ r) (matVecMul (matTranspose q) p0) (matVecMul q⁻¹ r0) = Book.Ch02.average (Response.adaptedDomain hq t) fun (x : Vec d) => phi x * (1 / 2 * vecDot ((Response.centeredResponseOptimizer (Response.adaptedDomain hq t) a p r).toH1.grad x - p0) (matVecMul ((a.coeffOn (Response.adaptedDomain hq t)).toCoeffField x) ((Response.centeredResponseOptimizer (Response.adaptedDomain hq t) a p r).toH1.grad x) - r0))

The reference cutoff product equals the normalized physical cutoff product for the centered primal optimizer, with both loads and both centers transformed.