Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.Corrector.C1AdjacentExactMinimizer

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.Corrector.C1AdjacentExactMinimizer

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Adjacent exact finite-affine minimizers #

Exact minimizers on two consecutive centered cubes have controlled boundary slopes. The proof reads the boundary slope from the average gradient of the finite affine solution and estimates that average by the two residual energies.

source
theorem HCPolySupport.HighContrast.Root.euclideanNorm_cubeAverageVec_solutionGradient_le {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) (s : ℝ) (hs : 0 < s) (k : ℤ) (herror : scalarIdentityWeakError a s k ≤ 1) (w : Book.Ch03.CubeSolution (originCube d k) a) :
euclideanNorm (cubeAverageVec (originCube d k) w.toH1.grad) ≤ √(4 * ↑d) * Book.Ch03.h1EnergyNormOnCube (originCube d k) a w.toH1

On a scale where the scalar-identity weak error is at most one, the average gradient of a cube solution is controlled by its normalized coefficient energy with a dimension-only constant.