High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Duality.DomainDualityFromHodge

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

The two printed negative rows from the domain Hodge estimate

The domain Hodge estimate prices the zero-trace potential part of a solenoidal sum by the complementary part, in the negative fractional norm. Given it, the two rows of PrintFaithfulDomainFluxDefectDuality follow from the field identity a ∇u − ∇h = (∇u − ∇h) + (a − 1) ∇u and subadditivity of the dual norm, with

Cdual = 2 * Chodge + 1.

No coefficient-law dependence enters that constant. This is the last algebraic step between the domain statement and the printed consumer surface.

theorem HCPolySupport.HighContrast.RowSupply.negSobolevNorm_add_le {d : ℕ} (V : Set (Vec d)) (s : ℝ) (F G : Vec d → Vec d) : (negSobolevNorm V s fun (x : Vec d) => F x + G x) ≤ negSobolevNorm V s F + negSobolevNorm V s G

The negative fractional norm is subadditive.

theorem HCPolySupport.HighContrast.RowSupply.domainFluxComparison_eq_add {d : ℕ} {U : Set (Vec d)} (aPhysical : CoeffField d) (u h : H1Function U) : (fun (x : Vec d) => matVecMul (aPhysical x) (u.grad x) - h.grad x) = fun (x : Vec d) => u.grad x - h.grad x + matVecMul (aPhysical x - 1) (u.grad x)

The physical comparison flux is the sum of the gradient difference and the identity-reference flux defect.

theorem HCPolySupport.HighContrast.RowSupply.isPotentialZeroTraceOn_gradSub_of_memAffineH10 {d : ℕ} {U : Set (Vec d)} (u h : H1Function U) (haff : MemAffineH10 U h u) : IsPotentialZeroTraceOn U fun (x : Vec d) => u.grad x - h.grad x

Affine zero-trace membership supplies the potential field of the duality argument.

theorem HCPolySupport.HighContrast.RowSupply.printFaithfulDomainFluxDefectDuality_of_hodgeBound_of_potential {d : ℕ} {U : Set (Vec d)} {s Chodge : ℝ} (hChodge : 0 ≤ Chodge) (aPhysical : CoeffField d) (u h : H1Function U) (hF : MemVectorL2 U fun (x : Vec d) => matVecMul (aPhysical x - 1) (u.grad x)) (hpot : IsPotentialZeroTraceOn U fun (x : Vec d) => u.grad x - h.grad x) (hsol : IsSolenoidalOn U fun (x : Vec d) => matVecMul (aPhysical x) (u.grad x) - h.grad x) (hodge : ∀ (w F : Vec d → Vec d), MemVectorL2 U F → IsPotentialZeroTraceOn U w → (IsSolenoidalOn U fun (x : Vec d) => w x + F x) → negSobolevNorm U s w ≤ ENNReal.ofReal Chodge * negSobolevNorm U s F) : PrintFaithfulDomainFluxDefectDuality U s aPhysical u h (2 * Chodge + 1)

The printed two-row duality from the domain Hodge estimate. The constant is 2 * Chodge + 1: the first row is one Hodge application, the second adds the defect itself through subadditivity of the dual norm.