Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.Corrector.C1FiniteRateComposition

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.Corrector.C1FiniteRateComposition

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

Real-rate control of adjacent exact affine minimizers #

The finite affine excess decay and the dimension-only adjacent-minimizer estimate combine with one common smallness threshold. The scale gap is written from the outer cube inward, which is the geometric orientation used by the finite slope telescope.

source
noncomputable def HCPolySupport.HighContrast.Root.finiteAffineExactMinimizer {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {n m : ℤ} (hnm : n ≤ m) (u : Book.Ch03.CubeSolution (originCube d m) a) :
Vec d

A proof-irrelevant choice of an exact finite affine excess minimizer.

Equations
Instances For
    source
    theorem HCPolySupport.HighContrast.Root.finiteAffineExactMinimizer_spec {d : ℕ} [NeZero d] (a : Book.Ch02.TriadicCoeffFamily d) {n m : ℤ} (hnm : n ≤ m) (u : Book.Ch03.CubeSolution (originCube d m) a) :
    (weightedGradNorm (a.coeffOn (originCube d n)).toCoeffField (openCubeSet (originCube d n)) fun (x : Vec d) => u.toH1.grad x - (finiteAffineSolution a m (finiteAffineExactMinimizer a hnm u)).toH1.grad x) = finiteAffineGradientExcess a n m u

    The selected finite affine minimizer realizes the excess exactly.