High-contrast homogenization:

Provider.PolynomialHomogenization.Root.CorrectorDecay.PhysicalClassBridge

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

theorem HCPolySupport.HighContrast.memVectorL2_globalGradient_originCube {d : ℕ} (z : NormalizedLocalH1Carrier d) (n : ℤ) : MemVectorL2 (openCubeSet (originCube d n)) z.globalGradientRepresentative

A canonical global gradient representative is square integrable on every integer-scale origin cube, including negative scales.

theorem HCPolySupport.HighContrast.correctorGradientOnOriginCube_eq_globalRepresentative {d : ℕ} (Phi : Vec d → NormalizedLocalH1Carrier d) (e : Vec d) (n : ℤ) : correctorGradientOnOriginCube Phi e n = toHilbertVectorL2OfVecField ⋯

The integer local component is exactly the L² class of the canonical global representative on that cube.

theorem HCPolySupport.HighContrast.localNegOneNorm_correctorGradient_eq_global {d : ℕ} (Phi : Vec d → NormalizedLocalH1Carrier d) (e : Vec d) (n : ℤ) : localNegOneNorm (openCubeSet (originCube d n)) (correctorGradientOnOriginCube Phi e n) = negOneNorm (openCubeSet (originCube d n)) (Phi e).globalGradientRepresentative

The local negative-one norm of the gradient class reads the canonical raw global gradient field.

theorem HCPolySupport.HighContrast.localNegOneNorm_correctorFlux_eq_global {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (Phi : Vec d → NormalizedLocalH1Carrier d) (e : Vec d) (n : ℤ) : localNegOneNorm (openCubeSet (originCube d n)) (scalarIdentityCorrectorFluxDefectOnOriginCube a Phi e n) = negOneNorm (openCubeSet (originCube d n)) fun (x : Vec d) => matVecMul ((a.coeffOn (originCube d n)).toCoeffField x) (e + (Phi e).globalGradientRepresentative x) - e

The local identity-flux class reads the literal cube-family coefficient times the canonical full gradient.

theorem HCPolySupport.HighContrast.triadicScaledNegOne_pair_eq_global {d : ℕ} (a : Book.Ch02.TriadicCoeffFamily d) (Phi : Vec d → NormalizedLocalH1Carrier d) (e : Vec d) (n : ℤ) : triadicScaledNegOneNorm n (correctorGradientOnOriginCube Phi e n) + triadicScaledNegOneNorm n (scalarIdentityCorrectorFluxDefectOnOriginCube a Phi e n) = ENNReal.ofReal (3 ^ n)⁻¹ * (negOneNorm (openCubeSet (originCube d n)) (Phi e).globalGradientRepresentative + negOneNorm (openCubeSet (originCube d n)) fun (x : Vec d) => matVecMul ((a.coeffOn (originCube d n)).toCoeffField x) (e + (Phi e).globalGradientRepresentative x) - e)

The class-level inverse-scale pair used by the finite-to-limit theorem is the raw canonical-gradient/canonical-flux pair used by affine transport.