Coarse-graining support: Support.Ambient.BlockMatrix

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

@[reducible, inline]

abbrev HCPolySupport.BlockCoord (d : ℕ) : Type

Coordinates for two copies of the d-dimensional coordinate space.

Equations

• HCPolySupport.BlockCoord d = (Fin d ⊕ Fin d)

@[reducible, inline]

abbrev HCPolySupport.FullBlockVec (d : ℕ) : Type

Real vectors indexed by the coordinates of both blocks.

Equations

• HCPolySupport.FullBlockVec d = (HCPolySupport.BlockCoord d → ℝ)

@[reducible, inline]

abbrev HCPolySupport.FullBlockMat (d : ℕ) : Type

Real matrices indexed by the coordinates of both blocks.

Equations

• HCPolySupport.FullBlockMat d = Matrix (HCPolySupport.BlockCoord d) (HCPolySupport.BlockCoord d) ℝ

def HCPolySupport.toFullBlockVec {d : ℕ} (X : BlockVec d) : FullBlockVec d

Represent a pair of vectors as one vector indexed by the two blocks.

Equations

• HCPolySupport.toFullBlockVec X (Sum.inl i) = X.1 i
• HCPolySupport.toFullBlockVec X (Sum.inr i) = X.2 i

def HCPolySupport.ofFullBlockVec {d : ℕ} (x : FullBlockVec d) : BlockVec d

Split a vector indexed by both blocks into its two component vectors.

Equations

• HCPolySupport.ofFullBlockVec x = (fun (i : Fin d) => x (Sum.inl i), fun (i : Fin d) => x (Sum.inr i))

def HCPolySupport.toFullBlockMat {d : ℕ} (A : BlockMat d) : FullBlockMat d

Represent the four blocks as a single matrix on block coordinates.

Equations

• HCPolySupport.toFullBlockMat A (Sum.inl i) (Sum.inl j) = A.upperLeft i j
• HCPolySupport.toFullBlockMat A (Sum.inl i) (Sum.inr j) = A.upperRight i j
• HCPolySupport.toFullBlockMat A (Sum.inr i) (Sum.inl j) = A.lowerLeft i j
• HCPolySupport.toFullBlockMat A (Sum.inr i) (Sum.inr j) = A.lowerRight i j

def HCPolySupport.ofFullBlockMat {d : ℕ} (M : FullBlockMat d) : BlockMat d

Extract the four component blocks of a matrix on block coordinates.

Equations

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

def HCPolySupport.blockMatEntry {d : ℕ} (A : BlockMat d) : BlockCoord d → BlockCoord d → ℝ

The matrix entry selected by a pair of block coordinates.

Equations

• HCPolySupport.blockMatEntry A (Sum.inl i) (Sum.inl j) = A.upperLeft i j
• HCPolySupport.blockMatEntry A (Sum.inl i) (Sum.inr j) = A.upperRight i j
• HCPolySupport.blockMatEntry A (Sum.inr i) (Sum.inl j) = A.lowerLeft i j
• HCPolySupport.blockMatEntry A (Sum.inr i) (Sum.inr j) = A.lowerRight i j

def HCPolySupport.blockBasis {d : ℕ} : BlockCoord d → BlockVec d

The standard basis vector in the specified component of a vector pair.

Equations

• HCPolySupport.blockBasis (Sum.inl i) = (Pi.single i 1, 0)
• HCPolySupport.blockBasis (Sum.inr i) = (0, Pi.single i 1)

def HCPolySupport.IsSymmetricBlockMat {d : ℕ} (A : BlockMat d) : Prop

Symmetry of all matrix entries under interchange of block coordinates.

Equations

• HCPolySupport.IsSymmetricBlockMat A = ∀ (α β : HCPolySupport.BlockCoord d), HCPolySupport.blockMatEntry A α β = HCPolySupport.blockMatEntry A β α

@[simp]

theorem HCPolySupport.toFullBlockVec_ofFullBlockVec {d : ℕ} (x : FullBlockVec d) : toFullBlockVec (ofFullBlockVec x) = x

@[simp]

theorem HCPolySupport.ofFullBlockVec_toFullBlockVec {d : ℕ} (X : BlockVec d) : ofFullBlockVec (toFullBlockVec X) = X

@[simp]

theorem HCPolySupport.ofFullBlockVec_add {d : ℕ} (x y : FullBlockVec d) : ofFullBlockVec (x + y) = ofFullBlockVec x + ofFullBlockVec y

@[simp]

theorem HCPolySupport.ofFullBlockVec_smul {d : ℕ} (c : ℝ) (x : FullBlockVec d) : ofFullBlockVec (c • x) = c • ofFullBlockVec x

@[simp]

theorem HCPolySupport.toFullBlockMat_ofFullBlockMat {d : ℕ} (M : FullBlockMat d) : toFullBlockMat (ofFullBlockMat M) = M

@[simp]

theorem HCPolySupport.ofFullBlockMat_toFullBlockMat {d : ℕ} (A : BlockMat d) : ofFullBlockMat (toFullBlockMat A) = A

@[simp]

theorem HCPolySupport.blockMatEntry_ofFullBlockMat {d : ℕ} (M : FullBlockMat d) (α β : BlockCoord d) : blockMatEntry (ofFullBlockMat M) α β = M α β

theorem HCPolySupport.dotProduct_toFullBlockVec {d : ℕ} (X Y : BlockVec d) : toFullBlockVec X ⬝ᵥ toFullBlockVec Y = blockVecDot X Y

theorem HCPolySupport.toFullBlockVec_blockMatVecMul {d : ℕ} (A : BlockMat d) (X : BlockVec d) : toFullBlockVec (blockMatVecMul A X) = Matrix.mulVec (toFullBlockMat A) (toFullBlockVec X)

theorem HCPolySupport.blockVecDot_blockMatVecMul_eq_toLinearMap₂' {d : ℕ} (A : BlockMat d) (X Y : BlockVec d) : blockVecDot X (blockMatVecMul A Y) = (((Matrix.toLinearMap₂' ℝ) (toFullBlockMat A)) (toFullBlockVec X)) (toFullBlockVec Y)

theorem HCPolySupport.isSymmetricBlockMat_of_isSymm {d : ℕ} {M : FullBlockMat d} (hM : Matrix.IsSymm M) : IsSymmetricBlockMat (ofFullBlockMat M)

theorem HCPolySupport.isSymmetricBlockMat_ofFullBlockMat_sub {d : ℕ} {A B : BlockMat d} (hA : IsSymmetricBlockMat A) (hB : IsSymmetricBlockMat B) : IsSymmetricBlockMat (ofFullBlockMat (toFullBlockMat A - toFullBlockMat B))

theorem HCPolySupport.vecDot_single_left {d : ℕ} (i : Fin d) (y : Vec d) : vecDot (Pi.single i 1) y = y i

theorem HCPolySupport.vecDot_single_right {d : ℕ} (x : Vec d) (i : Fin d) : vecDot x (Pi.single i 1) = x i

theorem HCPolySupport.matVecMul_single {d : ℕ} (A : Mat d) (j : Fin d) : matVecMul A (Pi.single j 1) = fun (i : Fin d) => A i j

theorem HCPolySupport.matVecMul_zero {d : ℕ} (A : Mat d) : matVecMul A 0 = 0

theorem HCPolySupport.add_matVecMul {d : ℕ} (A B : Mat d) (x : Vec d) : matVecMul (A + B) x = matVecMul A x + matVecMul B x

theorem HCPolySupport.smul_matVecMul {d : ℕ} (c : ℝ) (A : Mat d) (x : Vec d) : matVecMul (c • A) x = c • matVecMul A x

theorem HCPolySupport.neg_matVecMul {d : ℕ} (A : Mat d) (x : Vec d) : matVecMul (-A) x = -matVecMul A x

theorem HCPolySupport.sub_matVecMul {d : ℕ} (A B : Mat d) (x : Vec d) : matVecMul (A - B) x = matVecMul A x - matVecMul B x

theorem HCPolySupport.vecDot_zero_left {d : ℕ} (y : Vec d) : vecDot 0 y = 0

theorem HCPolySupport.vecDot_zero_right {d : ℕ} (x : Vec d) : vecDot x 0 = 0

theorem HCPolySupport.vecDot_comm {d : ℕ} (x y : Vec d) : vecDot x y = vecDot y x

theorem HCPolySupport.matVecMul_add {d : ℕ} (A : Mat d) (x y : Vec d) : matVecMul A (x + y) = matVecMul A x + matVecMul A y

theorem HCPolySupport.matVecMul_smul {d : ℕ} (A : Mat d) (c : ℝ) (x : Vec d) : matVecMul A (c • x) = c • matVecMul A x

theorem HCPolySupport.matVecMul_neg {d : ℕ} (A : Mat d) (x : Vec d) : matVecMul A (-x) = -matVecMul A x

theorem HCPolySupport.matVecMul_mul {d : ℕ} (A B : Mat d) (x : Vec d) : matVecMul A (matVecMul B x) = matVecMul (A * B) x

theorem HCPolySupport.vecDot_add_left {d : ℕ} (x y z : Vec d) : vecDot (x + y) z = vecDot x z + vecDot y z

theorem HCPolySupport.vecDot_add_right {d : ℕ} (x y z : Vec d) : vecDot x (y + z) = vecDot x y + vecDot x z

theorem HCPolySupport.vecDot_smul_left {d : ℕ} (c : ℝ) (x y : Vec d) : vecDot (c • x) y = c * vecDot x y

theorem HCPolySupport.vecDot_smul_right {d : ℕ} (x y : Vec d) (c : ℝ) : vecDot x (c • y) = c * vecDot x y

theorem HCPolySupport.vecDot_neg_left {d : ℕ} (x y : Vec d) : vecDot (-x) y = -vecDot x y

theorem HCPolySupport.vecDot_neg_right {d : ℕ} (x y : Vec d) : vecDot x (-y) = -vecDot x y

theorem HCPolySupport.vecDot_matVecMul_transpose {d : ℕ} (x y : Vec d) (A : Mat d) : vecDot x (matVecMul (matTranspose A) y) = vecDot (matVecMul A x) y

theorem HCPolySupport.transpose_mul_symm_mul_isSymm {d : ℕ} (K S : Mat d) (hS : Matrix.IsSymm S) : (matTranspose K * S * K).IsSymm

theorem HCPolySupport.isUnit_det_smul {d : ℕ} {A : Mat d} (hdet : IsUnit (Matrix.det A)) {c : ℝ} (hc : c ≠ 0) : IsUnit (Matrix.det (c • A))

theorem HCPolySupport.nonsing_inv_smul {d : ℕ} {A : Mat d} (c : ℝ) (hc : c ≠ 0) (hdet : IsUnit (Matrix.det A)) : (c • A)⁻¹ = c⁻¹ • A⁻¹

theorem HCPolySupport.basis_sum_pairing {d : ℕ} (M : Mat d) (i j : Fin d) : vecDot (Pi.single i 1 + Pi.single j 1) (matVecMul M (Pi.single i 1 + Pi.single j 1)) = M i i + M i j + M j i + M j j

theorem HCPolySupport.blockMatVecMul_add {d : ℕ} (A : BlockMat d) (X Y : BlockVec d) : blockMatVecMul A (X + Y) = blockMatVecMul A X + blockMatVecMul A Y

theorem HCPolySupport.blockMatVecMul_ofFullBlockMat_sub {d : ℕ} (A B : BlockMat d) (X : BlockVec d) : blockMatVecMul (ofFullBlockMat (toFullBlockMat A - toFullBlockMat B)) X = blockMatVecMul A X - blockMatVecMul B X

theorem HCPolySupport.blockVecDot_add_left {d : ℕ} (X Y Z : BlockVec d) : blockVecDot (X + Y) Z = blockVecDot X Z + blockVecDot Y Z

theorem HCPolySupport.blockVecDot_add_right {d : ℕ} (X Y Z : BlockVec d) : blockVecDot X (Y + Z) = blockVecDot X Y + blockVecDot X Z

theorem HCPolySupport.blockVecDot_sub_right {d : ℕ} (X Y Z : BlockVec d) : blockVecDot X (Y - Z) = blockVecDot X Y - blockVecDot X Z

theorem HCPolySupport.blockVecDot_comm {d : ℕ} (X Y : BlockVec d) : blockVecDot X Y = blockVecDot Y X

@[simp]

theorem HCPolySupport.blockVecDot_swap_right {d : ℕ} (X Y : BlockVec d) : blockVecDot X (Prod.swap Y) = blockVecDot (X.2, X.1) Y

theorem HCPolySupport.blockMatVecMul_smul {d : ℕ} (A : BlockMat d) (c : ℝ) (X : BlockVec d) : blockMatVecMul A (c • X) = c • blockMatVecMul A X

theorem HCPolySupport.blockVecDot_smul_left {d : ℕ} (c : ℝ) (X Y : BlockVec d) : blockVecDot (c • X) Y = c * blockVecDot X Y

theorem HCPolySupport.blockVecDot_smul_right {d : ℕ} (X Y : BlockVec d) (c : ℝ) : blockVecDot X (c • Y) = c * blockVecDot X Y

theorem HCPolySupport.blockVecDot_blockMatVecMul_ofFullBlockMat_sub {d : ℕ} (A B : BlockMat d) (X : BlockVec d) : blockVecDot X (blockMatVecMul (ofFullBlockMat (toFullBlockMat A - toFullBlockMat B)) X) = blockVecDot X (blockMatVecMul A X) - blockVecDot X (blockMatVecMul B X)

theorem HCPolySupport.blockVecDot_blockMatVecMul_sub_eq_ofFullBlockMat_sub {d : ℕ} (A B : BlockMat d) (X : BlockVec d) : blockVecDot X (blockMatVecMul A X) - blockVecDot X (blockMatVecMul B X) = blockVecDot X (blockMatVecMul (ofFullBlockMat (toFullBlockMat A - toFullBlockMat B)) X)

theorem HCPolySupport.blockVecDot_nonneg {d : ℕ} (X : BlockVec d) : 0 ≤ blockVecDot X X

theorem HCPolySupport.sq_blockVecDot_le_blockVecDot_mul_blockVecDot {d : ℕ} (X Y : BlockVec d) : blockVecDot X Y ^ 2 ≤ blockVecDot X X * blockVecDot Y Y

theorem HCPolySupport.blockVecDot_sub_self_le {d : ℕ} (X Y : BlockVec d) : blockVecDot (X - Y) (X - Y) ≤ 2 * (blockVecDot X X + blockVecDot Y Y)

def HCPolySupport.blockMatLinearMap {d : ℕ} (A : BlockMat d) : BlockVec d →ₗ[ℝ] BlockVec d

A block matrix acts linearly on doubled vectors.

Equations

• HCPolySupport.blockMatLinearMap A = { toFun := HCPolySupport.blockMatVecMul A, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem HCPolySupport.blockMatLinearMap_apply {d : ℕ} (A : BlockMat d) (X : BlockVec d) : (blockMatLinearMap A) X = blockMatVecMul A X

noncomputable def HCPolySupport.blockMatContinuousLinearMap {d : ℕ} (A : BlockMat d) : BlockVec d →L[ℝ] BlockVec d

A block matrix acts continuously on doubled vectors. Continuity is automatic because the carrier is finite-dimensional.

Equations

• HCPolySupport.blockMatContinuousLinearMap A = { toLinearMap := HCPolySupport.blockMatLinearMap A, cont := ⋯ }

@[simp]

theorem HCPolySupport.blockMatContinuousLinearMap_apply {d : ℕ} (A : BlockMat d) (X : BlockVec d) : (blockMatContinuousLinearMap A) X = blockMatVecMul A X

theorem HCPolySupport.blockBasis_pairing {d : ℕ} (A : BlockMat d) (α β : BlockCoord d) : blockVecDot (blockBasis α) (blockMatVecMul A (blockBasis β)) = blockMatEntry A α β

theorem HCPolySupport.blockBasis_sum_pairing {d : ℕ} (A : BlockMat d) (α β : BlockCoord d) : blockVecDot (blockBasis α + blockBasis β) (blockMatVecMul A (blockBasis α + blockBasis β)) = blockMatEntry A α α + blockMatEntry A α β + blockMatEntry A β α + blockMatEntry A β β

def HCPolySupport.blockReflect {d : ℕ} (A : BlockMat d) : BlockMat d

The block matrix obtained by exchanging the first and second blocks in both indices.

Equations

• HCPolySupport.blockReflect A = { upperLeft := A.lowerRight, upperRight := A.lowerLeft, lowerLeft := A.upperRight, lowerRight := A.upperLeft }

theorem HCPolySupport.isSymmetricBlockMat_blockReflect {d : ℕ} {A : BlockMat d} (hA : IsSymmetricBlockMat A) : IsSymmetricBlockMat (blockReflect A)

@[simp]

theorem HCPolySupport.blockReflect_upperLeft {d : ℕ} (A : BlockMat d) : (blockReflect A).upperLeft = A.lowerRight

@[simp]

theorem HCPolySupport.blockReflect_upperRight {d : ℕ} (A : BlockMat d) : (blockReflect A).upperRight = A.lowerLeft

@[simp]

theorem HCPolySupport.blockReflect_lowerLeft {d : ℕ} (A : BlockMat d) : (blockReflect A).lowerLeft = A.upperRight

@[simp]

theorem HCPolySupport.blockReflect_lowerRight {d : ℕ} (A : BlockMat d) : (blockReflect A).lowerRight = A.upperLeft

@[simp]

theorem HCPolySupport.blockReflect_blockReflect {d : ℕ} (A : BlockMat d) : blockReflect (blockReflect A) = A

def HCPolySupport.MatLoewnerLE {d : ℕ} (A B : Mat d) : Prop

Löwner order on finite-dimensional real matrices, expressed through the quadratic form \frac12 x \cdot A x.

Equations

• HCPolySupport.MatLoewnerLE A B = ∀ (x : HCPolySupport.Vec d), 1 / 2 * HCPolySupport.vecDot x (HCPolySupport.matVecMul A x) ≤ 1 / 2 * HCPolySupport.vecDot x (HCPolySupport.matVecMul B x)

def HCPolySupport.BlockMatLoewnerLE {d : ℕ} (A B : BlockMat d) : Prop

Löwner order on doubled block matrices, expressed through the quadratic form \frac12 X \cdot \mathbf A X.

Equations

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

theorem HCPolySupport.MatLoewnerLE.refl {d : ℕ} (A : Mat d) : MatLoewnerLE A A

theorem HCPolySupport.MatLoewnerLE.trans {d : ℕ} {A B C : Mat d} (hAB : MatLoewnerLE A B) (hBC : MatLoewnerLE B C) : MatLoewnerLE A C

theorem HCPolySupport.BlockMatLoewnerLE.refl {d : ℕ} (A : BlockMat d) : BlockMatLoewnerLE A A

theorem HCPolySupport.BlockMatLoewnerLE.trans {d : ℕ} {A B C : BlockMat d} (hAB : BlockMatLoewnerLE A B) (hBC : BlockMatLoewnerLE B C) : BlockMatLoewnerLE A C

@[simp]

theorem HCPolySupport.blockMatVecMul_blockReflect {d : ℕ} (A : BlockMat d) (X : BlockVec d) : blockMatVecMul (blockReflect A) X = Prod.swap (blockMatVecMul A (X.2, X.1))

theorem HCPolySupport.blockVecDot_blockMatVecMul_blockReflect {d : ℕ} (A : BlockMat d) (X : BlockVec d) : blockVecDot X (blockMatVecMul (blockReflect A) X) = blockVecDot (X.2, X.1) (blockMatVecMul A (X.2, X.1))

theorem HCPolySupport.blockMat_ext {d : ℕ} {A B : BlockMat d} (hUL : A.upperLeft = B.upperLeft) (hUR : A.upperRight = B.upperRight) (hLL : A.lowerLeft = B.lowerLeft) (hLR : A.lowerRight = B.lowerRight) : A = B