High-contrast homogenization: Provider.Response.CenteredResponseAbsolute

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

The absolute centered-response bound

Each centered response at a linearly generated load is a quadratic form in the generating vector. This gives boundedness on the Euclidean unit sphere and allows the trace estimate to be enlarged to the sum of the two absolute responses.

theorem HCPolySupport.HighContrast.Response.bddAbove_absolute_centeredResponses {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (U : Book.Ch02.Domain d) (hint : HasIntegrableCoarseBlock P U.carrier) {S SStar K : Mat d} (hStar : Matrix.PosDef SStar) (hE : toFullBlockMat (annealedBlock P U.carrier) = schurBlock S SStar K) : BddAbove ((fun (e : Vec d) => |centeredResponse P U (centeredResponseLoadP S SStar K e) (centeredResponseLoadQ S SStar K e - Matrix.mulVec (responseSkew K) (centeredResponseLoadP S SStar K e))| + |centeredAdjointResponse P U (centeredResponseLoadP S SStar K e) (centeredResponseLoadQ S SStar K e + Matrix.mulVec (responseSkew K) (centeredResponseLoadP S SStar K e))|) '' {e : Vec d | e ⬝ᵥ e = 1})

The sum of the absolute primal and adjoint responses on the response unit sphere is bounded above.