Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.CorrectorDecay.LawFreeCoarsePoincare

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.CorrectorDecay.LawFreeCoarsePoincare

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

source
theorem HCPolySupport.HighContrast.exists_lawFreeCoarsePoincareRowsConstant (d : ℕ) [NeZero d] (s : ℝ) (hs : 0 < s) :
∃ (C : ℝ), 0 < C ∧ ∀ (a : Book.Ch02.TriadicCoeffFamily d) (k : ℤ) (u : Book.Ch03.CubeSolution (originCube d k) a), scalarIdentityWeakError a s k ≤ 1 → cubeScaleNormalizedDualNegativeBesovVectorNormTwo (originCube d k) s u.toH1.grad ≤ C * Book.Ch03.h1EnergyNormOnCube (originCube d k) a u.toH1 ∧ (cubeScaleNormalizedDualNegativeBesovVectorNormTwo (originCube d k) s fun (x : Vec d) => matVecMul (Book.Ch03.publicCoeffField (originCube d k) a x) (u.toH1.grad x)) ≤ C * Book.Ch03.h1EnergyNormOnCube (originCube d k) a u.toH1

At a scalar-identity good scale, the coarse-Poincare gradient and flux rows have a dimension/order-only energy bound. In particular, neither microscopic ellipticity constant enters the multiplier.