High-contrast homogenization: Provider.Quenched.SmallContrastAbsorptionChoice

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

The absorption lag and gain choice

For every response constant Cpre ≥ 1 there are a lag H ≥ 4 and a Young gain eta > 0 with Cpre·eta + (3/2)·Cpre·3^{-H} ≤ 1/2. This is the scalar choice that the compact pre-Young reabsorption requires; the lag is dimension-dependent through Cpre and is selected before the law.

theorem HCPolySupport.HighContrast.Quenched.exists_absorption_lag_choice {Cpre : ℝ} (hCpre : 1 ≤ Cpre) : ∃ (H : ℕ) (eta : ℝ), 4 ≤ H ∧ 0 < eta ∧ Cpre * eta + 3 / 2 * Cpre * 3 ^ (-↑H) ≤ 1 / 2

The absorption choice: eta := (4·Cpre)⁻¹ and H := max 4 ⌈log₃(6·Cpre)⌉.