High-contrast homogenization: Setup.BlockAlgebra

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

Doubled block algebra: Schur data, contrasts, and matrix square roots

This file fixes the algebraic objects the reference text builds on a doubled block matrix: the Schur parametrization of e.annealed.schur, the scalar Loewner bound encoding the matrix norm |·|, the intrinsic contrast of the reference block, the reference aspect ratio of e.reference.aspect.ratio, and the positive semidefinite square root.

def HCPolySupport.HighContrast.blockScale {d : ℕ} (c : ℝ) (A : BlockMat d) : BlockMat d

Scalar dilation of a doubled block matrix.

Equations

• HCPolySupport.HighContrast.blockScale c A = { upperLeft := c • A.upperLeft, upperRight := c • A.upperRight, lowerLeft := c • A.lowerLeft, lowerRight := c • A.lowerRight }

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

A skew-symmetric d × d matrix.

Equations

• HCPolySupport.HighContrast.IsSkewMat h = (HCPolySupport.matTranspose h = -h)

noncomputable def HCPolySupport.HighContrast.specBound {d : ℕ} (M : Mat d) : ℝ

The scalar Loewner bound inf { t ≥ 0 : M ≤ t · I }; on symmetric positive semidefinite arguments this is the spectral norm |M|.

Equations

• HCPolySupport.HighContrast.specBound M = sInf {t : ℝ | 0 ≤ t ∧ HCPolySupport.MatLoewnerLE M (t • 1)}

noncomputable def HCPolySupport.HighContrast.schurSigmaStar {d : ℕ} (H : BlockMat d) : Mat d

The Schur σ_* block of a doubled block matrix in the parametrization e.annealed.schur: the lower-right block is σ_*⁻¹.

Equations

• HCPolySupport.HighContrast.schurSigmaStar H = H.lowerRight⁻¹

noncomputable def HCPolySupport.HighContrast.schurSkew {d : ℕ} (H : BlockMat d) : Mat d

The Schur skew block k of a doubled block matrix: the lower-left block is -σ_*⁻¹ k.

Equations

• HCPolySupport.HighContrast.schurSkew H = -(H.lowerRight⁻¹ * H.lowerLeft)

noncomputable def HCPolySupport.HighContrast.schurSigma {d : ℕ} (H : BlockMat d) : Mat d

The Schur symmetric block σ of a doubled block matrix: the upper-left block is σ + kᵗ σ_*⁻¹ k.

Equations

• HCPolySupport.HighContrast.schurSigma H = H.upperLeft - HCPolySupport.matTranspose (HCPolySupport.HighContrast.schurSkew H) * H.lowerRight * HCPolySupport.HighContrast.schurSkew H

noncomputable def HCPolySupport.HighContrast.blockContrast {d : ℕ} (H : BlockMat d) : ℝ

The intrinsic contrast of a doubled block matrix, in the Loewner-scaling form: inf of the t ≥ 0 for which some skew h gives σ + (k - h)ᵗ σ_*⁻¹ (k - h) ≤ t σ_*. On Schur-form positive blocks this is the paper's min_h |σ_*^{-1/2}(σ + (k-h)ᵗ σ_*⁻¹ (k-h)) σ_*^{-1/2}| (the intrinsic contrast of the reference block, e.Theta.m).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.lambdaRef {d : ℕ} (E : BlockMat d) : ℝ

λ_0 of the reference block (e.reference.aspect.ratio): |σ_{*,0}^{-1}|⁻¹, where σ_{*,0}^{-1} is the lower-right block.

Equations

• HCPolySupport.HighContrast.lambdaRef E = (HCPolySupport.HighContrast.specBound E.lowerRight)⁻¹

noncomputable def HCPolySupport.HighContrast.bigLambdaRef {d : ℕ} (E : BlockMat d) : ℝ

Λ_0 of the reference block (e.reference.aspect.ratio): min_h |σ_0 + (k_0 - h)ᵗ σ_{*,0}^{-1} (k_0 - h)| in Loewner-scaling form.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.aspectRatio {d : ℕ} (E : BlockMat d) : ℝ

The reference aspect ratio Π := Λ_0 / λ_0 (e.reference.aspect.ratio).

Equations

• HCPolySupport.HighContrast.aspectRatio E = HCPolySupport.HighContrast.bigLambdaRef E / HCPolySupport.HighContrast.lambdaRef E

noncomputable def HCPolySupport.HighContrast.refContrast {d : ℕ} (E : BlockMat d) : ℝ

The reference intrinsic contrast Θ (the intrinsic contrast of the reference block).

Equations

• HCPolySupport.HighContrast.refContrast E = HCPolySupport.HighContrast.blockContrast E

noncomputable def HCPolySupport.HighContrast.matSqrt {n : Type u_1} [Fintype n] [DecidableEq n] (M : Matrix n n ℝ) : Matrix n n ℝ

The positive-semidefinite square root, by canonical choice of the unique positive-semidefinite B with B * B = M; junk value 1 otherwise.

Equations

• HCPolySupport.HighContrast.matSqrt M = if h : ∃ (B : Matrix n n ℝ), B.PosSemidef ∧ B * B = M then h.choose else 1

Entrywise bookkeeping

theorem HCPolySupport.HighContrast.blockMatEntry_blockScale {d : ℕ} (c : ℝ) (A : BlockMat d) (α β : BlockCoord d) : blockMatEntry (blockScale c A) α β = c * blockMatEntry A α β

Entries of a scalar dilation of a doubled block matrix.

def HCPolySupport.HighContrast.blockEntrySum {d : ℕ} (A : BlockMat d) : ℝ

The sum of the absolute values of the entries of a doubled block matrix; a crude but uniform entrywise scale.

Equations

• HCPolySupport.HighContrast.blockEntrySum A = ∑ α : HCPolySupport.BlockCoord d, ∑ β : HCPolySupport.BlockCoord d, |HCPolySupport.blockMatEntry A α β|

theorem HCPolySupport.HighContrast.blockEntrySum_nonneg {d : ℕ} (A : BlockMat d) : 0 ≤ blockEntrySum A

theorem HCPolySupport.HighContrast.abs_blockMatEntry_le_blockEntrySum {d : ℕ} (A : BlockMat d) (α β : BlockCoord d) : |blockMatEntry A α β| ≤ blockEntrySum A

theorem HCPolySupport.HighContrast.blockEntrySum_blockScale {d : ℕ} {c : ℝ} (hc : 0 ≤ c) (A : BlockMat d) : blockEntrySum (blockScale c A) = c * blockEntrySum A

theorem HCPolySupport.HighContrast.abs_blockMatEntry_le_of_bounds {d : ℕ} {A F : BlockMat d} (hsymm : IsSymmetricBlockMat A) (hdiag0 : ∀ (γ : BlockCoord d), 0 ≤ blockMatEntry A γ γ) (hdiagF : ∀ (γ : BlockCoord d), blockMatEntry A γ γ ≤ blockMatEntry F γ γ) {α β : BlockCoord d} (hsum0 : 0 ≤ blockVecDot (blockBasis α + blockBasis β) (blockMatVecMul A (blockBasis α + blockBasis β))) (hsumF : blockVecDot (blockBasis α + blockBasis β) (blockMatVecMul A (blockBasis α + blockBasis β)) ≤ blockVecDot (blockBasis α + blockBasis β) (blockMatVecMul F (blockBasis α + blockBasis β))) : |blockMatEntry A α β| ≤ 2 * blockEntrySum F

Two-sided entrywise control of a symmetric doubled block matrix whose quadratic form is nonnegative on the diagonal and on the sums of two basis vectors, and is there dominated by that of a reference block.

theorem HCPolySupport.HighContrast.toFullBlockMat_eq_blockMatEntry {d : ℕ} (A : BlockMat d) (α β : BlockCoord d) : toFullBlockMat A α β = blockMatEntry A α β

The doubled quadratic form, expanded over the flattened basis.

theorem HCPolySupport.HighContrast.blockVecDot_blockMatVecMul_eq_sum {d : ℕ} (A : BlockMat d) (X : BlockVec d) : blockVecDot X (blockMatVecMul A X) = ∑ α : BlockCoord d, ∑ β : BlockCoord d, toFullBlockVec X α * (blockMatEntry A α β * toFullBlockVec X β)

theorem HCPolySupport.HighContrast.blockVecDot_inr {d : ℕ} (H : BlockMat d) (x : Vec d) : blockVecDot (0, x) (blockMatVecMul H (0, x)) = vecDot x (matVecMul H.lowerRight x)

The doubled quadratic form on the flux slot is the quadratic form of the lower-right block.