High-contrast homogenization: Provider.Quenched.SmallContrastAdjointMirrors

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

The adjoint mirrors: bad energy and centering variance

The adjoint sides of the bad-event optimizer energy and of the centering variance, by the same source-envelope and single-cell-variance routes as the primal sides; the adjoint state is the sign-congruent primal state at the transposed sample, so every bound transports through the sign congruence with the plus load in place of the minus load.

theorem HCPolySupport.HighContrast.Quenched.profileAdjointCenterVariance_le_variance {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {m : Mat d} (hm : Matrix.PosDef m) {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (hint : HasFiniteAdaptedMean P q t) (hEt : Book.Ch02.BlockPosDef (adaptedMean P q t)) (h0 : Mat d) (hh0 : IsSkewMat h0) (p r : Vec d) : Response.profileAdjointCenterVariance P m hq t (fun (a : CoeffSpace d) => a.subSkew h0 hh0) p r ≤ ENNReal.ofReal (Response.diagonalWeakMetricFactor m (Response.skewBlockCongr h0 (adaptedMean P q t)) * Response.diagonalWeakLoadPlus (Response.skewBlockCongr h0 (adaptedMean P q t)) p r) * scaleVariance P q (adaptedMean P q t) t

The adjoint centering variance at the recentered samples is bounded by the terminal single-cell fluctuation carrier in the adapted-mean normalization.