High-contrast homogenization: Geometry.CanonicalDeterminant

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

The determinant clause of the canonical balance

The determinant clause of the canonical balance reads determinants in the balance chain M(E) ≤ E ≤ 𝔡(E)^{1/2} M(E). Since det M(E) = 1 and the matrices have size 2d, this is 1 ≤ det(E) ≤ 𝔡(E)^d, the determinant bound used in p.global.selection, written before the d-th root is taken.

theorem HCPolySupport.HighContrast.canonImbalance_pos {d : ℕ} [Nonempty (Fin d)] {E : FullBlockMat d} (hE : Matrix.PosDef E) : 0 < canonImbalance E

The imbalance of a positive block is positive once the dimension is.

theorem HCPolySupport.HighContrast.one_le_det_of_fullBlockSharp_le {d : ℕ} {E : FullBlockMat d} (hE : Matrix.PosDef E) (hle : fullBlockSharp E ≤ E) : 1 ≤ Matrix.det E

The lower determinant bound used in p.global.selection: a self-dominating positive block has determinant at least one.

theorem HCPolySupport.HighContrast.det_le_canonImbalance_pow {d : ℕ} [Nonempty (Fin d)] {E : FullBlockMat d} (hE : Matrix.PosDef E) (hle : fullBlockSharp E ≤ E) : Matrix.det E ≤ canonImbalance E ^ d

The upper determinant bound used in p.global.selection: the determinant of a self-dominating positive block is at most the d-th power of its imbalance, the exponent being half the matrix size.