High-contrast homogenization: Entry.Multiscale.ResponseTransferHelpers

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

Matrix-analysis helpers for the K3/K4 kernels of the p.response.transfer decomposition

Generic matrix-order and Schur-complement lemmas, and the canonical-imbalance comparison 𝔡(X) ≤ c ↔ X ≤ c • 𝐑X⁻¹𝐑, used by ResponseBlockObjects and EccentricityScaleDecay.

noncomputable def HCPolySupport.HighContrast.Multiscale.canonicalImbalance {d : ℕ} (A : BlockMat d) : ℝ

The canonical imbalance 𝔡(A) of a block (e.response.canonical.imbalance, near e.response.canonical.imbalance): 𝔡(A) := |(𝐑A⁻¹𝐑)^{-1/2}A(𝐑A⁻¹𝐑)^{-1/2}|, where 𝐑 is the fixed swap block near e.scale.selection.complete.profile (blockSwap). It is rendered faithfully via normalizedBlock/blockOpNorm/blockSwap (HCPoly/Entry/Setup/ProjectiveDistance.lean), not via explicitCanonicalMetric (an unrelated adapted-grid reference object).

Equations

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

Private helpers for K3 (the canonical comparison).

The route: 𝔡(X) ≤ c is equivalent to the Loewner inequality X ≤ c • (𝐑 X⁻¹ 𝐑), because with S := (𝐑 X 𝐑)^{1/2} one has S⁻¹S⁻¹ = 𝐑X⁻¹𝐑 and 𝔡(X) = ‖S X S‖, and congruence by S, resp. S⁻¹, turns each side into the other. Then M ≤ (1+η)A ≤ (1+η)(1+δ)·𝐑A⁻¹𝐑 ≤ (1+η)²(1+δ)·𝐑M⁻¹𝐑, the last step by antitonicity of the inverse and congruence by 𝐑; finally (1+η)² ≤ (1+η)³/(1-η).

theorem HCPolySupport.HighContrast.Multiscale.transpose_eq_of_psd {n : Type u_1} {P : Matrix n n ℝ} (hP : P.PosSemidef) : P.transpose = P

A positive semidefinite real matrix is symmetric.

theorem HCPolySupport.HighContrast.Multiscale.isHermitian_smul_one {n : Type u_1} [DecidableEq n] (c : ℝ) : (c • 1).IsHermitian

c • 1 is Hermitian, for any real scalar c.

theorem HCPolySupport.HighContrast.Multiscale.toLp_norm_sq {n : Type u_1} [Fintype n] (v : n → ℝ) : ‖WithLp.toLp 2 v‖ ^ 2 = v ⬝ᵥ v

The squared Euclidean-space norm of a vector equals its self dot product.

theorem HCPolySupport.HighContrast.Multiscale.vecSq_mulVec_le {n : Type u_1} [Fintype n] [DecidableEq n] (P : Matrix n n ℝ) (v : n → ℝ) : P.mulVec v ⬝ᵥ P.mulVec v ≤ ‖P‖ ^ 2 * v ⬝ᵥ v

(P v). (P v) ≤ ‖P‖² (v. v), from the operator-norm bound on P applied to v.

theorem HCPolySupport.HighContrast.Multiscale.opNorm_le_of_vecSq_le {n : Type u_1} [Fintype n] [DecidableEq n] {P : Matrix n n ℝ} {K : ℝ} (hK : 0 ≤ K) (h : ∀ (v : n → ℝ), P.mulVec v ⬝ᵥ P.mulVec v ≤ K ^ 2 * v ⬝ᵥ v) : ‖P‖ ≤ K

Conversely, a uniform bound (P v). (P v) ≤ K² (v. v) for all v bounds the operator norm ‖P‖ ≤ K.

theorem HCPolySupport.HighContrast.Multiscale.sqrt_form {n : Type u_1} [Fintype n] [DecidableEq n] {P : Matrix n n ℝ} (hP : P.PosSemidef) (v : n → ℝ) : (matSqrt P).mulVec v ⬝ᵥ (matSqrt P).mulVec v = v ⬝ᵥ P.mulVec v

The quadratic form of the matrix square root: (√P v). (√P v) = v. (P v), for P positive semidefinite.

theorem HCPolySupport.HighContrast.Multiscale.sqrt_norm {n : Type u_1} [Fintype n] [DecidableEq n] {P : Matrix n n ℝ} (hP : P.PosSemidef) : ‖P‖ = ‖matSqrt P‖ * ‖matSqrt P‖

‖P‖ = ‖√P‖ * ‖√P‖, for P positive semidefinite.

theorem HCPolySupport.HighContrast.Multiscale.psd_dot_le_opNorm {n : Type u_1} [Fintype n] [DecidableEq n] {P : Matrix n n ℝ} (hP : P.PosSemidef) (v : n → ℝ) : v ⬝ᵥ P.mulVec v ≤ ‖P‖ * v ⬝ᵥ v

For a positive semidefinite P, the quadratic form is bounded by the operator norm.

theorem HCPolySupport.HighContrast.Multiscale.opNorm_le_of_psd_dot_le {n : Type u_1} [Fintype n] [DecidableEq n] {P : Matrix n n ℝ} (hP : P.PosSemidef) {K : ℝ} (hK : 0 ≤ K) (h : ∀ (v : n → ℝ), v ⬝ᵥ P.mulVec v ≤ K * v ⬝ᵥ v) : ‖P‖ ≤ K

Conversely a bound on the quadratic form bounds the operator norm.

theorem HCPolySupport.HighContrast.Multiscale.dot_le_of_le_smul_one {n : Type u_1} [Fintype n] [DecidableEq n] {P : Matrix n n ℝ} {c : ℝ} (h : P ≤ c • 1) (v : n → ℝ) : v ⬝ᵥ P.mulVec v ≤ c * v ⬝ᵥ v

P ≤ c • 1 implies the quadratic form bound v. (P v) ≤ c (v. v).

theorem HCPolySupport.HighContrast.Multiscale.le_smul_one_of_dot_le {n : Type u_1} [Fintype n] [DecidableEq n] {P : Matrix n n ℝ} (hP : P.IsHermitian) {c : ℝ} (h : ∀ (v : n → ℝ), v ⬝ᵥ P.mulVec v ≤ c * v ⬝ᵥ v) : P ≤ c • 1

Conversely, a uniform quadratic form bound v. (P v) ≤ c (v. v) for Hermitian P implies P ≤ c • 1.

theorem HCPolySupport.HighContrast.Multiscale.psd_smul {n : Type u_1} [Finite n] {N : Matrix n n ℝ} (hN : N.PosSemidef) {c : ℝ} (hc : 0 ≤ c) : (c • N).PosSemidef

A nonnegative scalar multiple of a positive semidefinite matrix is positive semidefinite.

theorem HCPolySupport.HighContrast.Multiscale.posDef_smul {n : Type u_1} [Finite n] {c : ℝ} (hc : 0 < c) {X : Matrix n n ℝ} (hX : X.PosDef) : (c • X).PosDef

A positive scalar multiple of a positive definite matrix is positive definite.

theorem HCPolySupport.HighContrast.Multiscale.smul_le_smul_left {n : Type u_1} [Finite n] {X Y : Matrix n n ℝ} {c : ℝ} (hc : 0 ≤ c) (h : X ≤ Y) : c • X ≤ c • Y

Scalar multiplication by a nonnegative c preserves the Loewner order: X ≤ Y implies c • X ≤ c • Y.

theorem HCPolySupport.HighContrast.Multiscale.smul_le_smul_psd {n : Type u_1} [Finite n] {N : Matrix n n ℝ} (hN : N.PosSemidef) {a b : ℝ} (hab : a ≤ b) : a • N ≤ b • N

For N positive semidefinite, a ≤ b implies a • N ≤ b • N.

theorem HCPolySupport.HighContrast.Multiscale.posDef_of_le {n : Type u_1} [Finite n] {X Y : Matrix n n ℝ} (hX : X.PosDef) (hY : Y.IsHermitian) (h : X ≤ Y) : Y.PosDef

A Hermitian matrix above a positive definite one, in the Loewner order, is itself positive definite.

theorem HCPolySupport.HighContrast.Multiscale.swap_hermitian (d : ℕ) : Matrix.IsHermitian (toFullBlockMat (blockSwap d))

The flattened swap block 𝐑 is Hermitian.

theorem HCPolySupport.HighContrast.Multiscale.swap_isUnit (d : ℕ) : IsUnit (toFullBlockMat (blockSwap d))

The flattened swap block 𝐑 is invertible, since it is its own inverse.

theorem HCPolySupport.HighContrast.Multiscale.swapConj_posSemidef {d : ℕ} {X : BlockMat d} (hX : Matrix.PosDef (toFullBlockMat X)) : (toFullBlockMat (blockSwap d) * (toFullBlockMat X)⁻¹ * toFullBlockMat (blockSwap d)).PosSemidef

The swap-conjugate 𝐑 X⁻¹ 𝐑 of the inverse of a positive definite flattened block is positive semidefinite.

theorem HCPolySupport.HighContrast.Multiscale.imbalance_data {d : ℕ} {X : BlockMat d} (hX : Matrix.PosDef (toFullBlockMat X)) : ∃ (S : Matrix (BlockCoord d) (BlockCoord d) ℝ), S.transpose = S ∧ S * S⁻¹ = 1 ∧ S⁻¹ * S = 1 ∧ S⁻¹ * S⁻¹ = toFullBlockMat (blockSwap d) * (toFullBlockMat X)⁻¹ * toFullBlockMat (blockSwap d) ∧ canonicalImbalance X = ‖S * toFullBlockMat X * S‖

The square root data behind the canonical imbalance of a positive block.

theorem HCPolySupport.HighContrast.Multiscale.le_of_imbalance_le {d : ℕ} {X : BlockMat d} (hX : Matrix.PosDef (toFullBlockMat X)) {c : ℝ} (h : canonicalImbalance X ≤ c) : toFullBlockMat X ≤ c • (toFullBlockMat (blockSwap d) * (toFullBlockMat X)⁻¹ * toFullBlockMat (blockSwap d))

𝔡(X) ≤ c implies the Loewner inequality X ≤ c • 𝐑X⁻¹𝐑.

theorem HCPolySupport.HighContrast.Multiscale.imbalance_le_of_le {d : ℕ} {X : BlockMat d} (hX : Matrix.PosDef (toFullBlockMat X)) {c : ℝ} (hc : 0 ≤ c) (h : toFullBlockMat X ≤ c • (toFullBlockMat (blockSwap d) * (toFullBlockMat X)⁻¹ * toFullBlockMat (blockSwap d))) : canonicalImbalance X ≤ c

Conversely the Loewner inequality X ≤ c • 𝐑X⁻¹𝐑 implies 𝔡(X) ≤ c.

theorem HCPolySupport.HighContrast.Multiscale.schur_cancel {d : ℕ} {E : BlockMat d} (hs : IsSymmetricBlockMat E) (hp : Book.Ch02.BlockPosDef E) : E.lowerRight * schurSkew E = -E.lowerLeft ∧ Matrix.conjTranspose (schurSkew E) * E.lowerRight = -E.upperRight

For a symmetric positive definite block E, the lower-right block cancels the skew Schur coefficient against the two off-diagonal blocks: L k = -lowerLeft and kᴴ L = -upperRight.

theorem HCPolySupport.HighContrast.Multiscale.normalized_le {n : Type u_1} [Fintype n] [DecidableEq n] {A B : Matrix n n ℝ} (hA : A.PosDef) (hB : B.PosDef) {c : ℝ} (hn : ‖matSqrt B⁻¹ * A * matSqrt B⁻¹‖ ≤ c) : A ≤ c • B

A norm bound on the B-normalized form √(B⁻¹) A √(B⁻¹) gives the Loewner bound A ≤ c • B, for A, B positive definite.

theorem HCPolySupport.HighContrast.Multiscale.inv_smul_real {n : Type u_1} [Fintype n] [DecidableEq n] {B : Matrix n n ℝ} (hB : B.PosDef) {c : ℝ} (hc : c ≠ 0) : (c • B)⁻¹ = c⁻¹ • B⁻¹

(c • B)⁻¹ = c⁻¹ • B⁻¹, for c ≠ 0 and B positive definite.

theorem HCPolySupport.HighContrast.Multiscale.canonical_dual_order {d : ℕ} {A : BlockMat d} (hs : IsSymmetricBlockMat A) (hp : Book.Ch02.BlockPosDef A) {c : ℝ} (hc : 0 < c) (h : canonicalImbalance A ≤ c) : toFullBlockMat (blockSwap d) * toFullBlockMat A * toFullBlockMat (blockSwap d) ≤ c • (toFullBlockMat A)⁻¹

𝔡(A) ≤ c implies the flattened Loewner bound 𝐑 A 𝐑 ≤ c • A⁻¹, for A symmetric positive definite.

theorem HCPolySupport.HighContrast.Multiscale.coupled_schur_le {d : ℕ} {A : BlockMat d} (hs : IsSymmetricBlockMat A) (hp : Book.Ch02.BlockPosDef A) {c : ℝ} (ho : toFullBlockMat (blockSwap d) * toFullBlockMat A * toFullBlockMat (blockSwap d) ≤ c • (toFullBlockMat A)⁻¹) : schurSigma A + Matrix.conjTranspose (schurSkew A + Matrix.conjTranspose (schurSkew A)) * A.lowerRight * (schurSkew A + Matrix.conjTranspose (schurSkew A)) ≤ c • A.lowerRight⁻¹

The flattened bound 𝐑 A 𝐑 ≤ c • A⁻¹ descends, via the block congruence V, to the Schur-complement bound schurSigma A + (k + kᴴ)ᴴ L (k + kᴴ) ≤ c • L⁻¹.

theorem HCPolySupport.HighContrast.Multiscale.skew_part {d : ℕ} (k : Mat d) : IsSkewMat (2⁻¹ • (k - matTranspose k))

The antisymmetrization (1/2) • (k - kᵀ) of a matrix k is skew.

theorem HCPolySupport.HighContrast.Multiscale.quarter_correction_le {d : ℕ} {A : BlockMat d} (hs : IsSymmetricBlockMat A) (hp : Book.Ch02.BlockPosDef A) : schurSigma A + matTranspose (schurSkew A - 2⁻¹ • (schurSkew A - matTranspose (schurSkew A))) * A.lowerRight * (schurSkew A - 2⁻¹ • (schurSkew A - matTranspose (schurSkew A))) ≤ schurSigma A + Matrix.conjTranspose (schurSkew A + Matrix.conjTranspose (schurSkew A)) * A.lowerRight * (schurSkew A + Matrix.conjTranspose (schurSkew A))

The Schur-complement bound built from the antisymmetrization of the skew Schur coefficient is Loewner-below the one built from k + kᴴ, since the two differ by a nonnegative multiple of a positive semidefinite quadratic form.

theorem HCPolySupport.HighContrast.Multiscale.blockContrast_sub_one_le_of_canonicalImbalance_le {d : ℕ} {A : BlockMat d} (hs : IsSymmetricBlockMat A) (hp : Book.Ch02.BlockPosDef A) {x : ℝ} (hx : 0 ≤ x) (h : canonicalImbalance A ≤ 1 + x) : blockContrast A - 1 ≤ 3 * x

K4. If the canonical imbalance of a symmetric positive definite block A is at most 1 + x, then its block contrast satisfies blockContrast A - 1 ≤ 3 * x.