High-contrast homogenization: Provider.Response.ProfileCenterIdentities

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

Exact centers after constant-skew recentering

The primal and coefficient-transpose optimizer centers are computed from their own loads. Constant-skew covariance identifies their annealed blocks with the corresponding shear congruences. The final two results flatten the identities in the signs used by the load-calibration argument.

The two independently annealed centers

theorem HCPolySupport.HighContrast.Response.profilePrimalCenter_subSkew_eq {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (hint : HasFiniteAdaptedMean P q t) (h0 : Mat d) (hh0 : IsSkewMat h0) (pMinus qMinus : Vec d) : profilePrimalCenter P hq t (fun (a : CoeffSpace d) => a.subSkew h0 hh0) pMinus qMinus = blockMatVecMul (Book.Ch02.blockR d) (blockMatVecMul (skewBlockCongr h0 (adaptedMean P q t)) (-pMinus, qMinus)) + (-pMinus, qMinus)

The primal hatted center is (I + R Êₜ)(-p⁻,q⁻).

theorem HCPolySupport.HighContrast.Response.profileAdjointCenter_subSkew_eq {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (hint : HasFiniteAdaptedMean P q t) (h0 : Mat d) (hh0 : IsSkewMat h0) (pPlus qPlus : Vec d) : profileAdjointCenter P hq t (fun (a : CoeffSpace d) => a.subSkew h0 hh0) pPlus qPlus = blockMatVecMul (Book.Ch02.blockR d) (blockMatVecMul (Book.Ch02.blockMatMul (Book.Ch02.blockDiag 1 (-1)) (Book.Ch02.blockMatMul (skewBlockCongr h0 (adaptedMean P q t)) (Book.Ch02.blockDiag 1 (-1)))) (-pPlus, qPlus)) + (-pPlus, qPlus)

The independently computed adjoint hatted center uses the signed congruence of the hatted mean and its own load.

Load-calibration forms

theorem HCPolySupport.HighContrast.Response.toFullBlockVec_profilePrimalCenter_subSkew_eq {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (hint : HasFiniteAdaptedMean P q t) (h0 : Mat d) (hh0 : IsSkewMat h0) (pMinus qMinus : Vec d) : toFullBlockVec (profilePrimalCenter P hq t (fun (a : CoeffSpace d) => a.subSkew h0 hh0) pMinus qMinus) = toFullBlockVec (-pMinus, qMinus) + Matrix.mulVec (fullBlockRefl d) (Matrix.mulVec (toFullBlockMat (skewBlockCongr h0 (adaptedMean P q t))) (toFullBlockVec (-pMinus, qMinus)))

Flattened primal identity in the exact x⁻ + R Êₜx⁻ form.

theorem HCPolySupport.HighContrast.Response.profileAdjointCenter_subSkew_paperSign_eq {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (hint : HasFiniteAdaptedMean P q t) (h0 : Mat d) (hh0 : IsSkewMat h0) (pPlus qPlus : Vec d) : blockMatVecMul (Book.Ch02.blockDiag (-1) 1) (profileAdjointCenter P hq t (fun (a : CoeffSpace d) => a.subSkew h0 hh0) pPlus qPlus) = (pPlus, qPlus) - blockMatVecMul (Book.Ch02.blockR d) (blockMatVecMul (skewBlockCongr h0 (adaptedMean P q t)) (pPlus, qPlus))

The paper-signed adjoint center is exactly x⁺ - R Êₜx⁺.

theorem HCPolySupport.HighContrast.Response.toFullBlockVec_profileAdjointCenter_subSkew_eq {d : ℕ} {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (hint : HasFiniteAdaptedMean P q t) (h0 : Mat d) (hh0 : IsSkewMat h0) (pPlus qPlus : Vec d) : toFullBlockVec (blockMatVecMul (Book.Ch02.blockDiag (-1) 1) (profileAdjointCenter P hq t (fun (a : CoeffSpace d) => a.subSkew h0 hh0) pPlus qPlus)) = toFullBlockVec (pPlus, qPlus) - Matrix.mulVec (fullBlockRefl d) (Matrix.mulVec (toFullBlockMat (skewBlockCongr h0 (adaptedMean P q t))) (toFullBlockVec (pPlus, qPlus)))

Flattened adjoint identity in the exact x⁺ - R Êₜx⁺ form.