Documentation

LeanPool.HighContrastHomogenization.Support.Internal.Ch02.BasicVariationalIdentities

Coarse-graining support: Support.Internal.Ch02.BasicVariationalIdentities #

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

source
theorem HCPolySupport.Internal.Ch02.BookCh02.responseSecondVariation_eq_of_isEllipticFieldOn {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField) (p q : Vec d) (v : Book.Ch02.Solution U a) (hv : Book.Ch02.IsResponseMaximizer U a p q v) (w : Book.Ch02.Solution U a) :
Book.Ch02.responseJ U a p q - Book.Ch02.responseValue U a p q w = Book.Ch02.secondVariationEnergyValue U a v w
source
theorem HCPolySupport.Internal.Ch02.BookCh02.responseJ_eq_energy_of_isEllipticFieldOn {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField) (p q : Vec d) (v : Book.Ch02.Solution U a) (hv : Book.Ch02.IsResponseMaximizer U a p q v) :
Book.Ch02.responseJ U a p q = 1 / 2 * Book.Ch02.variationEnergyValue U a v
source
theorem HCPolySupport.Internal.Ch02.BookCh02.averageGradient_eq_of_isEllipticFieldOn {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField) (hS : IsSigmaStarCoarse U.carrier a.toCoeffField (sigmaStarCoarse U.carrier a.toCoeffField)) (hK : IsKappaCoarse U.carrier a.toCoeffField (sigmaStarCoarse U.carrier a.toCoeffField) (kappaCoarse U.carrier a.toCoeffField)) (hdet : IsUnit (Matrix.det (sigmaStarCoarse U.carrier a.toCoeffField))) (p q : Vec d) (v : Book.Ch02.Solution U a) (hv : Book.Ch02.IsResponseMaximizer U a p q v) :
Book.Ch02.averageGradient U a v = -p + matVecMul (Book.Ch02.coarseMatrices U a).sigmaStarInv (q + matVecMul (Book.Ch02.coarseMatrices U a).kappa p)
source
theorem HCPolySupport.Internal.Ch02.BookCh02.averageFlux_eq_of_isEllipticFieldOn {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField) (hS : IsSigmaStarCoarse U.carrier a.toCoeffField (sigmaStarCoarse U.carrier a.toCoeffField)) (hK : IsKappaCoarse U.carrier a.toCoeffField (sigmaStarCoarse U.carrier a.toCoeffField) (kappaCoarse U.carrier a.toCoeffField)) {sigma : Mat d} (hSigma : IsSigmaCoarse U.carrier a.toCoeffField sigma (sigmaStarCoarse U.carrier a.toCoeffField) (kappaCoarse U.carrier a.toCoeffField)) (hdet : IsUnit (Matrix.det (sigmaStarCoarse U.carrier a.toCoeffField))) (p q : Vec d) (v : Book.Ch02.Solution U a) (hv : Book.Ch02.IsResponseMaximizer U a p q v) :
Book.Ch02.averageFlux U a v = q - matVecMul (matTranspose (Book.Ch02.coarseMatrices U a).kappa) (matVecMul (Book.Ch02.coarseMatrices U a).sigmaStarInv q) - matVecMul (Book.Ch02.coarseMatrices U a).b p
source
theorem HCPolySupport.Internal.Ch02.BookCh02.responseBasicVariationalIdentitiesTheory_of_isEllipticFieldOn {d : ℕ} [NeZero d] (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField) :
Book.Ch02.ResponseBasicVariationalIdentitiesTheory U a (Book.Ch02.coarseMatrices U a)
source
theorem HCPolySupport.Internal.Ch02.BookCh02.responseBasicVariationalIdentitiesTheory_of_neZero {d : ℕ} [NeZero d] (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) :
Book.Ch02.ResponseBasicVariationalIdentitiesTheory U a (Book.Ch02.coarseMatrices U a)
source
theorem HCPolySupport.Internal.Ch02.BookCh02.responseBasicVariationalIdentitiesTheory {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) :
Book.Ch02.ResponseBasicVariationalIdentitiesTheory U a (Book.Ch02.coarseMatrices U a)