High-contrast homogenization: Annealed.SchattenDefinedness #

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

Definedness obligations for the Schatten encoding #

The Schatten norm is written with the continuous functional calculus of the square of a symmetric doubled block matrix. The calculus is a total function: off its predicate it returns zero, and the Schatten norm would then be zero rather than large. This file discharges the obligations that show the predicate is met at every argument the fixed-grid statements evaluate it on, so that the encoding never returns that value.

The chain is: a symmetric doubled block matrix is self-adjoint as a 2d × 2d real matrix; the positive semidefinite square root is symmetric, and remains so on its own junk branch, where it is the identity; conjugation by a symmetric matrix preserves symmetry, so the normalized block of a symmetric block by an arbitrary block is symmetric; and the square of a self-adjoint matrix is self-adjoint. The coarse response and the annealed block are symmetric with no hypothesis, so the conclusion is unconditional at every argument the fixed-grid statements form.

Symmetry and self-adjointness of a doubled block matrix #

source

theorem HCPolySupport.HighContrast.isSelfAdjoint_toFullBlockMat {d : ℕ} {A : BlockMat d} (hA : IsSymmetricBlockMat A) :

IsSelfAdjoint (toFullBlockMat A)

Obligation O1. A symmetric doubled block matrix is self-adjoint as a 2d × 2d real matrix; this is the predicate of the continuous functional calculus that the Schatten norm evaluates.

source

theorem HCPolySupport.HighContrast.isSelfAdjoint_mul_self {R : Type u_1} [Ring R] [StarRing R] {x : R} (hx : IsSelfAdjoint x) :

IsSelfAdjoint (x * x)

The square of a self-adjoint element is self-adjoint.

Obligation O2 — the square root and the normalization #

source

theorem HCPolySupport.HighContrast.isSymm_matSqrt {n : Type u_1} [Fintype n] [DecidableEq n] (M : Matrix n n ℝ) :

(matSqrt M).IsSymm

Obligation O2, first half. The positive semidefinite square root is symmetric — on positive semidefinite data because the root is, and off it because the junk value is the identity.

source