High-contrast homogenization: Provider.Quenched.SmallContrastEntryCapsIsotropyAtLevel #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The account's entry caps at a released split level #
The account-side caps bundle with its two weak quantities read against the released sharp weak value.
theorem
HCPolySupport.HighContrast.Quenched.account_profile_caps_entry_of_block_at_level
{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)
{rho : ℝ}
(hrho0 : 0 < rho)
(hrho1 : rho < 1)
{s t : ℤ}
(hst : s ≤ t)
(Hw : ℕ)
(hstart : lAl ≤ t - ↑Hw)
{sKw : ℤ}
(hsKw : growthBar K ≤ 3 ^ sKw)
(hsKrange : sKw ≤ t - ↑Hw)
(hentry : sourceMomentTwo K ≤ 3 ^ (t + ↑(Gacc + 1) - sKw))
{S0 SStar0 K0 : Mat d}
(hS0 : Matrix.PosDef S0)
(hStar0 : Matrix.PosDef SStar0)
(hform : toFullBlockMat (adaptedMean P (roundedGrid lAl mAl) t) = schurBlock S0 SStar0 K0)
{eps : ℝ}
(hpos : 0 < eps)
(heps1 : eps ≤ 1)
(htr : ↑d * (schurHattedContrast S0 SStar0 - 1) ≤ eps)
(hdropSmall :
∀ j ≤ Hw,
↑d * (adaptedHattedContrast P (roundedGrid lAl mAl) (t - ↑j) - adaptedHattedContrast P (roundedGrid lAl mAl) t) ≤ 1)
{k0 : ℤ}
{cIso : ℝ}
(hcIso : 0 ≤ cIso)
(hiso :
∀ (k : ℤ),
k0 ≤ k →
k ≤ s →
∀ w ∈ Response.alignedIndex (roundedGrid lAl mAl) k s,
BlockMatLoewnerLE (annealedBlock P (adaptedCellAt (roundedGrid lAl mAl) k w)) (blockScale (1 + cIso) E))
{cDeep : ℝ}
(hcDeep : capsDeepConstant Cd g mAl (Gacc + 1) k0 s t ≤ cDeep)
{F : BlockMat d}
(hFsym : IsSymmetricBlockMat F)
(hFpd : Book.Ch02.BlockPosDef F)
{cF : ℝ}
(hcF0 : 0 ≤ cF)
(hFeq : F = blockScale cF E)
(henvF : BlockMatLoewnerLE (adaptedMean P (roundedGrid lAl mAl) t) F)
{kapE : ℝ}
(hkapE1 : 1 ≤ kapE)
(hcompE :
∀ (X : BlockVec d),
blockVecDot X (blockMatVecMul E X) ≤ kapE * blockVecDot X (blockMatVecMul (adaptedMean P (roundedGrid lAl mAl) t) X))
{R lev : ℝ}
(hR1 : 1 ≤ R)
(hlev : 1 ≤ lev)
(henvMax :
∀ᵐ (a : CoeffSpace d) ∂P, Response.diagonalWeakMaximum rho (roundedGrid lAl mAl) t F a ≤ ENNReal.ofReal (R * (max 1 (3 * S a * 3 ^ (-(↑t + ↑(Gacc + 1)))) ^ g / 2)))
{V : ℕ → ℝ}
{V0 Vmean : ℝ}
(hV : ∀ j ≤ Hw, 0 ≤ V j)
(hV0 : 0 ≤ V0)
(hVmean : 0 ≤ Vmean)
(hvar : ∀ j ≤ Hw, scaleVariance P (roundedGrid lAl mAl) F (t - ↑j) ≤ ENNReal.ofReal (V j))
(hvart : scaleVariance P (roundedGrid lAl mAl) F t ≤ ENNReal.ofReal V0)
(hvmean : scaleVariance P (roundedGrid lAl mAl) (adaptedMean P (roundedGrid lAl mAl) t) t ≤ ENNReal.ofReal Vmean)
(e : Vec d)
:
e ⬝ᵥ e = 1 →
Response.profilePrimalHattedEarlierRow P (roundedGrid lAl mAl) (Response.responseSkew K0) s
(Response.profilePrimalCenter P ⋯ t (fun (a : CoeffSpace d) => a.subSkew (Response.responseSkew K0) ⋯)
(Response.centeredResponseLoadP S0 SStar0 K0 e) (Response.centeredResponseLoadQ S0 SStar0 K0 e)).1
(Response.profilePrimalCenter P ⋯ t (fun (a : CoeffSpace d) => a.subSkew (Response.responseSkew K0) ⋯)
(Response.centeredResponseLoadP S0 SStar0 K0 e) (Response.centeredResponseLoadQ S0 SStar0 K0 e)).2 ≤ ENNReal.ofReal (rowValue2Isotropy d (rowSplitConstant cIso cDeep) kapE eps) ∧ Response.profileAdjointHattedEarlierRow P (roundedGrid lAl mAl) (Response.responseSkew K0) s
(Response.profileAdjointCenter P ⋯ t (fun (a : CoeffSpace d) => a.subSkew (Response.responseSkew K0) ⋯)
(Response.centeredResponseLoadP S0 SStar0 K0 e) (Response.centeredResponseLoadQ S0 SStar0 K0 e)).1
(Response.profileAdjointCenter P ⋯ t (fun (a : CoeffSpace d) => a.subSkew (Response.responseSkew K0) ⋯)
(Response.centeredResponseLoadP S0 SStar0 K0 e) (Response.centeredResponseLoadQ S0 SStar0 K0 e)).2 ≤ ENNReal.ofReal (rowValue2Isotropy d (rowSplitConstant cIso cDeep) kapE eps) ∧ Response.profilePrimalWeakQuantity P mAl ⋯ t (fun (a : CoeffSpace d) => a.subSkew (Response.responseSkew K0) ⋯)
(Response.centeredResponseLoadP S0 SStar0 K0 e) (Response.centeredResponseLoadQ S0 SStar0 K0 e) ≤ ENNReal.ofReal
(weakValueBoundSharpIsotropyAt (Response.recentConstantAtLevel lev) (Response.maxGroupConstantAtLevel lev)
(Response.energyGoodConstantAtLevel lev) P mAl (Response.responseSkew K0) F (loadScaleOfScalar cF kapE)
mAl rho Hw (R ^ 4 * badMomentMajorant K (t + ↑(Gacc + 1) - 1 - sKw)) (R / 2) lev t lAl V V0
(meanDrop2ValueIsotropy P lAl cF mAl E F t) Vmean) ∧ Response.profileAdjointWeakQuantity P mAl ⋯ t (fun (a : CoeffSpace d) => a.subSkew (Response.responseSkew K0) ⋯)
(Response.centeredResponseLoadP S0 SStar0 K0 e) (Response.centeredResponseLoadQ S0 SStar0 K0 e) ≤ ENNReal.ofReal
(weakValueBoundSharpIsotropyAt (Response.recentConstantAtLevel lev) (Response.maxGroupConstantAtLevel lev)
(Response.energyGoodConstantAtLevel lev) P mAl (Response.responseSkew K0) F (loadScaleOfScalar cF kapE)
mAl rho Hw (R ^ 4 * badMomentMajorant K (t + ↑(Gacc + 1) - 1 - sKw)) (R / 2) lev t lAl V V0
(meanDrop2ValueIsotropy P lAl cF mAl E F t) Vmean) ∧ 1 / 2 * |vecDot
(fun (i : Fin d) =>
∫ (a : CoeffSpace d), Book.Ch02.averageGradient (Response.adaptedDomain ⋯ t)
((a.subSkew (Response.responseSkew K0) ⋯).coeffOn (Response.adaptedDomain ⋯ t))
(Response.centeredResponseOptimizer (Response.adaptedDomain ⋯ t)
(a.subSkew (Response.responseSkew K0) ⋯) (Response.centeredResponseLoadP S0 SStar0 K0 e)
(Response.centeredResponseLoadQ S0 SStar0 K0 e))
i ∂P)
fun (i : Fin d) =>
∫ (a : CoeffSpace d), Book.Ch02.averageFlux (Response.adaptedDomain ⋯ t)
((a.subSkew (Response.responseSkew K0) ⋯).coeffOn (Response.adaptedDomain ⋯ t))
(Response.centeredResponseOptimizer (Response.adaptedDomain ⋯ t)
(a.subSkew (Response.responseSkew K0) ⋯) (Response.centeredResponseLoadP S0 SStar0 K0 e)
(Response.centeredResponseLoadQ S0 SStar0 K0 e))
i ∂P| ≤ (3 * ↑d + 4) * eps ^ 2 ∧ 1 / 2 * |vecDot
(fun (i : Fin d) =>
∫ (a : CoeffSpace d), Book.Ch02.averageGradient (Response.adaptedDomain ⋯ t)
((a.subSkew (Response.responseSkew K0) ⋯).transpose.coeffOn (Response.adaptedDomain ⋯ t))
(Response.centeredAdjointOptimizer (Response.adaptedDomain ⋯ t)
(a.subSkew (Response.responseSkew K0) ⋯) (Response.centeredResponseLoadP S0 SStar0 K0 e)
(Response.centeredResponseLoadQ S0 SStar0 K0 e))
i ∂P)
fun (i : Fin d) =>
∫ (a : CoeffSpace d), Book.Ch02.averageFlux (Response.adaptedDomain ⋯ t)
((a.subSkew (Response.responseSkew K0) ⋯).transpose.coeffOn (Response.adaptedDomain ⋯ t))
(Response.centeredAdjointOptimizer (Response.adaptedDomain ⋯ t)
(a.subSkew (Response.responseSkew K0) ⋯) (Response.centeredResponseLoadP S0 SStar0 K0 e)
(Response.centeredResponseLoadQ S0 SStar0 K0 e))
i ∂P| ≤ (3 * ↑d + 4) * eps ^ 2
The account's entry caps, at a released split level.