High-contrast homogenization: Provider.Quenched.SmallContrastWeakGroups #

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

The three-group split of the sharp weak value #

hrec_final_sharp_at_jb_src consumes the weak base in the shape

W ≤ u + v·F(j_b) + w, w² ≤ c_drop · iterationDropSum r F n,

with u the source group, v·F(j_b) the base-scale group (which squares into the recursion's quadratic slot) and w the drop group. This file performs that split for weakValueSharpMajorant_le_three_group_summed_at_level, from per-slot bounds of exactly the shape the (repaired) lagged variance supply and the mean-drop carrier produce:

every variance slot — V j, V0, Vmean — is ≤ vsrc + cV·F(j_b);
every drop slot is ≤ c_D·(F(n-j) - F n);
the bad-event group and the window tail are ≤ bsrc.

The output constants are explicit; in particular the source constant

C_src = (32·M·√L·(1-3^{-1/2})⁻¹ + c_const·M·√7)·vsrc + (16·M/(1-ρ))·bsrc

is named here (weakSourceGroup), which is what the polynomial bootstrap entry needs.

The two drop conversions are read at the same rate: the linear slot's weight is 3^{-1/2} and the rooted slot's is 3^{-(1/2-ρ/2)} = 3^{-α}, and iterationDropSum is increasing in its ratio (iterationDropSum_mono_r), so both land on iterationDropSum (3^{-α}) F n whenever α ≤ 1/2.

source

noncomputable def HCPolySupport.HighContrast.Quenched.halfGeom :

ℝ

The geometric constant of the linear weight 3^{-1/2}.

Equations