Documentation

LeanPool.HighContrastHomogenization.Provider.Response.PreYoungExplicitAssembly

High-contrast homogenization: Provider.Response.PreYoungExplicitAssembly #

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Explicit pre-Young component assembly #

The deterministic decomposition separates the centered response into a div--curl term, a cutoff-energy term, and a boundary-row term. This file combines bounds for those three components and passes the resulting six-term estimate to the compact pre-Young algebra.

source
theorem HCPolySupport.HighContrast.Response.explicit_pre_young_of_component_bounds {J divCurl cutoffEnergy boundaryRow a b scaleRoot rowRoot weak expo : ENNReal} {Ccut Crow Cdiv : ℝ} (hdecomposition : J ≤ divCurl + cutoffEnergy + boundaryRow) (hdivCurl : divCurl ≤ ENNReal.ofReal Cdiv * weak) (hcutoffEnergy : cutoffEnergy ≤ ENNReal.ofReal 2 * a * a + ENNReal.ofReal 4 * a * b + ENNReal.ofReal Ccut * expo * b * b) (hboundaryRow : boundaryRow ≤ ENNReal.ofReal √2 * a * scaleRoot + ENNReal.ofReal Crow * expo * b * rowRoot) :
J ≤ ENNReal.ofReal 2 * a * a + ENNReal.ofReal 4 * a * b + ENNReal.ofReal √2 * a * scaleRoot + ENNReal.ofReal Ccut * expo * b * b + ENNReal.ofReal Crow * expo * b * rowRoot + ENNReal.ofReal Cdiv * weak

Component bounds for the three terms of the centered-response decomposition give the explicit six-term pre-Young estimate.

source
theorem HCPolySupport.HighContrast.Response.compact_pre_young_of_component_bounds {J divCurl cutoffEnergy boundaryRow a b scaleRoot rowRoot weak expo : ENNReal} {Ccut Crow Cdiv Cresp : ℝ} (hdecomposition : J ≤ divCurl + cutoffEnergy + boundaryRow) (hdivCurl : divCurl ≤ ENNReal.ofReal Cdiv * weak) (hcutoffEnergy : cutoffEnergy ≤ ENNReal.ofReal 2 * a * a + ENNReal.ofReal 4 * a * b + ENNReal.ofReal Ccut * expo * b * b) (hboundaryRow : boundaryRow ≤ ENNReal.ofReal √2 * a * scaleRoot + ENNReal.ofReal Crow * expo * b * rowRoot) (hscaleRoot : scaleRoot ≤ rowRoot) (hfour : 4 ≤ Cresp) (hsqrtTwo : √2 ≤ Cresp) (hcut : Ccut ≤ Cresp) (hrow : Crow ≤ Cresp) (hdiv : Cdiv ≤ Cresp) :
J ≤ ENNReal.ofReal Cresp * a * (a + b + rowRoot) + ENNReal.ofReal Cresp * expo * b * (b + rowRoot) + ENNReal.ofReal Cresp * weak

The same three component bounds imply the exact compact mixed-ENNReal right-hand side used by the conditional response theorem.