High-contrast homogenization: Provider.Response.AffineAnnealedCutoffEnergyAdjointComponent #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The adjoint annealed cutoff-energy component on adapted cells #
The affine reference family for the transposed recentered coefficient is chosen independently of the primal family. The transported loads and the physical adjoint optimizer remain explicit throughout the identification.
theorem
HCPolySupport.HighContrast.Response.ofReal_abs_integral_affineAdjointSubSkewCutoffEnergyDefect_le_component
{d : ℕ}
[NeZero d]
{P : MeasureTheory.Measure (CoeffSpace d)}
(hP : IsStationaryLaw P)
{q : Mat d}
(hq : Matrix.PosDef q)
{l s t H : ℤ}
(hqGrid : IsRoundedGrid l q)
(hls : l ≤ s)
(j : ℕ)
(hscale : t - ↑j = s)
(hH : H = t - s)
(g : Mat d)
(hg : IsSkewMat g)
(p r : Vec d)
(hs :
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
Book.Ch02.responseJ (adaptedDomain hq s) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq s)) p r)
P)
(ht :
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)) p r)
P)
(hcutoff :
MeasureTheory.Integrable
(fun (a : CoeffSpace d) =>
(Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) =>
adaptedPreYoungCutoff q hq t x * (1 / 2 * vecDot ((centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x)
(matVecMul (((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)).toCoeffField x)
((centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x)))) - Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)) p r)
P)
:
ENNReal.ofReal
|∫ (a : CoeffSpace d), (Book.Ch02.average (adaptedDomain hq t) fun (x : Vec d) =>
adaptedPreYoungCutoff q hq t x * (1 / 2 * vecDot ((centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x)
(matVecMul (((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)).toCoeffField x)
((centeredAdjointOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x)))) - Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)) p r ∂P| ≤ ENNReal.ofReal 2 * ENNReal.ofReal √(profileAdjointResponseDefect P hq g hg s t p r) * ENNReal.ofReal √(profileAdjointResponseDefect P hq g hg s t p r) + ENNReal.ofReal 4 * ENNReal.ofReal √(profileAdjointResponseDefect P hq g hg s t p r) * ENNReal.ofReal
√(∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)) p
r ∂P) + ENNReal.ofReal (32 * ↑d ^ 2 * smoothTransitionProfile.derivBound) * ENNReal.ofReal (3 ^ (-H)) * ENNReal.ofReal
√(∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)) p
r ∂P) * ENNReal.ofReal
√(∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).transpose.coeffOn (adaptedDomain hq t)) p r ∂P)
The adjoint cutoff-energy contribution on the adapted terminal cell has the same three-term bound, using a separately chosen affine reference family for the transposed recentered coefficient.