High-contrast homogenization: Provider.Quenched.SmallContrastWeakCapSharpIsotropyAtLevel #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
The sharp weak caps at a released split level #
The two sharp caps at a parametrized normalizer, with the profile's split level free. Three constants move with the level and one majorant is replaced:
- the recent group's coefficient becomes
recentConstantAtLevel lev; - the maximum group's becomes
maxGroupConstantAtLevel lev; - the good branch's becomes
energyGoodConstantAtLevel lev; - the bad slot carries
profileBadMajorantAt 4 (R ^ 4 · badMomentMajorant K Δ) (R / 2) lev— the residue-free majorant at the matched threshold.
At lev = 1 and R = 1 the first three are the pinned numerals and the fourth
is the pinned majorant, so the pinned caps are the specialization. Everything
else — the five-group discharge, the measurability inputs, the recentering
identities — is the pinned proof unchanged.
theorem
HCPolySupport.HighContrast.Quenched.eLpNorm_profilePrimalWeakRoot_reference_le_sharp_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)
{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))
(h0 : Mat d)
(hh0 : IsSkewMat h0)
(p r : Vec d)
:
MeasureTheory.eLpNorm
(Response.profilePrimalWeakRoot m0 ⋯ t (fun (a : CoeffSpace d) => a.subSkew h0 hh0) p r
(Response.profilePrimalCenter P ⋯ t (fun (a : CoeffSpace d) => a.subSkew h0 hh0) p r))
2 P ≤ ENNReal.ofReal
(Response.recentConstantAtLevel lev * Response.diagonalWeakMetricFactor m0 (Response.skewBlockCongr h0 F) * Response.diagonalWeakLoadMinus (Response.skewBlockCongr h0 F) p r) * (∑ j ∈ Finset.range (Hw + 1), ENNReal.ofReal (3 ^ (-(1 / 2) * ↑j)) * weakScaleBudget P (roundedGrid l n) F t j + ∑ j ∈ Finset.range (Hw + 1),
ENNReal.ofReal (3 ^ (-(1 / 2 - rho / 2) * ↑j)) * ENNReal.ofReal
√(2 * ↑d * blockSize (blockSub (adaptedMean P (roundedGrid l n) (t - ↑j)) (adaptedMean P (roundedGrid l n) t))
F)) + ENNReal.ofReal
(Response.maxGroupConstantAtLevel lev * Response.diagonalWeakMetricFactor m0 (Response.skewBlockCongr h0 F) / (2 * ((1 - rho) / 2))) * (ENNReal.ofReal
(√2 * Response.profileEnergyLoad (Response.diagonalWeakLoadMinus F p (r - matVecMul h0 p)) p
(r - matVecMul h0 p) * Response.profileBadMajorantAt 4 (R ^ 4 * badMomentMajorant K (t + ↑G - 1 - sK)) (R / 2) lev) + ENNReal.ofReal
(Response.energyGoodConstantAtLevel lev * 3 ^ (-((1 - rho) / 2) * ↑Hw) * Response.profileEnergyLoad (Response.diagonalWeakLoadMinus F p (r - matVecMul h0 p)) p
(r - matVecMul h0 p))) + ENNReal.ofReal Response.constantSeminormCoefficient * (ENNReal.ofReal
(Response.diagonalWeakMetricFactor m0 (Response.skewBlockCongr h0 (adaptedMean P (roundedGrid l n) t)) * Response.diagonalWeakLoadMinus (Response.skewBlockCongr h0 (adaptedMean P (roundedGrid l n) t)) p r) * scaleVariance P (roundedGrid l n) (adaptedMean P (roundedGrid l n) t) t)
The sharp weak cap (primal), at a released split level.
theorem
HCPolySupport.HighContrast.Quenched.eLpNorm_profileAdjointWeakRoot_reference_le_sharp_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)
{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))
(h0 : Mat d)
(hh0 : IsSkewMat h0)
(p r : Vec d)
:
MeasureTheory.eLpNorm
(Response.profileAdjointWeakRoot m0 ⋯ t (fun (a : CoeffSpace d) => a.subSkew h0 hh0) p r
(Response.profileAdjointCenter P ⋯ t (fun (a : CoeffSpace d) => a.subSkew h0 hh0) p r))
2 P ≤ ENNReal.ofReal
(Response.recentConstantAtLevel lev * Response.diagonalWeakMetricFactor m0 (Response.skewBlockCongr h0 F) * Response.diagonalWeakLoadPlus (Response.skewBlockCongr h0 F) p r) * (∑ j ∈ Finset.range (Hw + 1), ENNReal.ofReal (3 ^ (-(1 / 2) * ↑j)) * weakScaleBudget P (roundedGrid l n) F t j + ∑ j ∈ Finset.range (Hw + 1),
ENNReal.ofReal (3 ^ (-(1 / 2 - rho / 2) * ↑j)) * ENNReal.ofReal
√(2 * ↑d * blockSize (blockSub (adaptedMean P (roundedGrid l n) (t - ↑j)) (adaptedMean P (roundedGrid l n) t))
F)) + ENNReal.ofReal
(Response.maxGroupConstantAtLevel lev * Response.diagonalWeakMetricFactor m0 (Response.skewBlockCongr h0 F) / (2 * ((1 - rho) / 2))) * (ENNReal.ofReal
(√2 * Response.profileEnergyLoad (Response.diagonalWeakLoadPlus F p (r + matVecMul h0 p)) p
(r + matVecMul h0 p) * Response.profileBadMajorantAt 4 (R ^ 4 * badMomentMajorant K (t + ↑G - 1 - sK)) (R / 2) lev) + ENNReal.ofReal
(Response.energyGoodConstantAtLevel lev * 3 ^ (-((1 - rho) / 2) * ↑Hw) * Response.profileEnergyLoad (Response.diagonalWeakLoadPlus F p (r + matVecMul h0 p)) p
(r + matVecMul h0 p))) + ENNReal.ofReal Response.constantSeminormCoefficient * (ENNReal.ofReal
(Response.diagonalWeakMetricFactor m0 (Response.skewBlockCongr h0 (adaptedMean P (roundedGrid l n) t)) * Response.diagonalWeakLoadPlus (Response.skewBlockCongr h0 (adaptedMean P (roundedGrid l n) t)) p r) * scaleVariance P (roundedGrid l n) (adaptedMean P (roundedGrid l n) t) t)
The sharp weak cap (adjoint), at a released split level.