High-contrast homogenization: Provider.Quenched.EndpointRelativeRowFamily #
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Endpoint-relative row decay from a growing radius family #
The stopping generation selects one member of the growing renormalization family. The successful branch uses that member's radius; the fallback branch uses the uniform coarse-ellipticity estimate.
theorem
HCPolySupport.HighContrast.Quenched.quenched_block_row_le_stoppingGeneration_of_endpoint_family
{d : ℕ}
[NeZero d]
{g gamma rho delta eta Cblk : ℝ}
{E Abar : BlockMat d}
{S : CoeffSpace d → ℝ}
{Ahat : ℕ → BlockMat d}
{radius : ℕ → CoeffSpace d → ℝ}
{nstar qfb q0 A L : ℕ}
{a : CoeffSpace d}
(hnstar : nstar = L * q0)
(hgamma0 : 0 ≤ gamma)
(hgr : g ≤ gamma)
(hgammaRho : gamma < rho)
(hdelta : 0 < delta)
(heta : 0 < eta)
(hL : 0 < L)
(hAbarSymm : IsSymmetricBlockMat Abar)
(hAbar : Book.Ch02.BlockPosDef 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))
(hradius :
∀ (n : ℕ),
nstar ≤ n →
radius n a = renormRadius S (Ahat n) (endpointTolerance delta eta q0 L n) gamma (endpointWindowLength A L n) n a)
(hwindow :
∀ (n : ℕ),
nstar ≤ n →
∃ (h : ℕ),
h = endpointWindowLength A L n ∧ renormScale S (Ahat n) (endpointTolerance delta eta q0 L n) gamma h n a ≠ ⊤ ∧ Book.Ch02.BlockPosDef (Ahat n) ∧ BlockMatLoewnerLE E (blockScale (2 * kappaRef E) (Ahat n)) ∧ BlockMatLoewnerLE (Ahat n) (blockScale (1 + endpointTolerance delta eta q0 L n) Abar) ∧ 2 * kappaRef E ≤ endpointTolerance delta eta q0 L n * 3 ^ ((gamma - g) * ↑h))
(hdeltaOne : delta ≤ 1)
(hCblkPos : 0 < Cblk)
(hCblk : 4 * 3 ^ eta * (1 - 3 ^ (-(rho - gamma)))⁻¹ ≤ Cblk)
(hfallback :
∀ (m : ℕ), nstar ≤ m → S a ≤ 3 ^ m → quenchedBlockRow rho Abar (S a) a m ≤ Cblk * delta * 3 ^ (eta / ↑L * ↑qfb))
(m : ℕ)
:
Pointwise assembly of the successful and fallback branches of the endpoint-relative row estimate.