Documentation

LeanPool.HighContrastHomogenization.Provider.Response.PreYoungAssemblyAlgebra

High-contrast homogenization: Provider.Response.PreYoungAssemblyAlgebra #

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

Algebraic closure of the pre-Young response estimate #

The cutoff, div--curl, and boundary-row estimates produce six nonnegative terms. This file records the coefficient enlargement and the distributive calculation that put those terms into the compact mixed form used by the response argument.

source
theorem HCPolySupport.HighContrast.Response.exists_one_le_pre_young_constant (d : ℕ) (Ctransport : ℝ) :
∃ (Cpre : ℝ), 1 ≤ Cpre ∧ 32 * ↑d ^ 2 * smoothTransitionProfile.derivBound ≤ Cpre ∧ Ctransport ≤ Cpre ∧ 4 ≤ Cpre ∧ √2 ≤ Cpre

A dimension-only cutoff constant and any further dimension-only transport coefficient admit one common pre-Young constant.

source
theorem HCPolySupport.HighContrast.Response.compact_pre_young_of_explicit_components {J a b scaleRoot rowRoot weak expo : ENNReal} {Ccut Crow Cdiv Cresp : ℝ} (hJ : 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) (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 explicit defect, energy, boundary-row, and weak terms are dominated by the compact mixed pre-Young expression once their coefficients share one upper bound.