High-contrast homogenization: Provider.Quenched.SmallContrastWeakValueSharpIsotropyAtLevel #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The sharp weak values at a released split level #
The two weak quantities against the released sharp weak value. The three coefficients are the ones the released weak-norm chain produces, and the bad slot carries the residue-free majorant at the matched threshold. Everything else is the pinned proof: the six load bounds, the budget comparison, the three group bounds and the assembly are unchanged.
theorem
HCPolySupport.HighContrast.Quenched.profilePrimalWeakQuantity_le_weakValueSharp_of_block_at_level
{d : ℕ}
[NeZero 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)
{n : Mat d}
(hn : Matrix.PosDef n)
(hgrid : IsRoundedGrid l (roundedGrid l n))
{m0 : Mat d}
(hm0 : Matrix.PosDef m0)
{rho : ℝ}
(hrho0 : 0 < rho)
(hrho1 : rho < 1)
(t : ℤ)
(Hw : ℕ)
(hstart : l ≤ t - ↑Hw)
{G : ℕ}
{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 l n) t F a ≤ ENNReal.ofReal (R * (max 1 (3 * S a * 3 ^ (-(↑t + ↑G))) ^ g / 2)))
{sK : ℤ}
(hsK : growthBar K ≤ 3 ^ sK)
(hDelta : 0 ≤ t + ↑G - 1 - sK)
(hintAll : ∀ (k : ℤ), HasFiniteAdaptedMean P (roundedGrid l n) k)
(hEt : Book.Ch02.BlockPosDef (adaptedMean P (roundedGrid l n) t))
{S0 SStar0 K0 : Mat d}
(hS0 : Matrix.PosDef S0)
(hStar0 : Matrix.PosDef SStar0)
(hform : toFullBlockMat (adaptedMean P (roundedGrid l n) 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 l n) t) X))
{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 l n) F (t - ↑j) ≤ ENNReal.ofReal (V j))
(hvart : scaleVariance P (roundedGrid l n) F t ≤ ENNReal.ofReal V0)
(hdrop :
∀ j ≤ Hw,
blockSize (blockSub (adaptedMean P (roundedGrid l n) (t - ↑j)) (adaptedMean P (roundedGrid l n) t)) F ≤ Dr j)
(hvmean : scaleVariance P (roundedGrid l n) (adaptedMean P (roundedGrid l n) t) t ≤ ENNReal.ofReal Vmean)
(e : Vec d)
(he : e ⬝ᵥ e = 1)
:
Response.profilePrimalWeakQuantity P m0 ⋯ 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 m0 (Response.responseSkew K0) F (loadScaleOfScalar cF kap) n rho Hw
(R ^ 4 * badMomentMajorant K (t + ↑G - 1 - sK)) (R / 2) lev t l V V0 Dr Vmean)
The primal weak quantity by the released sharp weak value.
theorem
HCPolySupport.HighContrast.Quenched.profileAdjointWeakQuantity_le_weakValueSharp_of_block_at_level
{d : ℕ}
[NeZero 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)
{n : Mat d}
(hn : Matrix.PosDef n)
(hgrid : IsRoundedGrid l (roundedGrid l n))
{m0 : Mat d}
(hm0 : Matrix.PosDef m0)
{rho : ℝ}
(hrho0 : 0 < rho)
(hrho1 : rho < 1)
(t : ℤ)
(Hw : ℕ)
(hstart : l ≤ t - ↑Hw)
{G : ℕ}
{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 l n) t F a ≤ ENNReal.ofReal (R * (max 1 (3 * S a * 3 ^ (-(↑t + ↑G))) ^ g / 2)))
{sK : ℤ}
(hsK : growthBar K ≤ 3 ^ sK)
(hDelta : 0 ≤ t + ↑G - 1 - sK)
(hintAll : ∀ (k : ℤ), HasFiniteAdaptedMean P (roundedGrid l n) k)
(hEt : Book.Ch02.BlockPosDef (adaptedMean P (roundedGrid l n) t))
{S0 SStar0 K0 : Mat d}
(hS0 : Matrix.PosDef S0)
(hStar0 : Matrix.PosDef SStar0)
(hform : toFullBlockMat (adaptedMean P (roundedGrid l n) 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 l n) t) X))
{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 l n) F (t - ↑j) ≤ ENNReal.ofReal (V j))
(hvart : scaleVariance P (roundedGrid l n) F t ≤ ENNReal.ofReal V0)
(hdrop :
∀ j ≤ Hw,
blockSize (blockSub (adaptedMean P (roundedGrid l n) (t - ↑j)) (adaptedMean P (roundedGrid l n) t)) F ≤ Dr j)
(hvmean : scaleVariance P (roundedGrid l n) (adaptedMean P (roundedGrid l n) t) t ≤ ENNReal.ofReal Vmean)
(e : Vec d)
(he : e ⬝ᵥ e = 1)
:
Response.profileAdjointWeakQuantity P m0 ⋯ 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 m0 (Response.responseSkew K0) F (loadScaleOfScalar cF kap) n rho Hw
(R ^ 4 * badMomentMajorant K (t + ↑G - 1 - sK)) (R / 2) lev t l V V0 Dr Vmean)
The adjoint weak quantity by the released sharp weak value.