High-contrast homogenization: Provider.Response.PreYoungWeakTop #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The infinite weak-quantity branch #
The compact pre-Young estimate is automatic when its weak quantity is infinite and the response coefficient is positive. Separating this branch keeps finiteness assumptions local to the analytic component estimates.
theorem
HCPolySupport.HighContrast.Response.le_compact_pre_young_of_weak_eq_top
{J a b row weak expo : ENNReal}
{Cresp : ℝ}
(hCresp : 0 < Cresp)
(hweak : weak = ⊤)
:
J ≤ ENNReal.ofReal Cresp * a * (a + b + row) + ENNReal.ofReal Cresp * expo * b * (b + row) + ENNReal.ofReal Cresp * weak
The compact pre-Young right-hand side is top when its weak quantity is top and its coefficient is positive.
theorem
HCPolySupport.HighContrast.Response.compact_pre_young_of_finite_weak
{J a b row weak expo : ENNReal}
{Cpre : ℝ}
(hCpre : 1 ≤ Cpre)
(hfinite :
weak ≠ ⊤ →
∀ (Cresp : ℝ),
Cpre ≤ Cresp →
J ≤ ENNReal.ofReal Cresp * a * (a + b + row) + ENNReal.ofReal Cresp * expo * b * (b + row) + ENNReal.ofReal Cresp * weak)
(Cresp : ℝ)
:
It suffices to prove the compact estimate under finiteness of the weak quantity; the complementary branch is automatic.
theorem
HCPolySupport.HighContrast.Response.compact_pre_young_of_finite_component_bounds
{J boundaryRow a b scaleRoot rowRoot weak expo : ENNReal}
{Ccut Crow Cdiv Cpre : ℝ}
(hCpre : 1 ≤ Cpre)
(hcomponents :
weak ≠ ⊤ →
∃ (divCurl : ENNReal) (cutoffEnergy : ENNReal),
J ≤ divCurl + cutoffEnergy + boundaryRow ∧ divCurl ≤ ENNReal.ofReal Cdiv * weak ∧ cutoffEnergy ≤ ENNReal.ofReal 2 * a * a + ENNReal.ofReal 4 * a * b + ENNReal.ofReal Ccut * expo * b * b ∧ boundaryRow ≤ ENNReal.ofReal √2 * a * scaleRoot + ENNReal.ofReal Crow * expo * b * rowRoot)
(hscaleRoot : scaleRoot ≤ rowRoot)
(hfour : 4 ≤ Cpre)
(hsqrtTwo : √2 ≤ Cpre)
(hcut : Ccut ≤ Cpre)
(hrow : Crow ≤ Cpre)
(hdiv : Cdiv ≤ Cpre)
(Cresp : ℝ)
:
Component estimates are needed only in the finite weak-quantity branch. The resulting compact estimate remains unconditional.