High-contrast homogenization: Provider.Quenched.SmallContrastSourcePolynomial #

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

The source constants are polynomial in the growth bar #

hentry needs an upper bound on 3 ^ N1, where N1 = sK + 1 + gap, and every factor of it must end up polynomial in the base 2 + aspectRatio Ebase * Kbase so's base-uniform machinery can convert it into a law-free exponent.

Three of the factors were already available; this file supplies the rest:

the ℤ-ceiling companion of's three_pow_ceil_logb_le, and with it a minimal gap — exists_gap_three_pow_le_minimal gives existence only, exactly as exists_source_scale_minimal did, and for the same reason that is not enough;
sourceMomentOne and sourceMomentSix against a power of the growth bar, the only obstacle being the Real.log inside them, which log x ≤ x - 1 removes;
badSourceConstant against sourceMomentSix, where the fractional powers are absorbed by y ^ c ≤ 1 + y for c ∈ [0,1].

Together with growthBar K ≤ 2 + aspectRatio E * K these put every source constant under a power of the base.

The `ℤ`-ceiling device, and a minimal gap #

source

theorem HCPolySupport.HighContrast.Quenched.three_zpow_ceil_logb_le {x : ℝ} (hx : 0 < x) :

3 ^ ⌈Real.logb 3 x⌉ ≤ 3 * x

The ℤ-ceiling companion of three_pow_ceil_logb_le.

source

theorem HCPolySupport.HighContrast.Quenched.exists_gap_three_pow_le_minimal {A sigma : ℝ} (hA : 0 < A) (hsigma : 0 < sigma) :

∃ (gap : ℤ), 1 ≤ gap ∧ A * 3 ^ (-↑gap) ≤ sigma ∧ 3 ^ gap ≤ 3 * max 1 (A / sigma)

The gap, chosen minimally. exists_gap_three_pow_le_minimal gives a gap that pushes the adapter error below tolerance; hentry also needs to know the gap is not much larger than the ratio it is built from.