Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch02.Theorems.BasicVariationalIdentities

Coarse-graining support: Support.Book.Ch02.Theorems.BasicVariationalIdentities #

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

source
theorem HCPolySupport.Book.Ch02.responseBasicVariationalIdentitiesTheory {d : ℕ} (U : Domain d) (a : CoeffOn U) :
ResponseBasicVariationalIdentitiesTheory U a (coarseMatrices U a)

Public Chapter 2 basic variational identities for the canonical coarse-grained matrices.

source
theorem HCPolySupport.Book.Ch02.harmonicMean_le_sigmaStarCoarse {d : ℕ} (U : Domain d) (a : CoeffOn U) :
MatLoewnerLE (averagedSymmPartInv U a)⁻¹ (sigmaStarCoarse U a)

Public lower bound in the coarse matrix order chain e.cg.bounds.basic.definitions.

source
theorem HCPolySupport.Book.Ch02.sigmaStarCoarse_le_sigmaCoarse {d : ℕ} (U : Domain d) (a : CoeffOn U) :
MatLoewnerLE (sigmaStarCoarse U a) (sigmaCoarse U a)

Public non-obvious order in the coarse matrix chain e.cg.bounds.basic.definitions.

source
theorem HCPolySupport.Book.Ch02.sigmaCoarse_le_bCoarse {d : ℕ} (U : Domain d) (a : CoeffOn U) :
MatLoewnerLE (sigmaCoarse U a) (bCoarse U a)

Public derived-matrix order in e.cg.bounds.basic.definitions.

source
theorem HCPolySupport.Book.Ch02.bCoarse_le_averagedSymmPartPlusCorrection {d : ℕ} (U : Domain d) (a : CoeffOn U) :
MatLoewnerLE (bCoarse U a) (averagedSymmPartPlusCorrection U a)

Public upper bound in the coarse matrix order chain e.cg.bounds.basic.definitions.

source
theorem HCPolySupport.Book.Ch02.secondVariation_eq_of_isResponseMaximizer {d : ℕ} {U : Domain d} {a : CoeffOn U} {p q : Vec d} {v : Solution U a} (hv : IsResponseMaximizer U a p q v) (w : Solution U a) :
responseJ U a p q - responseValue U a p q w = secondVariationEnergyValue U a v w

Public second-variation identity e.quadresp.basic.definitions.

source
theorem HCPolySupport.Book.Ch02.responseJ_eq_energy_of_isResponseMaximizer {d : ℕ} {U : Domain d} {a : CoeffOn U} {p q : Vec d} {v : Solution U a} (hv : IsResponseMaximizer U a p q v) :
responseJ U a p q = 1 / 2 * variationEnergyValue U a v

Public maximizer-energy identity e.Jenergyv.basic.definitions.

source
theorem HCPolySupport.Book.Ch02.averageGradient_eq_of_isResponseMaximizer {d : ℕ} {U : Domain d} {a : CoeffOn U} {p q : Vec d} {v : Solution U a} (hv : IsResponseMaximizer U a p q v) :
averageGradient U a v = -p + matVecMul (sigmaStarInvCoarse U a) (q + matVecMul (kappaCoarse U a) p)

Public averaged-gradient formula e.v.spatial.averages.basic.definitions.

source
theorem HCPolySupport.Book.Ch02.averageFlux_eq_of_isResponseMaximizer {d : ℕ} {U : Domain d} {a : CoeffOn U} {p q : Vec d} {v : Solution U a} (hv : IsResponseMaximizer U a p q v) :
averageFlux U a v = q - matVecMul (matTranspose (kappaCoarse U a)) (matVecMul (sigmaStarInvCoarse U a) q) - matVecMul (bCoarse U a) p

Public averaged-flux formula e.v.spatial.averages.basic.definitions.

source
theorem HCPolySupport.Book.Ch02.averageGradient_canonicalMaximizer_eq {d : ℕ} (U : Domain d) (a : CoeffOn U) (p q : Vec d) :
averageGradient U a (canonicalMaximizer ⋯ p q).toSolution = -p + matVecMul (sigmaStarInvCoarse U a) (q + matVecMul (kappaCoarse U a) p)

The whole-domain averaged gradient of the public canonical maximizer is the canonical coarse-matrix formula. This is a finite-dimensional consequence of the variational identities; it is not a measurable-selection statement for the maximizer field.

source
theorem HCPolySupport.Book.Ch02.averageFlux_canonicalMaximizer_eq {d : ℕ} (U : Domain d) (a : CoeffOn U) (p q : Vec d) :
averageFlux U a (canonicalMaximizer ⋯ p q).toSolution = q - matVecMul (matTranspose (kappaCoarse U a)) (matVecMul (sigmaStarInvCoarse U a) q) - matVecMul (bCoarse U a) p

The whole-domain averaged flux of the public canonical maximizer is the canonical coarse-matrix formula.

source
theorem HCPolySupport.Book.Ch02.averageGradient_canonicalMaximizer_eq_blockMatrix {d : ℕ} (U : Domain d) (a : CoeffOn U) (p q : Vec d) :
averageGradient U a (canonicalMaximizer ⋯ p q).toSolution = -p + matVecMul (coarseBlockMatrix U a).lowerRight q - matVecMul (coarseBlockMatrix U a).lowerLeft p

Block-matrix form of averageGradient_canonicalMaximizer_eq. Chapter 4 uses this finite formula as the measurable representative of the whole-cube canonical averaged gradient.

source
theorem HCPolySupport.Book.Ch02.averageFlux_canonicalMaximizer_eq_blockMatrix {d : ℕ} (U : Domain d) (a : CoeffOn U) (p q : Vec d) :
averageFlux U a (canonicalMaximizer ⋯ p q).toSolution = q + matVecMul (coarseBlockMatrix U a).upperRight q - matVecMul (coarseBlockMatrix U a).upperLeft p

Block-matrix form of averageFlux_canonicalMaximizer_eq. Chapter 4 uses this finite formula as the measurable representative of the whole-cube canonical averaged flux.