High-contrast homogenization: Provider.Quenched.SmallContrastWeakValueBaseAbsorb

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

Absorbing released group coefficients into the base's normalizer

The line producer reads the weak base at the pinned group coefficients, and the released weak-norm chain produces it at coefficients that move with the split level. The two are reconciled without touching the line producer: the base's normalizer is a free parameter of the consumer's constant bundle, and each group is linear in it, so a coefficient above the pinned one is paid for by enlarging the normalizer.

This is the only reconciliation the released route needs on the value side; the threshold pair itself is carried through the line producer as a parameter.

theorem HCPolySupport.HighContrast.Quenched.weakValueBaseIsotropyAtPar_absorb {d : ℕ} {cfirst cmax M M' L rho bmaj beta lev : ℝ} {Hw : ℕ} {V : ℕ → ℝ} {V0 : ℝ} {Dr : ℕ → ℝ} {Vmean : ℝ} (hcf : cfirst * M ≤ 16 * M') (hcm : cmax * M ≤ 16 * M') (hMM : M ≤ M') (hrho1 : rho < 1) (hbmaj : 0 ≤ bmaj) (hbeta : 0 ≤ beta) (hV : ∀ (j : ℕ), 0 ≤ V j) (hV0 : 0 ≤ V0) (hDr : ∀ (j : ℕ), 0 ≤ Dr j) (hVmean : 0 ≤ Vmean) : weakValueBaseIsotropyAtPar cfirst cmax M L rho Hw bmaj beta lev V V0 Dr Vmean ≤ weakValueBaseIsotropyAtPar 16 16 M' L rho Hw bmaj beta lev V V0 Dr Vmean

The absorption. A parametrized base at released coefficients is dominated by the pinned-coefficient base at an enlarged normalizer.