High-contrast homogenization: #
Provider.Quenched.SmallContrastVarianceLaggedNormalizedIsotropyOfEnvelopes
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The lagged variance at a parametrized normalizing block, abstract moments #
The isotropy-block lagged variance replacement with the mean-envelope and second-moment values of the normalized source scale as hypotheses — the corrected (deepened) moment interface at the opaque-carrier variant.
theorem
HCPolySupport.HighContrast.Quenched.scaleVariance_le_lagged_normalized_of_block_of_envelopes
{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)
{l : ℤ}
(hl : ↑(kZero d) ≤ l)
{Cd : ℝ}
(hCd : max 1 (12 * ↑d * √↑d) ≤ Cd)
{n : Mat d}
(hn : Matrix.PosDef n)
(hgrid : IsRoundedGrid l (roundedGrid l n))
{j p : ℤ}
(hlj : l ≤ j)
(hjp : j ≤ p)
{Sj SStarj Kj : Mat d}
(hSj : Matrix.PosDef Sj)
(hStarj : Matrix.PosDef SStarj)
(hformj : toFullBlockMat (adaptedMean P (roundedGrid l n) j) = schurBlock Sj SStarj Kj)
{Sp SStarp Kp : Mat d}
(hSp : Matrix.PosDef Sp)
(hStarp : Matrix.PosDef SStarp)
(hformp : toFullBlockMat (adaptedMean P (roundedGrid l n) 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)
(hdropSmall : 4 * ↑d * (adaptedHattedContrast P (roundedGrid l n) j - adaptedHattedContrast P (roundedGrid l n) p) ≤ 1)
{Gc : ℕ}
{S' : CoeffSpace d → ℝ}
{cPt : ℝ}
(hcPt0 : 0 ≤ cPt)
(hpt' :
∀ᵐ (a : CoeffSpace d) ∂P, BlockMatLoewnerLE (coarseBlock (adaptedCell (roundedGrid l n) j) a)
(blockScale (cPt * normalizedSourceScale S' (j + ↑Gc - 1) a ^ g) E))
{cE mu2 : ℝ}
(hcEPt : cPt ≤ cE)
(hcE1 : 1 ≤ cE)
(hmu20 : 0 ≤ mu2)
(hmean : BlockMatLoewnerLE (adaptedMean P (roundedGrid l n) j) (blockScale cE E))
(hmom : ∫⁻ (a : CoeffSpace d), ENNReal.ofReal (normalizedSourceScale S' (j + ↑Gc - 1) a ^ ↑2) ∂P ≤ ENNReal.ofReal mu2)
{kapB : ℝ}
(hkapB0 : 0 ≤ kapB)
(hbSmeanp : blockSize E (adaptedMean P (roundedGrid l n) p) ≤ kapB)
{F : BlockMat d}
(hFsym : IsSymmetricBlockMat F)
(hFpd : Book.Ch02.BlockPosDef F)
{cN : ℝ}
(hcN1 : 1 ≤ cN)
(hmeanpF2 : toFullBlockMat (adaptedMean P (roundedGrid l n) p) ≤ cN • toFullBlockMat F)
{Csub : ℝ}
(hCsub : 0 < Csub)
(hsubdiv :
∀ (j' p' : ℤ),
l ≤ j' →
j' ≤ p' →
∃ (Z : Finset (Fin d → ℤ)),
↑Z = {w : Fin d → ℤ | adaptedCellCenter (roundedGrid l n) j' w ∈ adaptedCell (roundedGrid l n) 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 l n) j' w) a)))
(adaptedMean P (roundedGrid l n) j'))
(adaptedMean P (roundedGrid l n) p') ≤ ENNReal.ofReal (Csub * ↑Z.card ^ (-2⁻¹)) * lqSchattenSize P 2
(fun (a : CoeffSpace d) =>
blockSub (coarseBlock (adaptedCell (roundedGrid l n) j') a)
(adaptedMean P (roundedGrid l n) j'))
(adaptedMean P (roundedGrid l n) p'))
:
scaleVariance P (roundedGrid l n) F p ≤ ENNReal.ofReal
(√(2 * ↑d) * cN * ((2 + 4 * (1 + 4 * ↑d * (adaptedHattedContrast P (roundedGrid l n) j - adaptedHattedContrast P (roundedGrid l n) p)) ^ 2) * (Csub * ↑(3 ^ (d * (p - j).toNat)) ^ (-2⁻¹) * ((2 * ↑d) ^ 2⁻¹ * kapB * (2 * cE) * √mu2)) + 4 * (1 + 4 * ↑d * (adaptedHattedContrast P (roundedGrid l n) j - adaptedHattedContrast P (roundedGrid l n) p)) ^ 2 * (36 * epsj) + 4 * ↑d * (adaptedHattedContrast P (roundedGrid l n) j - adaptedHattedContrast P (roundedGrid l n) p)))