Coarse-graining support: Support.Ambient.Basic

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

@[reducible, inline]

abbrev HCPolySupport.Vec (d : ℕ) : Type

Real coordinate vectors in dimension d.

Equations

• HCPolySupport.Vec d = (Fin d → ℝ)

@[reducible, inline]

abbrev HCPolySupport.Mat (d : ℕ) : Type

Real square matrices with d rows and columns.

Equations

• HCPolySupport.Mat d = Matrix (Fin d) (Fin d) ℝ

@[reducible, inline]

abbrev HCPolySupport.BlockVec (d : ℕ) : Type

Pairs of real d-dimensional vectors.

Equations

• HCPolySupport.BlockVec d = (HCPolySupport.Vec d × HCPolySupport.Vec d)

structure HCPolySupport.BlockMat (d : ℕ) : Type

A two-by-two block matrix with real d-by-d blocks.

• upperLeft : Mat d

  The block mapping the first input vector to the first output vector.

• upperRight : Mat d

  The block mapping the second input vector to the first output vector.

• lowerLeft : Mat d

  The block mapping the first input vector to the second output vector.

• lowerRight : Mat d

  The block mapping the second input vector to the second output vector.

@[instance_reducible]

instance HCPolySupport.instInhabitedBlockMat {a✝ : ℕ} : Inhabited (BlockMat a✝)

Equations

• HCPolySupport.instInhabitedBlockMat = { default := HCPolySupport.instInhabitedBlockMat.default }

def HCPolySupport.vecDot {d : ℕ} (x y : Vec d) : ℝ

The Euclidean dot product, given by the sum of coordinate products.

Equations

• HCPolySupport.vecDot x y = ∑ i : Fin d, x i * y i

def HCPolySupport.vecNormSq {d : ℕ} (x : Vec d) : ℝ

The squared Euclidean length of a vector.

Equations

• HCPolySupport.vecNormSq x = HCPolySupport.vecDot x x

theorem HCPolySupport.sq_vecDot_le_vecNormSq_mul_vecNormSq {d : ℕ} (x y : Vec d) : vecDot x y ^ 2 ≤ vecNormSq x * vecNormSq y

theorem HCPolySupport.vecNormSq_nonneg {d : ℕ} (x : Vec d) : 0 ≤ vecNormSq x

theorem HCPolySupport.sq_apply_le_vecNormSq {d : ℕ} (x : Vec d) (i : Fin d) : x i ^ 2 ≤ vecNormSq x

theorem HCPolySupport.abs_le_add_halves_of_sq_le_mul {u A B : ℝ} (hu_sq : u ^ 2 ≤ A * B) (hA : 0 ≤ A) (hB : 0 ≤ B) : |u| ≤ A / 2 + B / 2

A real Young inequality packaged for Cauchy-Schwarz consequences.

theorem HCPolySupport.abs_vecDot_le_add_halves_vecNormSq {d : ℕ} (x y : Vec d) : |vecDot x y| ≤ vecNormSq x / 2 + vecNormSq y / 2

Young's inequality for the Euclidean dot product on project vectors.

theorem HCPolySupport.abs_mul_mul_vecDot_le_add_halves_mul_sq_vecNormSq {d : ℕ} (a b : ℝ) (x y : Vec d) : |a * b * vecDot x y| ≤ a ^ 2 * vecNormSq x / 2 + b ^ 2 * vecNormSq y / 2

Young's inequality for scalar-weighted Euclidean dot products.

theorem HCPolySupport.vecNormSq_eq_zero {d : ℕ} {x : Vec d} (h : vecNormSq x = 0) : x = 0

theorem HCPolySupport.vecNormSq_eq_zero_iff {d : ℕ} {x : Vec d} : vecNormSq x = 0 ↔ x = 0

theorem HCPolySupport.vecNormSq_smul {d : ℕ} (c : ℝ) (x : Vec d) : vecNormSq (c • x) = c ^ 2 * vecNormSq x

theorem HCPolySupport.vecNormSq_add_le {d : ℕ} (x y : Vec d) : vecNormSq (x + y) ≤ 2 * (vecNormSq x + vecNormSq y)

theorem HCPolySupport.vecNormSq_four_add_le {d : ℕ} (w x y z : Vec d) : vecNormSq (w + x + y + z) ≤ 4 * (vecNormSq w + vecNormSq x + vecNormSq y + vecNormSq z)

Four-term Cauchy estimate for the squared Euclidean norm.

theorem HCPolySupport.vecNormSq_sub_le {d : ℕ} (x y : Vec d) : vecNormSq (x - y) ≤ 2 * (vecNormSq x + vecNormSq y)

def HCPolySupport.matVecMul {d : ℕ} (A : Mat d) (x : Vec d) : Vec d

Matrix multiplication applied to a coordinate vector.

Equations

• HCPolySupport.matVecMul A x i = ∑ j : Fin d, A i j * x j

def HCPolySupport.matTranspose {d : ℕ} (A : Mat d) : Mat d

The matrix obtained by interchanging row and column indices.

Equations

• HCPolySupport.matTranspose A = Matrix.transpose A

def HCPolySupport.blockVecDot {d : ℕ} (X Y : BlockVec d) : ℝ

The sum of the Euclidean dot products of the two vector components.

Equations

• HCPolySupport.blockVecDot X Y = HCPolySupport.vecDot X.1 Y.1 + HCPolySupport.vecDot X.2 Y.2

def HCPolySupport.blockMatVecMul {d : ℕ} (A : BlockMat d) (X : BlockVec d) : BlockVec d

The action of a two-by-two block matrix on a pair of vectors.

Equations

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

@[simp]

theorem HCPolySupport.blockMatVecMul_fst {d : ℕ} (A : BlockMat d) (p q : Vec d) : (blockMatVecMul A (p, q)).1 = matVecMul A.upperLeft p + matVecMul A.upperRight q

@[simp]

theorem HCPolySupport.blockMatVecMul_snd {d : ℕ} (A : BlockMat d) (p q : Vec d) : (blockMatVecMul A (p, q)).2 = matVecMul A.lowerLeft p + matVecMul A.lowerRight q

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

The symmetric part (A + Aᵀ) / 2 of a real matrix.

Equations

• HCPolySupport.symmPart A i j = (A i j + A j i) / 2

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

The skew-symmetric part (A - Aᵀ) / 2 of a real matrix.

Equations

• HCPolySupport.skewPart A i j = (A i j - A j i) / 2

theorem HCPolySupport.symmPart_eq_smul_add_transpose {d : ℕ} (A : Mat d) : symmPart A = (1 / 2) • (A + matTranspose A)

theorem HCPolySupport.skewPart_eq_smul_sub_transpose {d : ℕ} (A : Mat d) : skewPart A = (1 / 2) • (A - matTranspose A)

@[simp]

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

@[simp]

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