High-contrast homogenization: Provider.Response.AffineAnnealedCutoffEnergyComponent

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

The annealed cutoff-energy component on adapted cells

The affine reference family is chosen inside the proof. Its child responses cancel by physical stationarity, while its terminal response and difference energy are identified with the physical adapted-cell quantities. The final statements therefore expose no reference-family or transport premise.

Primal component

theorem HCPolySupport.HighContrast.Response.ofReal_abs_integral_affineSubSkewCutoffEnergyDefect_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).coeffOn (adaptedDomain hq s)) p r) P) (ht : MeasureTheory.Integrable (fun (a : CoeffSpace d) => Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).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 ((centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x) (matVecMul (((a.subSkew g hg).coeffOn (adaptedDomain hq t)).toCoeffField x) ((centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x)))) - Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).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 ((centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x) (matVecMul (((a.subSkew g hg).coeffOn (adaptedDomain hq t)).toCoeffField x) ((centeredResponseOptimizer (adaptedDomain hq t) (a.subSkew g hg) p r).toH1.grad x)))) - Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).coeffOn (adaptedDomain hq t)) p r ∂P| ≤ ENNReal.ofReal 2 * ENNReal.ofReal √(profilePrimalResponseDefect P hq g hg s t p r) * ENNReal.ofReal √(profilePrimalResponseDefect P hq g hg s t p r) + ENNReal.ofReal 4 * ENNReal.ofReal √(profilePrimalResponseDefect P hq g hg s t p r) * ENNReal.ofReal √(∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).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).coeffOn (adaptedDomain hq t)) p r ∂P) * ENNReal.ofReal √(∫ (a : CoeffSpace d), Book.Ch02.responseJ (adaptedDomain hq t) ((a.subSkew g hg).coeffOn (adaptedDomain hq t)) p r ∂P)

The primal cutoff-energy contribution on the adapted terminal cell has the three-term extended-nonnegative bound, with the physical response defect and terminal response on the right.