Coarse-graining support: Support.Book.Ch02.Theorems.BasicVariationalIdentitiesDefinitions

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

structure HCPolySupport.Book.Ch02.ResponseBasicVariationalIdentitiesTheory {d : ℕ} (U : Domain d) (a : CoeffOn U) (M : CoarseMatrices d) : Prop

Public theorem package for Lemma l.basic.cg.identities.basic.definitions.

This packages exactly the basic variational identities of Section 2.3.1: the matrix order chain e.cg.bounds.basic.definitions, the second-variation identity e.quadresp.basic.definitions, the maximizer energy identity e.Jenergyv.basic.definitions, and the averaged-gradient/flux formulas e.v.spatial.averages.basic.definitions.

The canonical public theorem proving this package is responseBasicVariationalIdentitiesTheory in BasicVariationalIdentities.lean.

• matrix_identities : ResponseMatrixIdentities U a M
• sigmaStar_symm : Matrix.IsSymm M.sigmaStar
• harmonicMean_le_sigmaStar : MatLoewnerLE (averagedSymmPartInv U a)⁻¹ M.sigmaStar
• sigmaStar_le_sigma : MatLoewnerLE M.sigmaStar M.sigma
• sigma_le_b : MatLoewnerLE M.sigma M.b
• b_le_averagedSymmPartPlusCorrection : MatLoewnerLE M.b (averagedSymmPartPlusCorrection U a)
• second_variation (p q : Vec d) (v : Solution U a) : 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
• maximizer_energy (p q : Vec d) (v : Solution U a) : IsResponseMaximizer U a p q v → responseJ U a p q = 1 / 2 * variationEnergyValue U a v
• average_gradient (p q : Vec d) (v : Solution U a) : IsResponseMaximizer U a p q v → averageGradient U a v = -p + matVecMul M.sigmaStarInv (q + matVecMul M.kappa p)
• average_flux (p q : Vec d) (v : Solution U a) : IsResponseMaximizer U a p q v → averageFlux U a v = q - matVecMul (matTranspose M.kappa) (matVecMul M.sigmaStarInv q) - matVecMul M.b p

theorem HCPolySupport.Book.Ch02.ResponseBasicVariationalIdentitiesTheory.ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) {M : CoarseMatrices d} (hTheory : ResponseBasicVariationalIdentitiesTheory U a M) : ResponseBasicVariationalIdentitiesTheory U b M

The basic variational identities depend only on the coefficient field up to a.e. equality on the public domain. The matrix package is fixed; canonical packages can be rewritten separately by coarseMatrices_eq_ofAEEq.

theorem HCPolySupport.Book.Ch02.ResponseBasicVariationalIdentitiesTheory.iff_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) {M : CoarseMatrices d} : ResponseBasicVariationalIdentitiesTheory U a M ↔ ResponseBasicVariationalIdentitiesTheory U b M

A.e.-equivalent coefficient representatives satisfy the same basic variational theorem package for a fixed matrix package.

theorem HCPolySupport.Book.Ch02.ResponseBasicVariationalIdentitiesTheory.toResponseMatrixIdentities {d : ℕ} {U : Domain d} {a : CoeffOn U} {M : CoarseMatrices d} (h : ResponseBasicVariationalIdentitiesTheory U a M) : ResponseMatrixIdentities U a M

The basic variational identities contain the matrix-extraction identities.

theorem HCPolySupport.Book.Ch02.ResponseBasicVariationalIdentitiesTheory.secondVariation_eq {d : ℕ} {U : Domain d} {a : CoeffOn U} {M : CoarseMatrices d} (h : ResponseBasicVariationalIdentitiesTheory U a M) {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

Accessor for the second-variation identity e.quadresp.basic.definitions.

theorem HCPolySupport.Book.Ch02.ResponseBasicVariationalIdentitiesTheory.responseJ_eq_energy {d : ℕ} {U : Domain d} {a : CoeffOn U} {M : CoarseMatrices d} (h : ResponseBasicVariationalIdentitiesTheory U a M) {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

Accessor for the maximizer energy identity e.Jenergyv.basic.definitions.

theorem HCPolySupport.Book.Ch02.ResponseBasicVariationalIdentitiesTheory.averageGradient_eq {d : ℕ} {U : Domain d} {a : CoeffOn U} {M : CoarseMatrices d} (h : ResponseBasicVariationalIdentitiesTheory U a M) {p q : Vec d} {v : Solution U a} (hv : IsResponseMaximizer U a p q v) : averageGradient U a v = -p + matVecMul M.sigmaStarInv (q + matVecMul M.kappa p)

Accessor for the averaged-gradient formula in e.v.spatial.averages.basic.definitions.

theorem HCPolySupport.Book.Ch02.ResponseBasicVariationalIdentitiesTheory.averageFlux_eq {d : ℕ} {U : Domain d} {a : CoeffOn U} {M : CoarseMatrices d} (h : ResponseBasicVariationalIdentitiesTheory U a M) {p q : Vec d} {v : Solution U a} (hv : IsResponseMaximizer U a p q v) : averageFlux U a v = q - matVecMul (matTranspose M.kappa) (matVecMul M.sigmaStarInv q) - matVecMul M.b p

Accessor for the averaged-flux formula in e.v.spatial.averages.basic.definitions.