High-contrast homogenization: Provider.Quenched.SmallContrastEntryRateParts

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

The three source-decay parts of the entry estimate

the corresponding argument named three missing sub-estimates behind hentry; this file supplies them, each with its constant named, and repairs a rate leak found on the way.

The leak. The slot-source split bounds the weighted slot source by (H_w+1)·(c₁+c₂+c₃)·3^{-J/2}. The factor H_w + 1 is an artefact of the coarse shallow exponent e ≥ 1/2 used there: the shallow legs are then bounded by 3^{-j/2}·3^{-(J-j)/2} = 3^{-J/2}, a constant in j, and summing J+1 of them costs the window height. In the construction the shallow exponent is e = d/2, which for d ≥ 2 is at least 1; then the shallow legs are bounded by 3^{-J/2}·3^{-(J-j)/2}, which is geometric in the lag, and the sum is halfGeom·3^{-J/2} with no window factor at all.

This matters because the margin is exactly nil: the deep-leg source decays at rate 1/2 in the lag J, J ≈ n/4 per generation, so the achievable rate is 1/8 per generation, and recursionAlpha 0 = 1/8. Any extra polynomial factor destroys the rate at g = 0. slot_source_sum_split_sharp removes it.

The three parts.

• (a) slotVsumSharp_le — the variance leg, ≤ C_v·3^{-J/2};
• (b) the profile bad-majorant moment bound — the bad-event leg, ≤ C_b·3^{-Δ/2} in the absolute-generation gap Δ;
• (c) the window-tail bound, 3^{-contrastAlpha g·H_w}, restated at a common rate.

The half-step ratio

noncomputable def HCPolySupport.HighContrast.Quenched.halfRatio : ℝ

The one-step ratio of the linear weight, 3^{-1/2}.

Equations

• HCPolySupport.HighContrast.Quenched.halfRatio = 3 ^ (-(1 / 2))

theorem HCPolySupport.HighContrast.Quenched.halfRatio_pos : 0 < halfRatio

theorem HCPolySupport.HighContrast.Quenched.halfRatio_lt_one : halfRatio < 1

theorem HCPolySupport.HighContrast.Quenched.halfGeom_eq_inv : halfGeom = (1 - halfRatio)⁻¹

theorem HCPolySupport.HighContrast.Quenched.halfGeom_one_le : 1 ≤ halfGeom

theorem HCPolySupport.HighContrast.Quenched.linWeight_eq_pow (j : ℕ) : linWeight j = halfRatio ^ j

theorem HCPolySupport.HighContrast.Quenched.halfRatio_geom_sum_le (m : ℕ) : ∑ k ∈ Finset.range m, halfRatio ^ k ≤ halfGeom

theorem HCPolySupport.HighContrast.Quenched.halfRatio_sq : halfRatio ^ 2 = 3 ^ (-1)

theorem HCPolySupport.HighContrast.Quenched.rpow_neg_one_mul_eq_pow (m : ℕ) : 3 ^ (-1 * ↑m) = halfRatio ^ (2 * m)

The unit-rate weight is the square of the half-rate weight.

theorem HCPolySupport.HighContrast.Quenched.rpow_neg_mul_le_pow {e : ℝ} (he : 1 ≤ e) (m : ℕ) : 3 ^ (-e * ↑m) ≤ halfRatio ^ (2 * m)

A shallow leg at exponent at least one is dominated by the unit-rate leg.

The sharp slot-source summation

theorem HCPolySupport.HighContrast.Quenched.slot_source_sum_split_sharp {Hw J : ℕ} {vs : ℕ → ℝ} {c1 c2 c3 e : ℝ} (hc1 : 0 ≤ c1) (hc2 : 0 ≤ c2) (hc3 : 0 ≤ c3) (he : 1 ≤ e) (hshallow : ∀ j ∈ Finset.range (Hw + 1), j ≤ J → vs j ≤ c1 * 3 ^ (-e * ↑(J - j)) + c2 * 3 ^ (-1 * ↑(J - j))) (hdeep : ∀ j ∈ Finset.range (Hw + 1), J ≤ j → vs j ≤ c3) : ∑ j ∈ Finset.range (Hw + 1), linWeight j * vs j ≤ halfGeom * (c1 + c2 + c3) * halfRatio ^ J

The sharp slot-source summation. With the shallow exponent at least one — which is e = d/2 at d ≥ 2 — the weighted source sum is geometric in the lag, with no factor of the window height.

Part (a): the variance leg

theorem HCPolySupport.HighContrast.Quenched.one_le_half_dim {d : ℕ} (hd : 2 ≤ d) : 1 ≤ ↑d / 2

The shallow exponent d/2 is at least one at d ≥ 2.

theorem HCPolySupport.HighContrast.Quenched.slotSourceSeq_sum_le_sharp {d : ℕ} (hd : 2 ≤ d) {Csub Msc delta : ℝ} (hCsub : 0 ≤ Csub) (hMsc : 0 ≤ Msc) (hdelta : 0 ≤ delta) (Hw J : ℕ) : ∑ j ∈ Finset.range (Hw + 1), linWeight j * slotSourceSeq d Csub Msc delta J j ≤ halfGeom * (√(2 * ↑d) * 18 * Csub * Msc + √(2 * ↑d) * 288 + deepSlotConstant d Csub Msc delta) * halfRatio ^ J

The sharp summed source of the slot family. Identical to slotSourceSeq_sum_le_sharp except that the window-height factor is gone.

noncomputable def HCPolySupport.HighContrast.Quenched.slotVsumSharp (d : ℕ) (Csub Msc delta : ℝ) (J : ℕ) : ℝ

The sharp summed source constant — the window-height-free replacement for slotVsumSharp.

Equations

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

theorem HCPolySupport.HighContrast.Quenched.hVsum_of_family_sharp {d : ℕ} (hd : 2 ≤ d) {Csub Msc delta Fjb : ℝ} (hCsub : 0 ≤ Csub) (hMsc : 0 ≤ Msc) (hdelta : 0 ≤ delta) (hFjb : 0 ≤ Fjb) (Hw J : ℕ) : ∑ j ∈ Finset.range (Hw + 1), linWeight j * (slotFamilyValue d Csub Msc delta Fjb J j + slotFamilyValue d Csub Msc delta Fjb J 0) ≤ slotVsumSharp d Csub Msc delta J + slotCVsum d * Fjb

The hVsum hypothesis at the sharp constant. Drop-in replacement for hVsum_of_family_sharp, with the same base coefficient slotCVsum d.

noncomputable def HCPolySupport.HighContrast.Quenched.vsumSourceConstant (d : ℕ) (Csub Msc delta : ℝ) : ℝ

The variance leg's source constant.

Equations

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

theorem HCPolySupport.HighContrast.Quenched.slotVsumSharp_le {d : ℕ} (hd : 2 ≤ d) {Csub Msc delta : ℝ} (hCsub : 0 ≤ Csub) (hMsc : 0 ≤ Msc) (J : ℕ) : slotVsumSharp d Csub Msc delta J ≤ vsumSourceConstant d Csub Msc delta * halfRatio ^ J

Part (a): the variance leg decays at the half rate in the lag.

Part (b): the bad-event leg

noncomputable def HCPolySupport.HighContrast.Quenched.badSourceConstant (K : ℝ) : ℝ

The bad-event leg's source constant.

Equations

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

theorem HCPolySupport.HighContrast.Quenched.badSourceConstant_nonneg (K : ℝ) : 0 ≤ badSourceConstant K

Part (c): the window tail, and the common-rate comparison

theorem HCPolySupport.HighContrast.Quenched.one_sub_contrastRho_half_eq (g : ℝ) : (1 - contrastRho g) / 2 = contrastAlpha g

The window tail's rate is the corrected rooted rate.

theorem HCPolySupport.HighContrast.Quenched.three_rpow_neg_le {a b : ℝ} (hab : b ≤ a) : 3 ^ (-a) ≤ 3 ^ (-b)

Part (c): a slower decay dominates a faster one. The single comparison that puts the three legs on a common rate.

theorem HCPolySupport.HighContrast.Quenched.halfRatio_pow_le {r : ℝ} {J : ℕ} (hr : r ≤ 1 / 2 * ↑J) : halfRatio ^ J ≤ 3 ^ (-r)

The half-rate weight in the lag, as a rate comparison.