High-contrast homogenization: Provider.Quenched.RenormalizationParameterArithmetic

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

Arithmetic for the one-time renormalization

The parameter choices below are made before the probability law. They turn a single triadic bracket for the polynomial base into the window, inner-scale, and radius-buffer inequalities used by the renormalized dagger.

theorem HCPolySupport.HighContrast.Quenched.renorm_buffer_of_multiplier {d A B q : ℕ} {mu : ℝ} (hmu : 0 < mu) (hA : 1 ≤ A) (hq : 1 ≤ q) (hB : (2 * ↑A + ↑d * ↑A * Real.log 3) / frGaugeConst d + 1 ≤ 3 ^ (2 * mu * ↑B)) : Real.log (2 * renormCellCount d (A * q)) ≤ frGaugeConst d * (3 ^ (2 * mu * ↑(B * q)) - 1)

A fixed multiple of the base index absorbs the radius union-bound prefactor uniformly in that index.

theorem HCPolySupport.HighContrast.Quenched.mul_base_le_rpow_mul_index {C a : ℝ} {A q : ℕ} (ha : 0 < a) (hq : 1 ≤ q) (hcoef : 0 ≤ a * ↑A - a - 1) (hbase : C ≤ 3 ^ (a * ↑A - a - 1)) {base : ℝ} (hbase0 : 0 ≤ base) (hbase3 : base ≤ 3 ^ q) : C * base ≤ 3 ^ (a * ↑(A * q) - a)

A fixed exponent multiplier propagates a one-index triadic bound to every positive index.

theorem HCPolySupport.HighContrast.Quenched.exists_renormalization_parameters (d : ℕ) {g rho mu delta G0 : ℝ} (hdiff : 0 < rho - g) (hmu : 0 < mu) (hdelta : 0 < delta) (hdelta1 : delta < 1) (hG0 : 0 < G0) : ∃ (T : ℝ) (A : ℕ) (D : ℕ) (B : ℕ), 1 ≤ T ∧ Real.log 2 ≤ frGaugeConst d * T ^ 2 * (3 ^ (2 * mu) - 1) ∧ 1 ≤ A ∧ 0 ≤ (rho - g) * ↑A - 1 ∧ 12 / (1 + delta) ≤ 3 ^ ((rho - g) * ↑A - 1) ∧ 1 ≤ D ∧ 0 ≤ mu * ↑D - mu - 1 ∧ G0 * T / delta ≤ 3 ^ (mu * ↑D - mu - 1) ∧ 1 ≤ B ∧ (2 * ↑A + ↑d * ↑A * Real.log 3) / frGaugeConst d + 1 ≤ 3 ^ (2 * mu * ↑B)

Fixed parameters, chosen before the law, that absorb all dimensional constants in the one-time renormalization.