Documentation

LeanPool.HighContrastHomogenization.Support.CoarseGraining.Symmetric.Basic

Coarse-graining support: Support.CoarseGraining.Symmetric.Basic #

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

Symmetric coefficient fields #

This file contains the lightweight pointwise symmetry API used to specialize the general nonsymmetric coarse-graining definitions to symmetric coefficient fields.

source
def HCPolySupport.IsSymmetricCoeffField {d : ℕ} (a : CoeffField d) :
Prop

A coefficient field is symmetric if each pointwise coefficient matrix is symmetric.

Equations
Instances For
    source
    theorem HCPolySupport.IsSymmetricCoeffField.apply {d : ℕ} {a : CoeffField d} (ha : IsSymmetricCoeffField a) (x : Vec d) :
    Matrix.IsSymm (a x)
    source
    theorem HCPolySupport.IsSymmetricCoeffField.translateCoeffField {d : ℕ} {a : CoeffField d} (ha : IsSymmetricCoeffField a) (z : Vec d) :
    IsSymmetricCoeffField (HCPolySupport.translateCoeffField z a)
    source
    theorem HCPolySupport.isSymmetricCoeffField_iff_matTranspose_eq {d : ℕ} {a : CoeffField d} :
    IsSymmetricCoeffField a ↔ ∀ (x : Vec d), matTranspose (a x) = a x
    source
    theorem HCPolySupport.adjointCoeffField_eq_self_of_isSymmetricCoeffField {d : ℕ} {a : CoeffField d} (ha : IsSymmetricCoeffField a) :
    adjointCoeffField a = a
    source
    theorem HCPolySupport.symmPart_eq_self_of_isSymmetricCoeffField {d : ℕ} {a : CoeffField d} (ha : IsSymmetricCoeffField a) (x : Vec d) :
    symmPart (a x) = a x
    source
    theorem HCPolySupport.skewPart_eq_zero_of_isSymmetricCoeffField {d : ℕ} {a : CoeffField d} (ha : IsSymmetricCoeffField a) (x : Vec d) :
    skewPart (a x) = 0
    source
    theorem HCPolySupport.symmCoeffField_eq_self_of_isSymmetricCoeffField {d : ℕ} {a : CoeffField d} (ha : IsSymmetricCoeffField a) :
    symmCoeffField a = a
    source
    theorem HCPolySupport.skewCoeffField_eq_zero_of_isSymmetricCoeffField {d : ℕ} {a : CoeffField d} (ha : IsSymmetricCoeffField a) :
    skewCoeffField a = 0