Documentation

LeanPool.HighContrastHomogenization.Geometry.Sharp

High-contrast homogenization: Geometry.Sharp #

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

The sharp involution and the shear #

On a doubled block matrix the reference text sets R := (0 I; I 0), the swap matrix of s.scale.selection, and H^♯ := R H^{-1} R, and writes G_h := (I 0; h I) for the shear. This file fixes both on the flattened carrier FullBlockMat d, where the doubled index type is a sum type and Matrix.fromBlocks is available, and proves the rules for the primal-adjoint involution together with its invariance under a constant skew shear: the sharp map is an involution, it reverses the Loewner order, it is homogeneous of degree minus one, and it commutes with congruence by a shear along a skew matrix.

The recentering identity rests on the two displayed identities of the reference proof, R G_h^{-1} = G_h^t R and G_h^{-t} R = R G_h, valid exactly because h is skew.

def HCPolySupport.HighContrast.fullBlockRefl (d : ℕ) :

The reflection R = (0 I; I 0) of s.scale.selection.

Equations

HCPolySupport.HighContrast.fullBlockRefl d = Matrix.fromBlocks 0 1 1 0

Instances For

def HCPolySupport.HighContrast.fullBlockShear {d : ℕ} (h : Mat d) :

The shear G_h = (I 0; h I).

Equations

HCPolySupport.HighContrast.fullBlockShear h = Matrix.fromBlocks 1 0 h 1

Instances For

noncomputable def HCPolySupport.HighContrast.fullBlockSharp {d : ℕ} (H : FullBlockMat d) :

The primal-adjoint involution H^♯ = R H^{-1} R.

Equations

HCPolySupport.HighContrast.fullBlockSharp H = HCPolySupport.HighContrast.fullBlockRefl d * H⁻¹ * HCPolySupport.HighContrast.fullBlockRefl d

Instances For

The reflection #

@[simp]

theorem HCPolySupport.HighContrast.fullBlockRefl_mul_self {d : ℕ} :

fullBlockRefl d * fullBlockRefl d = 1

theorem HCPolySupport.HighContrast.conjTranspose_fullBlockRefl {d : ℕ} :

Matrix.conjTranspose (fullBlockRefl d) = fullBlockRefl d

theorem HCPolySupport.HighContrast.isUnit_fullBlockRefl {d : ℕ} :

IsUnit (fullBlockRefl d)

theorem HCPolySupport.HighContrast.isUnit_det_fullBlockRefl {d : ℕ} :

IsUnit (Matrix.det (fullBlockRefl d))

@[simp]

theorem HCPolySupport.HighContrast.fullBlockRefl_inv {d : ℕ} :

(fullBlockRefl d)⁻¹ = fullBlockRefl d

theorem HCPolySupport.HighContrast.posDef_refl_conj {d : ℕ} {H : FullBlockMat d} (hH : Matrix.PosDef H) :

(fullBlockRefl d * H * fullBlockRefl d).PosDef

Conjugation by the reflection preserves positive definiteness.

theorem HCPolySupport.HighContrast.refl_conj_le_refl_conj {d : ℕ} {H K : FullBlockMat d} (h : H ≤ K) :

fullBlockRefl d * H * fullBlockRefl d ≤ fullBlockRefl d * K * fullBlockRefl d

Conjugation by the reflection is monotone.

The sharp involution #

theorem HCPolySupport.HighContrast.posDef_fullBlockSharp {d : ℕ} {H : FullBlockMat d} (hH : Matrix.PosDef H) :

Matrix.PosDef (fullBlockSharp H)

The sharp of a positive definite block is positive definite.

theorem HCPolySupport.HighContrast.fullBlockSharp_fullBlockSharp {d : ℕ} {H : FullBlockMat d} (hH : Matrix.PosDef H) :

fullBlockSharp (fullBlockSharp H) = H

The sharp map is an involution.

theorem HCPolySupport.HighContrast.fullBlockSharp_le_fullBlockSharp {d : ℕ} {H K : FullBlockMat d} (hH : Matrix.PosDef H) (hK : Matrix.PosDef K) (h : H ≤ K) :

fullBlockSharp K ≤ fullBlockSharp H

The sharp map reverses the Loewner order.

theorem HCPolySupport.HighContrast.fullBlockSharp_smul {d : ℕ} {H : FullBlockMat d} (hH : Matrix.PosDef H) {c : ℝ} (hc : 0 < c) :

fullBlockSharp (c • H) = c⁻¹ • fullBlockSharp H

The sharp map is homogeneous of degree minus one.

theorem HCPolySupport.HighContrast.det_fullBlockSharp {d : ℕ} {H : FullBlockMat d} (hH : Matrix.PosDef H) :

Matrix.det (fullBlockSharp H) = (Matrix.det H)⁻¹

The determinant of the sharp is the inverse determinant.

The shear and recentering #

@[simp]

theorem HCPolySupport.HighContrast.fullBlockShear_zero {d : ℕ} :

fullBlockShear 0 = 1

theorem HCPolySupport.HighContrast.fullBlockShear_mul {d : ℕ} (h k : Mat d) :

fullBlockShear h * fullBlockShear k = fullBlockShear (h + k)

theorem HCPolySupport.HighContrast.fullBlockShear_inv {d : ℕ} (h : Mat d) :

(fullBlockShear h)⁻¹ = fullBlockShear (-h)

theorem HCPolySupport.HighContrast.isUnit_fullBlockShear {d : ℕ} (h : Mat d) :

IsUnit (fullBlockShear h)

theorem HCPolySupport.HighContrast.conjTranspose_fullBlockShear {d : ℕ} (h : Mat d) :

Matrix.conjTranspose (fullBlockShear h) = Matrix.fromBlocks 1 (Matrix.conjTranspose h) 0 1

theorem HCPolySupport.HighContrast.refl_mul_shear_inv {d : ℕ} {h : Mat d} (hskew : Matrix.conjTranspose h = -h) :

fullBlockRefl d * (fullBlockShear h)⁻¹ = Matrix.conjTranspose (fullBlockShear h) * fullBlockRefl d

The first recentering identity of the reference proof, R G_h^{-1} = G_h^t R, for a skew h.

theorem HCPolySupport.HighContrast.conjTranspose_fullBlockShear_inv {d : ℕ} {h : Mat d} (hskew : Matrix.conjTranspose h = -h) :

(Matrix.conjTranspose (fullBlockShear h))⁻¹ = Matrix.fromBlocks 1 h 0 1

The inverse of the transposed shear along a skew matrix is the transposed shear along its negative.

theorem HCPolySupport.HighContrast.shear_inv_conjTranspose_mul_refl {d : ℕ} {h : Mat d} (hskew : Matrix.conjTranspose h = -h) :

(Matrix.conjTranspose (fullBlockShear h))⁻¹ * fullBlockRefl d = fullBlockRefl d * fullBlockShear h

The second recentering identity of the reference proof, G_h^{-t} R = R G_h, for a skew h.

theorem HCPolySupport.HighContrast.fullBlockSharp_shear_conj {d : ℕ} {H : FullBlockMat d} (hH : Matrix.PosDef H) {h : Mat d} (hskew : Matrix.conjTranspose h = -h) :

fullBlockSharp (Matrix.conjTranspose (fullBlockShear h) * H * fullBlockShear h) = Matrix.conjTranspose (fullBlockShear h) * fullBlockSharp H * fullBlockShear h

Recentering: the sharp map commutes with congruence by a shear along a skew matrix.