High-contrast homogenization: Provider.Quenched.RenormalizedRowDecay #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Block-row decay below a renormalized stopping radius #
The renormalized radius controls the recent cells by an additive comparison. The original coarse-ellipticity datum controls the older cells, where the growing window absorbs the reference loss. Keeping these two cases separate preserves the small factor that is lost when they are bundled into a new coarse-ellipticity datum.
theorem
HCPolySupport.HighContrast.Quenched.quenched_block_row_le_of_renormRadius_le
{d : ℕ}
[NeZero d]
{g gamma rho delta eps : ℝ}
{E Ahat Abar : BlockMat d}
{S : CoeffSpace d → ℝ}
{n h m : ℕ}
{a : CoeffSpace d}
(hgamma0 : 0 ≤ gamma)
(hgr : g ≤ gamma)
(hgammaRho : gamma < rho)
(hdelta : delta ∈ Set.Icc 0 1)
(heps : eps ∈ Set.Icc 0 1)
(hAhat : Book.Ch02.BlockPosDef Ahat)
(hAbarSymm : IsSymmetricBlockMat Abar)
(hAbar : Book.Ch02.BlockPosDef Abar)
(href : BlockMatLoewnerLE E (blockScale (2 * kappaRef E) Ahat))
(hcomp : BlockMatLoewnerLE Ahat (blockScale (1 + eps) Abar))
(hburn : 2 * kappaRef E ≤ delta * 3 ^ ((gamma - g) * ↑h))
(hcoarse :
∀ (M : ℤ),
S a ≤ 3 ^ M →
∀ k ≤ M,
∀ (w : Fin d → ℤ),
standardCellCenter k w ∈ centeredCube d M →
BlockMatLoewnerLE (coarseBlock (standardCell d k w) a) (blockScale (3 ^ (g * (↑M - ↑k))) E))
(hfin : renormScale S Ahat delta gamma h n a ≠ ⊤)
(hnm : n ≤ m)
(hradius : renormRadius S Ahat delta gamma h n a ≤ 3 ^ m)
(hsource : S a ≤ 3 ^ m)
:
A single renormalized window gives a geometrically summable block-row bound. The small parameters are kept additive in the conclusion.
theorem
HCPolySupport.HighContrast.Quenched.quenched_block_row_le_fallback
{d : ℕ}
[NeZero d]
{g rho eps : ℝ}
{E Ahat Abar : BlockMat d}
{S : CoeffSpace d → ℝ}
{a : CoeffSpace d}
{m : ℕ}
(hg : 0 ≤ g)
(hgrho : g < rho)
(heps : eps ∈ Set.Icc 0 1)
(hAbarSymm : IsSymmetricBlockMat Abar)
(hAbar : Book.Ch02.BlockPosDef Abar)
(hkappa : 0 ≤ kappaRef E)
(href : BlockMatLoewnerLE E (blockScale (2 * kappaRef E) Ahat))
(hcomp : BlockMatLoewnerLE Ahat (blockScale (1 + eps) Abar))
(hcoarse :
∀ (M : ℤ),
S a ≤ 3 ^ M →
∀ k ≤ M,
∀ (w : Fin d → ℤ),
standardCellCenter k w ∈ centeredCube d M →
BlockMatLoewnerLE (coarseBlock (standardCell d k w) a) (blockScale (3 ^ (g * (↑M - ↑k))) E))
(hsource : S a ≤ 3 ^ m)
:
The original coarse-ellipticity estimate gives a uniform fallback row bound whenever the source cutoff is active.