High-contrast homogenization: Provider.Quenched.SmallContrastLinearDecay

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

The linear level schedule's geometric conversion: hdecay at a law-free rate

second half. The exact log-level recursion of the squaring level schedule (linY_succ: y_{j+1} = 2y_j − log₃(128A²), hence z := y − log₃(128A²) doubles exactly), the per-round spacing bound s_j ≤ Cs·y_j with the single explicit constant linCs (every logarithm in the lags, memories, window counts, and pads is at most a multiple of the level logarithm once y_j ≥ 1), and the telescoping r_{j+1} − r_0 ≤ 4·Cs·z_j give

F n ≤ ((3:ℝ)^(−linRate))^(n − nStart) for n ≥ nStart := linR … 0,

with linRate := 1/(4·linCs) — an explicit function of (A, α, b₀, b_A, b₂, c_A, S₀) only: LAW-FREE at the instantiation where S₀ is the dimension-only lag channel, and the start nStart linear in ns + log₃S₁/b_A + log₃S₂/b₂ — the one-time burn-in.

noncomputable def HCPolySupport.HighContrast.Quenched.linY (A d0 : ℝ) (j : ℕ) : ℝ

The level logarithm.

Equations

• HCPolySupport.HighContrast.Quenched.linY A d0 j = Real.logb 3 (1 / HCPolySupport.HighContrast.Quenched.linLam A d0 j)

noncomputable def HCPolySupport.HighContrast.Quenched.linZ (A d0 : ℝ) (j : ℕ) : ℝ

The centered level logarithm: doubles exactly.

Equations

• HCPolySupport.HighContrast.Quenched.linZ A d0 j = HCPolySupport.HighContrast.Quenched.linY A d0 j - Real.logb 3 (128 * A ^ 2)

noncomputable def HCPolySupport.HighContrast.Quenched.linCs (A alpha b0 bA b2 : ℝ) (cA : ℕ) (S0 : ℝ) : ℝ

The single spacing constant.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def HCPolySupport.HighContrast.Quenched.linRate (A alpha b0 bA b2 : ℝ) (cA : ℕ) (S0 : ℝ) : ℝ

The law-free conclusion rate.

Equations

• HCPolySupport.HighContrast.Quenched.linRate A alpha b0 bA b2 cA S0 = 1 / (4 * HCPolySupport.HighContrast.Quenched.linCs A alpha b0 bA b2 cA S0)

theorem HCPolySupport.HighContrast.Quenched.linY_succ {A d0 : ℝ} (hA : 1 ≤ A) (hd0 : 0 < d0) (j : ℕ) : linY A d0 (j + 1) = 2 * linY A d0 j - Real.logb 3 (128 * A ^ 2)

theorem HCPolySupport.HighContrast.Quenched.linZ_succ {A d0 : ℝ} (hA : 1 ≤ A) (hd0 : 0 < d0) (j : ℕ) : linZ A d0 (j + 1) = 2 * linZ A d0 j

theorem HCPolySupport.HighContrast.Quenched.linZ_eq {A d0 : ℝ} (hA : 1 ≤ A) (hd0 : 0 < d0) (j : ℕ) : linZ A d0 j = 2 ^ j * linZ A d0 0

theorem HCPolySupport.HighContrast.Quenched.linZ_zero_ge {A d0 : ℝ} (hA : 1 ≤ A) (hd0 : 0 < d0) (hgs3 : (128 * A ^ 2) ^ 3 * d0 ≤ 1 / 3) : Real.logb 3 (128 * A ^ 2) + 1 ≤ linZ A d0 0

The base separation from the strengthened smallness.

theorem HCPolySupport.HighContrast.Quenched.linZ_one_le {A d0 : ℝ} (hA : 1 ≤ A) (hd0 : 0 < d0) (hgs3 : (128 * A ^ 2) ^ 3 * d0 ≤ 1 / 3) (j : ℕ) : 1 ≤ linZ A d0 j

theorem HCPolySupport.HighContrast.Quenched.linY_ge_linZ {A d0 : ℝ} (hA : 1 ≤ A) (j : ℕ) : linZ A d0 j ≤ linY A d0 j

theorem HCPolySupport.HighContrast.Quenched.linY_le_two_linZ {A d0 : ℝ} (hA : 1 ≤ A) (hd0 : 0 < d0) (hgs3 : (128 * A ^ 2) ^ 3 * d0 ≤ 1 / 3) (j : ℕ) : linY A d0 j ≤ 2 * linZ A d0 j

theorem HCPolySupport.HighContrast.Quenched.linLam_eq_rpow {A d0 : ℝ} (hA : 1 ≤ A) (hd0 : 0 < d0) (j : ℕ) : linLam A d0 j = 3 ^ (-linY A d0 j)

The level value in rpow form.

The spacing bound and the telescoping

theorem HCPolySupport.HighContrast.Quenched.linCs_one_le {A alpha b0 bA b2 : ℝ} {cA : ℕ} {S0 : ℝ} (hA : 1 ≤ A) (halpha : 0 < alpha) (hb0 : 0 < b0) (hbA : 0 < bA) (hb2 : 0 < b2) (hS0 : 1 ≤ S0) : 1 ≤ linCs A alpha b0 bA b2 cA S0

theorem HCPolySupport.HighContrast.Quenched.gs_of_gs3 {A d0 : ℝ} (hA : 1 ≤ A) (hd0 : 0 < d0) (hgs3 : (128 * A ^ 2) ^ 3 * d0 ≤ 1 / 3) : 128 * A ^ 2 * d0 ≤ 1

The strengthened smallness implies the plain one.

theorem HCPolySupport.HighContrast.Quenched.linSpacing_le {A alpha b0 bA b2 d0 S0 : ℝ} {cA j : ℕ} (hA : 1 ≤ A) (halpha : 0 < alpha) (hb0 : 0 < b0) (hbA : 0 < bA) (hb2 : 0 < b2) (hS0 : 1 ≤ S0) (hd0 : 0 < d0) (hgs3 : (128 * A ^ 2) ^ 3 * d0 ≤ 1 / 3) : ↑(max (linL A b0 S0 (linLam A d0 j)) (linT alpha d0 (linLam A d0 j)) + linII A (linLam A d0 j) * (cA + 1) + linPad A bA b2 (linLam A d0 j) + 1) ≤ linCs A alpha b0 bA b2 cA S0 * linY A d0 j

The per-round spacing is at most Cs times the level logarithm.

theorem HCPolySupport.HighContrast.Quenched.linR_telescope {ns cA : ℕ} {A alpha b0 bA b2 S0 S1 S2 d0 : ℝ} (hA : 1 ≤ A) (halpha : 0 < alpha) (hb0 : 0 < b0) (hbA : 0 < bA) (hb2 : 0 < b2) (hS0 : 1 ≤ S0) (hd0 : 0 < d0) (hgs3 : (128 * A ^ 2) ^ 3 * d0 ≤ 1 / 3) (j : ℕ) : ↑(linR ns cA A alpha b0 bA b2 S0 S1 S2 d0 j) ≤ ↑(linR ns cA A alpha b0 bA b2 S0 S1 S2 d0 0) + 2 * linCs A alpha b0 bA b2 cA S0 * (linZ A d0 j - linZ A d0 0)

The telescoping: the round starts stay within 2Cs centered levels.

theorem HCPolySupport.HighContrast.Quenched.linR_lower {ns cA : ℕ} {A alpha b0 bA b2 S0 S1 S2 d0 : ℝ} (j : ℕ) : linR ns cA A alpha b0 bA b2 S0 S1 S2 d0 0 + j ≤ linR ns cA A alpha b0 bA b2 S0 S1 S2 d0 j

The round starts grow at least linearly.

theorem HCPolySupport.HighContrast.Quenched.linear_descent_hdecay {A alpha d0 S0 S1 S2 b0 bA b2 : ℝ} {F : ℕ → ℝ} {src : ℕ → ℕ → ℝ} {ns cA : ℕ} (hA : 1 ≤ A) (halpha : 0 < alpha) (hcA : 24 * A ≤ 3 ^ (alpha * ↑cA)) (hd0 : 0 < d0) (hgs3 : (128 * A ^ 2) ^ 3 * d0 ≤ 1 / 3) (hS0 : 1 ≤ S0) (hS1 : 1 ≤ S1) (hS2 : 1 ≤ S2) (hb0 : 0 < b0) (hbA : 0 < bA) (hb2 : 0 < b2) (hFnn : ∀ (n : ℕ), 0 ≤ F n) (hFmono : ∀ (p q : ℕ), p ≤ q → F q ≤ F p) (hFd0 : ∀ (n : ℕ), F n ≤ d0) (hfam : ∀ (n m : ℕ), ns ≤ m → m ≤ n → F n ≤ A * iterationDropSum (3 ^ (-alpha)) F n + A * F m ^ 2 + src n m) (hsrc : ∀ (n m : ℕ), ns ≤ m → m ≤ n → src n m ≤ S1 * 3 ^ (-(bA * ↑m)) + S0 * 3 ^ (-(b0 * ↑(n - m))) + S2 * 3 ^ (-(b2 * ↑n))) : 0 < linRate A alpha b0 bA b2 cA S0 ∧ linRate A alpha b0 bA b2 cA S0 ≤ 1 ∧ ↑(linR ns cA A alpha b0 bA b2 S0 S1 S2 d0 0) ≤ ↑ns + Real.logb 3 (S1 / (A * d0 ^ 2)) / bA + Real.logb 3 (S2 / (A * d0 ^ 2)) / b2 + 2 ∧ ∀ (n : ℕ), linR ns cA A alpha b0 bA b2 S0 S1 S2 d0 0 ≤ n → F n ≤ (3 ^ (-linRate A alpha b0 bA b2 cA S0)) ^ (n - linR ns cA A alpha b0 bA b2 S0 S1 S2 d0 0)

The corrected-model descent in hdecay shape. Law-free rate linRate (a function of A, α, b₀, b_A, b₂, c_A, S₀ only), threshold linear in ns plus the one-time absolute burn-ins.