High-contrast homogenization: Provider.Response.ConstantSkewNormalization

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

Scalar invariants of constant-skew congruence

The lower triangular shear is invertible. A common congruence by this shear therefore preserves the doubled Loewner order and the two scalar sizes used by the response profile. Normalization is also recorded as a linear operation, which lets the recent averaged defect be handled without choosing an orthogonal representative of the congruence.

theorem HCPolySupport.HighContrast.Response.skewBlockCongr_loewner_iff {d : ℕ} (g : Mat d) (A B : BlockMat d) : BlockMatLoewnerLE (skewBlockCongr g A) (skewBlockCongr g B) ↔ BlockMatLoewnerLE A B

A common shear congruence preserves and reflects the structural Loewner order.

theorem HCPolySupport.HighContrast.Response.blockScale_skewBlockCongr {d : ℕ} (g : Mat d) (c : ℝ) (A : BlockMat d) : skewBlockCongr g (blockScale c A) = blockScale c (skewBlockCongr g A)

Scalar dilation commutes with a shear congruence.

theorem HCPolySupport.HighContrast.Response.blockSub_skewBlockCongr {d : ℕ} (g : Mat d) (A B : BlockMat d) : skewBlockCongr g (blockSub A B) = blockSub (skewBlockCongr g A) (skewBlockCongr g B)

Subtraction commutes with a shear congruence.

theorem HCPolySupport.HighContrast.Response.blockSize_skewBlockCongr {d : ℕ} (g : Mat d) (A E : BlockMat d) : blockSize (skewBlockCongr g A) (skewBlockCongr g E) = blockSize A E

The two-sided normalized block size is invariant under a common shear congruence.

theorem HCPolySupport.HighContrast.Response.blockExcess_skewBlockCongr {d : ℕ} (g : Mat d) (A E : BlockMat d) : blockExcess (skewBlockCongr g A) (skewBlockCongr g E) = blockExcess A E

The positive normalized excess is invariant under a common shear congruence.

theorem HCPolySupport.HighContrast.Response.blockSize_normalizedBlock_identity {d : ℕ} {A E : BlockMat d} (hA : IsSymmetricBlockMat A) (hE : IsSymmetricBlockMat E) (hEpd : Book.Ch02.BlockPosDef E) : blockSize (normalizedBlock A E) (Book.Ch02.blockIdentity d) = blockSize A E

Measuring a normalized symmetric block against the identity gives the same scalar size as measuring the original block against its reference.

theorem HCPolySupport.HighContrast.Response.normalizedBlock_ofFullBlockMat_smul_sum {d : ℕ} {ι : Type u_1} (s : Finset ι) (c : ℝ) (A : ι → BlockMat d) (E : BlockMat d) : normalizedBlock (ofFullBlockMat (c • ∑ i ∈ s, toFullBlockMat (A i))) E = ofFullBlockMat (c • ∑ i ∈ s, toFullBlockMat (normalizedBlock (A i) E))

A fixed normalization commutes with a finite weighted sum.

theorem HCPolySupport.HighContrast.Response.skewBlockCongr_ofFullBlockMat_smul_sum {d : ℕ} {ι : Type u_1} (g : Mat d) (s : Finset ι) (c : ℝ) (A : ι → BlockMat d) : skewBlockCongr g (ofFullBlockMat (c • ∑ i ∈ s, toFullBlockMat (A i))) = ofFullBlockMat (c • ∑ i ∈ s, toFullBlockMat (skewBlockCongr g (A i)))

A shear congruence commutes with a finite weighted sum.