High-contrast homogenization: Provider.PolynomialHomogenization.RuledWhitneyPhysicalDualRHSRow #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
theorem
HCPolySupport.HighContrast.negativeWhitneyCellEnergy_le_fullDual
{d : ℕ}
(hd : 1 ≤ d)
{U : Set (Vec d)}
{rho Rad s : ℝ}
(system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad)
(i : system.CellIndex)
(hs : 0 < s)
(hsHalf : s < 1 / 2)
(F : Vec d → Vec d)
(hF : MemVectorL2 (system.cell i) F)
:
negativeWhitneyCellEnergy system s F i ≤ fractionalDualToBesovConstant d ^ 2 * ENNReal.ofReal (physicalFullDualBesovVectorNorm (whitneyCellCube system i) s F) ^ 2
The available fractional smooth-dual comparison controls one physical negative Whitney square by the corresponding physical full-dual square.