High-contrast homogenization: Provider.Quenched.SmallContrastYoungAbsorption #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Young absorption for the small-contrast response bound #
The pre-Young response estimate contains mixed square-root products. At small terminal energy, a tunable Young inequality absorbs the energy contribution back into the response and leaves a linear bound in the defect, row, and weak terms.
theorem
HCPolySupport.HighContrast.Quenched.response_le_linear_of_preYoung
{response energy defect row weak center C expo eta : ℝ}
(hresponse : 0 ≤ response)
(henergy : 0 ≤ energy)
(hdefect : 0 ≤ defect)
(hrow : 0 ≤ row)
(hcenter : 0 ≤ center)
(hC : 0 ≤ C)
(hexpo : 0 ≤ expo)
(hexpoOne : expo ≤ 1)
(heta : 0 < eta)
(henergyResponse : energy ≤ response + center)
(hpreYoung : response ≤ C * √defect * (√defect + √energy + √row) + C * expo * √energy * (√energy + √row) + C * weak)
(habsorb : C * eta + 3 / 2 * C * expo ≤ 1 / 2)
:
A mixed pre-Young response estimate becomes linear after absorbing an energy bounded by the response plus a nonnegative center error.