High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.FrozenWitnessZeroTrace

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

The zero-trace datum at the gauge cube

The cube solution takes its zeroTraceDifference as a binder. This module discharges it from the hole's own MemH1a0 premise, through E15's exists_h10Function_gaugeCube_of_memH1a0 — the one matrix-and-translation composite for H10Function, which until now had no consumer anywhere in the repository.

The premises E15 asks for are all in hand at the frozen witness:

• MeasurableSet U, volume U ≠ ⊤ — the isOpen_witnessDomain premise and the frozenWitness_physicalDomain_isOpenBoundedConvexDomain premise;
• the a.e. ellipticity of a field agreeing with scaledCoeff ε a almost everywhere on the bounded witness domain — the globally elliptic companion of IsAELocallyUniformlyElliptic.exists_ae_isEllipticMatrix_ae_eq_restrict, which memH1a0_congr_coeff lets the MemH1a0 datum be read at;
• the a.e. ellipticity of its affine pullback — the public aeElliptic_affineCoefficient, with affineLowerEllipticity_pos for the lower constant;
• the gauge identification and the convexity of the translated cube — that module and that module.

The value identity is then exact, not merely a.e.: E15 returns w.toFun y = (uFun - g₀.toFun) (S (y + c)), and pullbacks give uObs.toFun y = uFun (S (y + c)) and gObs.toFun y = g₀.toFun (S (y + c)).

theorem HCPolySupport.HighContrast.RowSupply.exists_frozenWitnessZeroTraceDifference {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} {j : ℤ} {z : Vec d} {epsilon : ℝ} {a : CoeffSpace d} (hepsilon : 0 < epsilon) (hU : U = (fun (y : Vec d) => z + matVecMul (matSqrt (symmPart abar)) y) '' openCubeSet (originCube d j)) (uFun : Vec d → ℝ) (uGrad : Vec d → Vec d) (g₀ : H1Function U) (hu0 : MemH1a0 (scaledCoeff epsilon a) U (fun (x : Vec d) => uFun x - g₀.toFun x) fun (x : Vec d) => uGrad x - g₀.grad x) (uObs gObs : H1Function (openCubeSet (originCube d j))) (huObsFun : ∀ (y : Vec d), uObs.toFun y = uFun (matVecMul (matSqrt (symmPart abar)) (y + matVecMul (matSqrt (symmPart abar))⁻¹ z))) (hgObsFun : ∀ (y : Vec d), gObs.toFun y = g₀.toFun (matVecMul (matSqrt (symmPart abar)) (y + matVecMul (matSqrt (symmPart abar))⁻¹ z))) : ∃ (w : H10Function (openCubeSet (originCube d j))), w.toFun =ᵐ[volumeMeasureOn (openCubeSet (originCube d j))] fun (x : Vec d) => uObs.toFun x - gObs.toFun x

the analytic inputs (b), completed. The zero-trace difference of cube solution, from the hole's MemH1a0 datum.