Documentation

LeanPool.HighContrastHomogenization.Provider.Response.ConstantSkewAnnealed

High-contrast homogenization: Provider.Response.ConstantSkewAnnealed #

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

Constant-skew covariance after annealing #

The samplewise gradient and flux transformations commute with expectation under coarse-block integrability. Consequently the centered response is unchanged after correcting the second load.

source
theorem HCPolySupport.HighContrast.Response.annealedOptimizerGradient_subSkew {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} (U : Book.Ch02.Domain d) (g : Mat d) (hg : IsSkewMat g) (p q : Vec d) :
(fun (i : Fin d) => ∫ (a : CoeffSpace d), Book.Ch02.averageGradient U ((a.subSkew g hg).coeffOn U) (centeredResponseOptimizer U (a.subSkew g hg) p q) i ∂P) = annealedOptimizerGradient P U p (q - matVecMul g p)

The separately annealed optimizer gradient is unchanged by recentering after the load correction.

source
theorem HCPolySupport.HighContrast.Response.annealedOptimizerFlux_subSkew {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (U : Book.Ch02.Domain d) (hint : HasIntegrableCoarseBlock P U.carrier) (g : Mat d) (hg : IsSkewMat g) (p q : Vec d) :
(fun (i : Fin d) => ∫ (a : CoeffSpace d), Book.Ch02.averageFlux U ((a.subSkew g hg).coeffOn U) (centeredResponseOptimizer U (a.subSkew g hg) p q) i ∂P) = annealedOptimizerFlux P U p (q - matVecMul g p) - matVecMul g (annealedOptimizerGradient P U p (q - matVecMul g p))

The separately annealed optimizer flux is shifted by the constant skew matrix applied to the annealed optimizer gradient.

source
theorem HCPolySupport.HighContrast.Response.centeredResponse_subSkew {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] (U : Book.Ch02.Domain d) (hint : HasIntegrableCoarseBlock P U.carrier) (g : Mat d) (hg : IsSkewMat g) (p q : Vec d) :
(∫ (a : CoeffSpace d), Book.Ch02.responseJ U ((a.subSkew g hg).coeffOn U) p q ∂P - 1 / 2 * vecDot (fun (i : Fin d) => ∫ (a : CoeffSpace d), Book.Ch02.averageGradient U ((a.subSkew g hg).coeffOn U) (centeredResponseOptimizer U (a.subSkew g hg) p q) i ∂P) fun (i : Fin d) => ∫ (a : CoeffSpace d), Book.Ch02.averageFlux U ((a.subSkew g hg).coeffOn U) (centeredResponseOptimizer U (a.subSkew g hg) p q) i ∂P) = centeredResponse P U p (q - matVecMul g p)

A constant-skew recentering preserves the centered response after the second load is corrected. Both annealed optimizer means are transformed before their scalar product is simplified.