High-contrast homogenization: Provider.Response.PreYoungRowClosingAssembly #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Closing the pre-Young boundary rows #
The boundary means split into a defect contribution and a cutoff-oscillation contribution. This file records the carrier conversion for that split and specializes the four scale-sum estimates to the literal primal and adjoint row premises used by the boundary-mean assembly.
Generic component assembly #
theorem
HCPolySupport.HighContrast.Response.ofReal_abs_le_add_of_eq_add
{mean defect oscillation : ℝ}
(hmean : mean = defect + oscillation)
:
An exact decomposition into defect and oscillation terms gives the corresponding mixed-ENNReal triangle bound.
theorem
HCPolySupport.HighContrast.Response.ofReal_abs_le_add_of_component_bounds
{mean defect oscillation : ℝ}
{defectBound oscillationBound : ENNReal}
(hsplit : ENNReal.ofReal |mean| ≤ ENNReal.ofReal |defect| + ENNReal.ofReal |oscillation|)
(hdefect : ENNReal.ofReal |defect| ≤ defectBound)
(hoscillation : ENNReal.ofReal |oscillation| ≤ oscillationBound)
:
A triangle bound closes once its defect and oscillation components have been bounded separately.