High-contrast homogenization: Provider.Quenched.SmallContrastMeanDropCarrier #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The mean-drop carrier #
The reference-normalized mean drop between two scales of one grid is
first-order in the hatted contrast drop: the mean dilation bounds the
difference by 4d·(hat_j − hat_p) times the later mean, the terminal
envelope converts the later mean into the scaled reference, and the
sandwich bound converts the Loewner estimate into the scalar size.
theorem
HCPolySupport.HighContrast.Quenched.blockSize_meanDrop_le
{d : ℕ}
[NeZero d]
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
(hstat : IsStationaryLaw P)
{l : ℤ}
{q : Mat d}
(hgrid : IsRoundedGrid l q)
{j p : ℤ}
(hlj : l ≤ j)
(hjp : j ≤ p)
(hfinj : HasFiniteAdaptedMean P q j)
(hfinp : HasFiniteAdaptedMean P q p)
(hsmall : ↑d * (adaptedHattedContrast P q j - adaptedHattedContrast P q p) ≤ 1)
{E : BlockMat d}
(hEsym : IsSymmetricBlockMat E)
{cT : ℝ}
(hcT : 0 ≤ cT)
(henvT : BlockMatLoewnerLE (adaptedMean P q p) (blockScale cT E))
{F : BlockMat d}
(hFsym : IsSymmetricBlockMat F)
(hFpd : Book.Ch02.BlockPosDef F)
:
blockSize (blockSub (adaptedMean P q j) (adaptedMean P q p)) F ≤ 4 * ↑d * (adaptedHattedContrast P q j - adaptedHattedContrast P q p) * cT * blockSize E F
The mean-drop carrier bound.