Block Matrix

Support for the Armstrong–Vicol anomalous-diffusion formalization.

@[reducible, inline]

abbrev Homogenization.BlockCoord (d : ℕ) : Type

Coordinate indices for the two blocks of a doubled vector.

Equations

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

@[reducible, inline]

abbrev Homogenization.FullBlockVec (d : ℕ) : Type

Doubled vector represented by a function on the disjoint union of coordinate indices.

Equations

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

@[reducible, inline]

abbrev Homogenization.FullBlockMat (d : ℕ) : Type

Doubled matrix represented on the disjoint union of coordinate indices.

Equations

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

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

Flatten a pair of spatial vectors into a doubled coordinate vector.

Equations

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

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

Split a doubled coordinate vector into its two spatial blocks.

Equations

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

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

Flatten a block matrix into a matrix on doubled coordinate indices.

Equations

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

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

Split a doubled coordinate matrix into its four spatial matrix blocks.

Equations

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

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

Entry of a block matrix indexed by the doubled coordinate set.

Equations

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

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

Coordinate basis of the doubled vector space in block form.

Equations

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

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

Symmetry of all entries of a block matrix under exchange of coordinate indices.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem Homogenization.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 Homogenization.isSymmetricBlockMat_of_isSymm {d : ℕ} {M : FullBlockMat d} (hM : Matrix.IsSymm M) : IsSymmetricBlockMat (ofFullBlockMat M)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Homogenization.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 Homogenization.blockMatVecMul_add {d : ℕ} (A : BlockMat d) (X Y : BlockVec d) : blockMatVecMul A (X + Y) = blockMatVecMul A X + blockMatVecMul A Y

theorem Homogenization.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 Homogenization.blockVecDot_add_left {d : ℕ} (X Y Z : BlockVec d) : blockVecDot (X + Y) Z = blockVecDot X Z + blockVecDot Y Z

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

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

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

@[simp]

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

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

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

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

theorem Homogenization.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 Homogenization.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 Homogenization.blockVecDot_nonneg {d : ℕ} (X : BlockVec d) : 0 ≤ blockVecDot X X

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

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

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

A block matrix acts linearly on doubled vectors.

Equations

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

@[simp]

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

noncomputable def Homogenization.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

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

@[simp]

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

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

theorem Homogenization.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 Homogenization.blockReflect {d : ℕ} (A : BlockMat d) : BlockMat d

Exchange both input and output blocks of a block matrix.

Equations

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def Homogenization.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

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

def Homogenization.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 Homogenization.MatLoewnerLE.refl {d : ℕ} (A : Mat d) : MatLoewnerLE A A

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

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

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

@[simp]

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

theorem Homogenization.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 Homogenization.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