Documentation

LeanPool.HighContrastHomogenization.Support.Book.Ch04.Theorems.CanonicalSolutions.AverageIdentities

Coarse-graining support: Support.Book.Ch04.Theorems.CanonicalSolutions.AverageIdentities #

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

source
theorem HCPolySupport.Book.Ch04.canonicalScalarResponseGradientAverageCubeSet_eq_cubeAverageVec_canonicalMaximizer {d : ℕ} [NeZero d] (aR : RegCoeffField d) (ha : AELocallyUniformlyEllipticField aR) {Q R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) (p q : Vec d) :
canonicalScalarResponseGradientAverageCubeSet Q R p q aR.toFun = cubeAverageVec R fun (x : Vec d) => (Ch02.canonicalMaximizer ⋯ p q).toSolution.toH1.grad x

Correctness of the Ch4 scalar-response gradient average: on the a.e. elliptic support it is the descendant-cube average of the raw Chapter 2 canonical scalar-response maximizer gradient.

source
theorem HCPolySupport.Book.Ch04.canonicalScalarResponseFluxAverageCubeSet_eq_cubeAverageVec_canonicalMaximizerFlux {d : ℕ} [NeZero d] (aR : RegCoeffField d) (ha : AELocallyUniformlyEllipticField aR) {Q R : TriadicCube d} {j : ℕ} (hR : R ∈ descendantsAtDepth Q j) (p q : Vec d) :
canonicalScalarResponseFluxAverageCubeSet Q R p q aR.toFun = cubeAverageVec R fun (x : Vec d) => matVecMul (((triadicCoeffFamilyOfAELocallyUniformlyEllipticField aR ha).coeffOn Q).toCoeffField x) ((Ch02.canonicalMaximizer ⋯ p q).toSolution.toH1.grad x)

Correctness of the Ch4 scalar-response flux average: on the a.e. elliptic support it is the descendant-cube average of the raw Chapter 2 canonical scalar-response maximizer flux.