Coarse-graining support: Support.CoarseGraining.BlockFormalism.Structures

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

Block formalism -- structures and private matrix helpers

BlockState structure, constVecField, blockMatrixOfCoeff / blockCoeffField definitions, plus symmPart / skewPart / inverse / conjugation helpers used throughout.

structure HCPolySupport.BlockState (d : ℕ) : Type

A pair of vector fields representing a potential component and a flux component.

• potential : Vec d → Vec d

  The vector field in the potential component of the block state.

• flux : Vec d → Vec d

  The vector field in the flux component of the block state.

theorem HCPolySupport.BlockState.ext {d : ℕ} {X Y : BlockState d} (hpot : X.potential = Y.potential) (hflux : X.flux = Y.flux) : X = Y

theorem HCPolySupport.BlockState.ext_iff {d : ℕ} {X Y : BlockState d} : X = Y ↔ X.potential = Y.potential ∧ X.flux = Y.flux

@[instance_reducible]

instance HCPolySupport.instAddBlockState {d : ℕ} : Add (BlockState d)

Equations

• HCPolySupport.instAddBlockState = { add := fun (X Y : HCPolySupport.BlockState d) => { potential := X.potential + Y.potential, flux := X.flux + Y.flux } }

@[instance_reducible]

instance HCPolySupport.instSMulRealBlockState {d : ℕ} : SMul ℝ (BlockState d)

Equations

• HCPolySupport.instSMulRealBlockState = { smul := fun (c : ℝ) (X : HCPolySupport.BlockState d) => { potential := c • X.potential, flux := c • X.flux } }

def HCPolySupport.BlockState.eval {d : ℕ} (X : BlockState d) (x : Vec d) : BlockVec d

The pair of potential and flux values at a point.

Equations

• X.eval x = (X.potential x, X.flux x)

@[simp]

theorem HCPolySupport.BlockState.eval_add {d : ℕ} (X Y : BlockState d) (x : Vec d) : (X + Y).eval x = X.eval x + Y.eval x

@[simp]

theorem HCPolySupport.BlockState.eval_smul {d : ℕ} (c : ℝ) (X : BlockState d) (x : Vec d) : (c • X).eval x = c • X.eval x

def HCPolySupport.BlockState.mapMatrix {d : ℕ} (R : Mat d) (X : BlockState d) : BlockState d

Apply the same matrix to both vector fields of a block state pointwise.

Equations

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

@[simp]

theorem HCPolySupport.BlockState.eval_mapMatrix {d : ℕ} (R : Mat d) (X : BlockState d) (x : Vec d) : (mapMatrix R X).eval x = (matVecMul R (X.potential x), matVecMul R (X.flux x))

def HCPolySupport.BlockState.flipFlux {d : ℕ} (X : BlockState d) : BlockState d

Negate the flux component of a block state.

Equations

• X.flipFlux = { potential := X.potential, flux := fun (x : HCPolySupport.Vec d) => -X.flux x }

@[simp]

theorem HCPolySupport.BlockState.eval_flipFlux {d : ℕ} (X : BlockState d) (x : Vec d) : X.flipFlux.eval x = (X.potential x, -X.flux x)

def HCPolySupport.constVecField {d : ℕ} (p : Vec d) : Vec d → Vec d

The constant vector field with value p.

Equations

• HCPolySupport.constVecField p x✝ = p

noncomputable def HCPolySupport.blockMatrixOfCoeff {d : ℕ} (A : Mat d) : BlockMat d

The block matrix with blocks s + kᵀ s⁻¹ k, -kᵀ s⁻¹, -s⁻¹ k, and s⁻¹, where s and k are the symmetric and skew parts of A.

Equations

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

noncomputable def HCPolySupport.blockCoeffField {d : ℕ} (a : CoeffField d) : Vec d → BlockMat d

The block coefficient field obtained by applying the block matrix construction pointwise.

Equations

• HCPolySupport.blockCoeffField a x = HCPolySupport.blockMatrixOfCoeff (a x)

def HCPolySupport.blockVecConj {d : ℕ} (R : Mat d) (X : BlockVec d) : BlockVec d

Apply R to each component of a vector pair.

Equations

• HCPolySupport.blockVecConj R X = (HCPolySupport.matVecMul R X.1, HCPolySupport.matVecMul R X.2)

def HCPolySupport.blockMatConj {d : ℕ} (R : Mat d) (B : BlockMat d) : BlockMat d

Multiply each block of B on both sides by R.

Equations

• HCPolySupport.blockMatConj R B = { upperLeft := R * B.upperLeft * R, upperRight := R * B.upperRight * R, lowerLeft := R * B.lowerLeft * R, lowerRight := R * B.lowerRight * R }

theorem HCPolySupport.symmPart_matTranspose {d : ℕ} (A : Mat d) : symmPart (matTranspose A) = symmPart A

theorem HCPolySupport.skewPart_matTranspose {d : ℕ} (A : Mat d) : skewPart (matTranspose A) = -skewPart A

theorem HCPolySupport.matTranspose_mul_mul_of_transpose_eq_self {d : ℕ} {R A : Mat d} (hR : matTranspose R = R) : matTranspose (R * A * R) = R * matTranspose A * R

theorem HCPolySupport.symmPart_mul_mul_of_transpose_eq_self {d : ℕ} {R A : Mat d} (hR : matTranspose R = R) : symmPart (R * A * R) = R * symmPart A * R

theorem HCPolySupport.skewPart_mul_mul_of_transpose_eq_self {d : ℕ} {R A : Mat d} (hR : matTranspose R = R) : skewPart (R * A * R) = R * skewPart A * R

theorem HCPolySupport.isUnit_det_mul_mul_iff_of_mul_self_eq_one {d : ℕ} {R A : Mat d} (hR2 : R * R = 1) : IsUnit (R * A * R).det ↔ IsUnit (Matrix.det A)

theorem HCPolySupport.nonsing_inv_mul_mul_of_mul_self_eq_one {d : ℕ} {R A : Mat d} (hR2 : R * R = 1) : (R * A * R)⁻¹ = R * A⁻¹ * R

theorem HCPolySupport.mul_mul_mul_conj_of_mul_self_eq_one {d : ℕ} {R B C : Mat d} (hR2 : R * R = 1) : R * B * R * (R * C * R) = R * (B * C) * R

theorem HCPolySupport.matVecMul_mul_mul_cancel_of_mul_self_eq_one {d : ℕ} {R A : Mat d} {x : Vec d} (hR2 : R * R = 1) : matVecMul (R * A * R) (matVecMul R x) = matVecMul R (matVecMul A x)

theorem HCPolySupport.vecDot_matVecMul_conj_of_transpose_eq_self_of_mul_self_eq_one {d : ℕ} {R : Mat d} (hR : matTranspose R = R) (hR2 : R * R = 1) (x y : Vec d) : vecDot (matVecMul R x) (matVecMul R y) = vecDot x y

@[simp]

theorem HCPolySupport.blockMatrixOfCoeff_matTranspose_upperLeft {d : ℕ} (A : Mat d) : (blockMatrixOfCoeff (matTranspose A)).upperLeft = (blockMatrixOfCoeff A).upperLeft

@[simp]

theorem HCPolySupport.blockMatrixOfCoeff_matTranspose_upperRight {d : ℕ} (A : Mat d) : (blockMatrixOfCoeff (matTranspose A)).upperRight = -(blockMatrixOfCoeff A).upperRight

@[simp]

theorem HCPolySupport.blockMatrixOfCoeff_matTranspose_lowerLeft {d : ℕ} (A : Mat d) : (blockMatrixOfCoeff (matTranspose A)).lowerLeft = -(blockMatrixOfCoeff A).lowerLeft