High-contrast homogenization: Provider.Quenched.SmallContrastVarianceHatted #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The variance split at the recentered frame #
The abstract variance split instantiated at the recentered coarse blocks and means: every input transports through the shear congruence, the two frame inputs are the recentered sharp bounds, and the conclusion returns to the plain frame by the congruence invariance of the two-sided size.
theorem
HCPolySupport.HighContrast.Quenched.blockSize_variance_replacement_pathwise
{d : ℕ}
[NeZero d]
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
(hstat : IsStationaryLaw P)
{l : ℤ}
{q : Mat d}
(hq : IsRoundedGrid l q)
{j p : ℤ}
(hlj : l ≤ j)
(hjp : j ≤ p)
(hintj : HasFiniteAdaptedMean P q j)
(hintp : HasFiniteAdaptedMean P q p)
{Sj SStarj Kj : Mat d}
(hSj : Matrix.PosDef Sj)
(hStarj : Matrix.PosDef SStarj)
(hformj : toFullBlockMat (adaptedMean P q j) = schurBlock Sj SStarj Kj)
{Sp SStarp Kp : Mat d}
(hSp : Matrix.PosDef Sp)
(hStarp : Matrix.PosDef SStarp)
(hformp : toFullBlockMat (adaptedMean P q p) = schurBlock Sp SStarp Kp)
{epsj epsp : ℝ}
(hposj : 0 ≤ epsj)
(hepsj1 : epsj ≤ 1)
(htrj : ↑d * (schurHattedContrast Sj SStarj - 1) ≤ epsj)
(hposp : 0 < epsp)
(hepsp1 : epsp ≤ 1)
(htrp : ↑d * (schurHattedContrast Sp SStarp - 1) ≤ epsp)
(hposj' : 0 < epsj)
(hdropSmall : 4 * ↑d * (adaptedHattedContrast P q j - adaptedHattedContrast P q p) ≤ 1)
{Z : Finset (Fin d → ℤ)}
(hZ : ↑Z = {w : Fin d → ℤ | adaptedCellCenter q j w ∈ adaptedCell q p})
(hZne : Z.Nonempty)
(a : CoeffSpace d)
:
blockSize (blockSub (coarseBlock (adaptedCell q p) a) (adaptedMean P q p)) (adaptedMean P q p) ≤ (2 + 4 * (1 + 4 * ↑d * (adaptedHattedContrast P q j - adaptedHattedContrast P q p)) ^ 2) * blockSize
(blockSub (ofFullBlockMat ((↑Z.card)⁻¹ • ∑ w ∈ Z, toFullBlockMat (coarseBlock (adaptedCellAt q j w) a)))
(adaptedMean P q j))
(adaptedMean P q p) + 4 * (1 + 4 * ↑d * (adaptedHattedContrast P q j - adaptedHattedContrast P q p)) ^ 2 * (36 * epsj) + 4 * ↑d * (adaptedHattedContrast P q j - adaptedHattedContrast P q p)
The pathwise variance replacement, plain-frame conclusion.