High-contrast homogenization: Provider.Quenched.SmallContrastHvarFamilySplit #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The burn-split variance family at a parametrized normalizer #
The variance family at the burn-split slot bounds: the family values carry
supplyMscSplit d E โ dimensional up to ฮบ_๐.
theorem
HCPolySupport.HighContrast.Quenched.hvar_family_of_account_of_block_split
{d : โ}
[NeZero d]
(hd : 2 โค d)
{g : โ}
(hg : g โ Set.Ico 0 1)
{P : MeasureTheory.Measure (CoeffSpace d)}
[MeasureTheory.IsProbabilityMeasure P]
{E : BlockMat d}
{ฮจ : โ โ โ}
{K : โ}
{S : CoeffSpace d โ โ}
(hdag : CoarseEllipticityDagger P g E ฮจ K S)
(hstat : IsStationaryLaw P)
{lAl : โค}
(hl : โ(kZero d) โค lAl)
{Cd : โ}
(hCd : max 1 (12 * โd * โโd) โค Cd)
{mAl : Mat d}
(hn : Matrix.PosDef mAl)
(hgrid : IsRoundedGrid lAl (roundedGrid lAl mAl))
{Gacc : โ}
(hqnorm : โroundedGrid lAl mAlโ * โโd โค 3 ^ Gacc)
(hDbc : boundaryConst Cd g mAl โค 3 ^ (Gacc + 1))
(hmeso :
โแต (a : CoeffSpace d) โP, โ (m : โค),
S a โค 3 ^ m โ
โ k โค m,
โ (w : Fin d โ โค),
standardCellCenter k w โ centeredCube d m โ
BlockMatLoewnerLE (coarseBlock (standardCell d k w) a)
(blockScale (3 ^ (g * max (โm - 2 * โ(Gacc + 1) - โk) 0)) E))
{sKw : โค}
(hsKw : growthBar K โค 3 ^ sKw)
{t : โค}
{Hw : โ}
{jb : โค}
(hstart : lAl โค t - โHw)
(hsKstart : sKw โค t - โHw)
(hjbstart : t - โHw โค jb)
(hjbt : jb โค t)
(M : โ)
(hburnStart :
1 + 2 * โ(2 + M) * (1 + Real.log (growthBar K)) * growthBar K ^ IndependentSums.natTriangular (2 + M) โค 3 ^ (โM * โ(t - โHw + โ(Gacc + 1) - 1 - sKw)))
{delta : โ}
(hdelta4 : delta โค 1 / 4)
(hsm : โ (k : โค), lAl โค k โ k โค t โ hatExcessAt P (roundedGrid lAl mAl) k โค delta)
{F : BlockMat d}
(hFsym : IsSymmetricBlockMat F)
(hFpd : Book.Ch02.BlockPosDef F)
(henvFam : โ j โค Hw, BlockMatLoewnerLE (adaptedMean P (roundedGrid lAl mAl) (t - โj)) F)
{Csub : โ}
(hCsub : 0 < Csub)
(hsubdiv :
โ (j' p' : โค),
lAl โค j' โ
j' โค p' โ
โ (Z : Finset (Fin d โ โค)),
โZ = {w : Fin d โ โค | adaptedCellCenter (roundedGrid lAl mAl) j' w โ adaptedCell (roundedGrid lAl mAl) p'} โง Z.card = 3 ^ (d * (p' - j').toNat) โง Z.Nonempty โง lqSchattenSize P 2
(fun (a : CoeffSpace d) =>
blockSub
(ofFullBlockMat
((โZ.card)โปยน โข โ w โ Z, toFullBlockMat (coarseBlock (adaptedCellAt (roundedGrid lAl mAl) j' w) a)))
(adaptedMean P (roundedGrid lAl mAl) j'))
(adaptedMean P (roundedGrid lAl mAl) p') โค ENNReal.ofReal (Csub * โZ.card ^ (-2โปยน)) * lqSchattenSize P 2
(fun (a : CoeffSpace d) =>
blockSub (coarseBlock (adaptedCell (roundedGrid lAl mAl) j') a)
(adaptedMean P (roundedGrid lAl mAl) j'))
(adaptedMean P (roundedGrid lAl mAl) p'))
(j : โ)
:
j โค Hw โ
scaleVariance P (roundedGrid lAl mAl) F (t - โj) โค ENNReal.ofReal
(slotFamilyValue d Csub (supplyMscSplit d E) delta (hatExcessAt P (roundedGrid lAl mAl) jb) (t - jb).toNat j)
The variance family, at a parametrized normalizer.