High-contrast homogenization: Provider.Response.ConstantSkewProfiles

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

Constant-skew invariance of response profile carriers

The hatted blocks in the response argument are simultaneous shear congruences of the original samplewise blocks and annealed means. This file identifies the resulting all-scale maximum, recent defects, and centered and below-start profile maxima with their unhatted carriers.

theorem HCPolySupport.HighContrast.Response.diagonalWeakMaximum_subSkew {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (rho : ℝ) (t : ℤ) (E : BlockMat d) (a : CoeffSpace d) (g : Mat d) (hg : IsSkewMat g) : diagonalWeakMaximum rho q t (skewBlockCongr g E) (a.subSkew g hg) = diagonalWeakMaximum rho q t E a

Constant-skew recentering preserves the all-scale positive excess maximum when the reference block is recentered simultaneously.

theorem HCPolySupport.HighContrast.Response.diagonalWeakCellDefect_subSkew {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k t : ℤ) (E : BlockMat d) (a : CoeffSpace d) (g : Mat d) (hg : IsSkewMat g) : diagonalWeakCellDefect q k t (skewBlockCongr g E) (a.subSkew g hg) = diagonalWeakCellDefect q k t E a

Constant-skew recentering preserves every recent cell defect.

theorem HCPolySupport.HighContrast.Response.diagonalWeakAverageDefect_eq_normalized_average {d : ℕ} (q : Mat d) (k t : ℤ) (E : BlockMat d) (a : CoeffSpace d) : diagonalWeakAverageDefect q k t E a = normalizedBlock (ofFullBlockMat ((↑(alignedIndex q k t).card)⁻¹ • ∑ w ∈ alignedIndex q k t, toFullBlockMat (blockSub (adaptedResponse q k w a) (coarseBlock (adaptedCell q t) a)))) E

The average of normalized defects is the normalization of their raw average.

theorem HCPolySupport.HighContrast.Response.blockSize_diagonalWeakAverageDefect_subSkew {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (k t : ℤ) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (a : CoeffSpace d) (g : Mat d) (hg : IsSkewMat g) : blockSize (diagonalWeakAverageDefect q k t (skewBlockCongr g E) (a.subSkew g hg)) (Book.Ch02.blockIdentity d) = blockSize (diagonalWeakAverageDefect q k t E a) (Book.Ch02.blockIdentity d)

The scalar size of the averaged normalized defect is unchanged by a constant-skew recentering.

theorem HCPolySupport.HighContrast.Response.diagonalWeakCellSum_subSkew {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (H : ℕ) (s : ℝ) (E : BlockMat d) (a : CoeffSpace d) (g : Mat d) (hg : IsSkewMat g) : diagonalWeakCellSum q t H s (skewBlockCongr g E) (a.subSkew g hg) = diagonalWeakCellSum q t H s E a

Constant-skew recentering preserves the recent cell sum.

theorem HCPolySupport.HighContrast.Response.diagonalWeakAverageSum_subSkew {d : ℕ} {q : Mat d} (hq : Matrix.PosDef q) (t : ℤ) (H : ℕ) (s rho : ℝ) {E : BlockMat d} (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) (a : CoeffSpace d) (g : Mat d) (hg : IsSkewMat g) : diagonalWeakAverageSum q t H s rho (skewBlockCongr g E) (a.subSkew g hg) = diagonalWeakAverageSum q t H s rho E a

Constant-skew recentering preserves the recent averaged-defect sum.