High-contrast homogenization: Provider.Response.PreYoungBoundaryNormalization #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Boundary-row normalization #
The child--parent energy uses the half-energy normalization. Consequently,
each of the two coordinate rows carries sqrt (4 * tau). Their half-sum is
still controlled by the standard sqrt 2 * sqrt tau Schur-load coefficient.
theorem
HCPolySupport.HighContrast.Response.abs_boundaryMean_le_of_four_mul_responseDefect
{d : ℕ}
{tau gain meanGrad meanFlux : ℝ}
{row : ENNReal}
{H : BlockMat d}
{Pcen Qcen : Vec d}
(hgradRow :
ENNReal.ofReal |meanGrad| ≤ ENNReal.ofReal (√(4 * tau) * profileSchurLoadFlux H Qcen) + ENNReal.ofReal gain * row ^ (1 / 2))
(hfluxRow :
ENNReal.ofReal |meanFlux| ≤ ENNReal.ofReal (√(4 * tau) * profileSchurLoadGradient H Pcen) + ENNReal.ofReal gain * row ^ (1 / 2))
:
ENNReal.ofReal (1 / 2 * |meanGrad + meanFlux|) ≤ ENNReal.ofReal (√2 * √tau * √(profileSchurLoad H Pcen Qcen)) + ENNReal.ofReal gain * row ^ (1 / 2)
Two coordinate-row estimates with the half-energy normalization combine into the standard boundary-mean estimate.