Documentation

LeanPool.HighContrastHomogenization.Provider.Response.ProfileDefectHistory

High-contrast homogenization: Provider.Response.ProfileDefectHistory #

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

Nonlinear-history bounds for the positive response defects #

The scale-s term in the terminal nonlinear history controls the relative mean gain. Combined with the terminal load estimates, this gives the primal and adjoint response-defect bounds with their independent loads.

source
theorem HCPolySupport.HighContrast.Response.profilePrimalResponseDefect_nonneg_of_stationary {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {l : ℤ} {q g : Mat d} (hg : IsSkewMat g) {s t : ℤ} (hP : IsStationaryLaw P) (hgrid : IsRoundedGrid l q) (hls : l ≤ s) (hst : s ≤ t) (hints : HasFiniteAdaptedMean P q s) (hintt : HasFiniteAdaptedMean P q t) (p r : Vec d) :
0 ≤ profilePrimalResponseDefect P ⋯ g hg s t p r

Stationarity and aligned mean order make the primal response defect nonnegative.

source
theorem HCPolySupport.HighContrast.Response.profileAdjointResponseDefect_nonneg_of_stationary {d : ℕ} [NeZero d] {P : MeasureTheory.Measure (CoeffSpace d)} [MeasureTheory.IsProbabilityMeasure P] {l : ℤ} {q g : Mat d} (hg : IsSkewMat g) {s t : ℤ} (hP : IsStationaryLaw P) (hgrid : IsRoundedGrid l q) (hls : l ≤ s) (hst : s ≤ t) (hints : HasFiniteAdaptedMean P q s) (hintt : HasFiniteAdaptedMean P q t) (p r : Vec d) :
0 ≤ profileAdjointResponseDefect P ⋯ g hg s t p r

Stationarity and aligned mean order make the coefficient-transpose response defect nonnegative.