Documentation

LeanPool.HighContrastHomogenization.Provider.PolynomialHomogenization.Root.CorrectorDecay.IdentityAffineReplacement

High-contrast homogenization: #

Provider.PolynomialHomogenization.Root.CorrectorDecay.IdentityAffineReplacement

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

source
theorem HCPolySupport.HighContrast.identityHarmonicReplacementDatum_affine_grad_ae {d : ℕ} [NeZero d] (a : Book.Ch03.CoeffFamily d) (m : ℤ) (e : Vec d) :
let u := (finiteAffineSolution a m e).toH1; have hu := ⋯; have W := identityHarmonicReplacementDatum a m u hu; W.v.grad =ᵐ[volumeMeasureOn (cubeSet (originCube d m))] fun (x : Vec d) => e

The exact identity-harmonic replacement of a finite affine solution has the prescribed affine gradient.

source
theorem HCPolySupport.HighContrast.identityHarmonicReplacementDatum_affine_toFun_ae {d : ℕ} [NeZero d] (a : Book.Ch03.CoeffFamily d) (m : ℤ) (e : Vec d) :
let u := (finiteAffineSolution a m e).toH1; have hu := ⋯; have W := identityHarmonicReplacementDatum a m u hu; W.v.toFun =ᵐ[volumeMeasureOn (cubeSet (originCube d m))] (finiteAffineBoundaryH1 m e).toFun

The exact identity-harmonic replacement also has the prescribed affine value, not merely its gradient. The shared Dirichlet trace puts the difference in H¹₀, and the zero-gradient conclusion above then removes the otherwise possible additive constant.