High-contrast homogenization: Provider.Response.CenteredResponseAnnealed

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

Annealed response energy and optimizer means

The scalar response and the two spatial averages of its canonical optimizer are quadratic and linear readings of the same coarse block. Entrywise integrability of that block therefore identifies their annealed values with the corresponding readings of the annealed block.

theorem HCPolySupport.HighContrast.Response.responseJ_eq_coarseBlock {d : ℕ} (U : Book.Ch02.Domain d) (a : CoeffSpace d) (p q : Vec d) : Book.Ch02.responseJ U (a.coeffOn U) p q = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (coarseBlock U.carrier a) (-p, q)) - vecDot p q

The response value is the coarse-block quadratic form at the signed load.

theorem HCPolySupport.HighContrast.Response.integrable_coarseBlock_mulVec_apply {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {U : Set (Vec d)} (hint : HasIntegrableCoarseBlock P U) (X : BlockVec d) (α : BlockCoord d) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => toFullBlockVec (blockMatVecMul (coarseBlock U a) X) α) P

Each coordinate of a coarse block applied to a fixed doubled vector is integrable under an integrable coefficient law.

theorem HCPolySupport.HighContrast.Response.integrable_coarseBlock_quadratic {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {U : Set (Vec d)} (hint : HasIntegrableCoarseBlock P U) (X : BlockVec d) : MeasureTheory.Integrable (fun (a : CoeffSpace d) => blockVecDot X (blockMatVecMul (coarseBlock U a) X)) P

The quadratic form of the random coarse block is integrable.

theorem HCPolySupport.HighContrast.Response.integral_coarseBlock_mulVec {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} {U : Set (Vec d)} (hint : HasIntegrableCoarseBlock P U) (X : BlockVec d) : (fun (α : BlockCoord d) => ∫ (a : CoeffSpace d), toFullBlockVec (blockMatVecMul (coarseBlock U a) X) α ∂P) = toFullBlockVec (blockMatVecMul (annealedBlock P U) X)

Integration commutes with applying the coarse block to a deterministic doubled vector.

theorem HCPolySupport.HighContrast.Response.annealed_responseJ_eq {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (U : Book.Ch02.Domain d) (hint : HasIntegrableCoarseBlock P U.carrier) (p q : Vec d) : ∫ (a : CoeffSpace d), Book.Ch02.responseJ U (a.coeffOn U) p q ∂P = 1 / 2 * blockVecDot (-p, q) (blockMatVecMul (annealedBlock P U.carrier) (-p, q)) - vecDot p q

The annealed response energy is the annealed-block quadratic form.

theorem HCPolySupport.HighContrast.Response.annealed_optimizer_average_eq {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (U : Book.Ch02.Domain d) (hint : HasIntegrableCoarseBlock P U.carrier) (p q : Vec d) : (annealedOptimizerGradient P U p q, annealedOptimizerFlux P U p q) = blockMatVecMul (Book.Ch02.blockR d) (blockMatVecMul (annealedBlock P U.carrier) (-p, q)) + (-p, q)

The two separately annealed optimizer averages are the two rows of (R E + I)(-p,q).