High-contrast homogenization:

Provider.PolynomialHomogenization.Root.RowSupply.PrintFaithfulPost109CapSurface

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

Print-faithful coarse-row cap surface

The localization proof uses two negative rows: the physical gradient and the physical flux defect. Its positive row belongs to the arbitrary dual test field. This interface therefore contains no fractional seminorm of a constant-coefficient comparison extension.

def HCPolySupport.HighContrast.RowSupply.PrintFaithfulPositiveTestRow {d : ℕ} {U : Set (Vec d)} {rho Rad : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (s : ℝ) (G : Vec d → Vec d) (hardyConstant : ENNReal) : Prop

The positive row in the printed pairing belongs to the dual test field. It is independent of the response cap and of every comparison extension.

Equations

• One or more equations did not get rendered due to their size.

def HCPolySupport.HighContrast.RowSupply.PrintFaithfulDomainFluxDefectDuality {d : ℕ} (U : Set (Vec d)) (s : ℝ) (aPhysical : CoeffField d) (u h : H1Function U) (Cdual : ℝ) : Prop

The domain duality step used after the printed flux-defect estimate. This is the exact comparison-extension occurrence on the printed route: it occurs only on the left side, never through hsNormSq U s h.grad.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.HighContrast.RowSupply.ofReal_abs_globalPairing_le_printFaithfulFullDualCap {d : ℕ} {U : Set (Vec d)} {rho Rad s : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (hd : 1 ≤ d) (hU : IsOpenBoundedConvexDomain U) (hUpos : 0 < MeasureTheory.volume U) (hUtop : MeasureTheory.volume U ≠ ⊤) (hs : 0 < s) (hsHalf : s < 1 / 2) (F : system.CellIndex → Vec d → Vec d) (G : Vec d → Vec d) (f : Vec d → ℝ) (hf : MeasureTheory.IntegrableOn f U MeasureTheory.volume) (hpair : ∀ (i : system.CellIndex), volumeAverage (system.cell i) f = volumeAverage (system.cell i) fun (x : Vec d) => vecDot (F i x) (G x)) (hF : ∀ (i : system.CellIndex), MeasureTheory.MemLp (F i) 2 (MeasureTheory.volume.restrict (system.cell i))) (hG : ∀ (i : system.CellIndex), MeasureTheory.Integrable G (MeasureTheory.volume.restrict (system.cell i))) (hGfinite : ∀ (i : system.CellIndex), hsNormSq (system.cell i) s G ≠ ⊤) {cap hardyConstant : ENNReal} (hcap : normalizedWhitneyRowEnergy system (physicalFullDualWhitneyFamilyCellEnergy system s F) ≤ cap) (hHardy : PrintFaithfulPositiveTestRow system s G hardyConstant) : ENNReal.ofReal |volumeAverage U f| ≤ (fractionalDualToBesovConstant d ^ 2 * cap) ^ (1 / 2) * (hardyConstant * hsNormSq U s G) ^ (1 / 2)

Generic printed pairing consumption for the physical full-dual row. In particular it applies to the physical flux-defect field without introducing a comparison extension.