High-contrast homogenization: Provider.Quenched.SmallContrastCapsBundleEntryIsotropyAtLevel #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The entry caps bundle at a released split level #
The six-clause bundle with its two weak quantities read against the released sharp weak value. The four row and centering clauses are level-free and are the pinned ones.
theorem
HCPolySupport.HighContrast.Quenched.profile_caps_bundle_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))
{rho : ℝ}
(hrho0 : 0 < rho)
(hrho1 : rho < 1)
{s t : ℤ}
(hst : s ≤ t)
(Hw : ℕ)
(hstart : lAl ≤ t - ↑Hw)
{G : ℕ}
(hgeomS :
∀ k ≤ s,
∀ w ∈ Response.alignedIndex (roundedGrid lAl mAl) k s,
adaptedCellAt (roundedGrid lAl mAl) k w ⊆ centeredCube d (t + ↑G))
{sK : ℤ}
(hsK : growthBar K ≤ 3 ^ sK)
(hDelta : 0 ≤ t + ↑G - 1 - sK)
(hentry : sourceMomentTwo K ≤ 3 ^ (t + ↑G - sK))
(hintAll : ∀ (k : ℤ), HasFiniteAdaptedMean P (roundedGrid lAl mAl) k)
(hEt : Book.Ch02.BlockPosDef (adaptedMean P (roundedGrid lAl mAl) t))
{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)
{kap : ℝ}
(hkap0 : 0 ≤ kap)
(hcomp :
∀ (X : BlockVec d),
blockVecDot X (blockMatVecMul E X) ≤ kap * blockVecDot X (blockMatVecMul (adaptedMean P (roundedGrid lAl mAl) t) X))
{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))
{F : BlockMat d}
(hFsym : IsSymmetricBlockMat F)
(hFpd : Book.Ch02.BlockPosDef F)
{cF : ℝ}
(hcF0 : 0 ≤ cF)
(hFeq : F = blockScale cF E)
{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 + ↑G))) ^ g / 2)))
{V : ℕ → ℝ}
{V0 : ℝ}
{Dr : ℕ → ℝ}
{Vmean : ℝ}
(hV : ∀ j ≤ Hw, 0 ≤ V j)
(hV0 : 0 ≤ V0)
(hDr0 : ∀ j ≤ Hw, 0 ≤ Dr j)
(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)
(hdrop :
∀ j ≤ Hw,
blockSize (blockSub (adaptedMean P (roundedGrid lAl mAl) (t - ↑j)) (adaptedMean P (roundedGrid lAl mAl) t)) F ≤ Dr j)
(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 (capsDeepConstant Cd g mAl G k0 s t)) kap 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 (capsDeepConstant Cd g mAl G k0 s t)) kap 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 kap) mAl
rho Hw (R ^ 4 * badMomentMajorant K (t + ↑G - 1 - sK)) (R / 2) lev t lAl V V0 Dr 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 kap)
mAl rho Hw (R ^ 4 * badMomentMajorant K (t + ↑G - 1 - sK)) (R / 2) lev t lAl V V0 Dr 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 entry caps bundle, at a released split level.