High-contrast homogenization: Provider.Entry.AdapterSeries

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

The geometric series of the adapted-to-Euclidean comparison

The proof of the comparison between adapted and Euclidean cubes splits the boundary layers of a cross-grid filling at the comparison generation k. The layers at or above it are paid by the annealed mean order, whose total relative volume is at most one; the layers below it are paid by the Euclidean cell bound E[𝐀(z+□_r)] ≤ (1 + 9K_{Ψ_S}^23^{-r})^g𝐄 against the cross-grid row weight C_d3^{r-n}, and their total is the printed geometric-series calculation

Σ_{r<k}3^{r-n}(1 + 9K^23^{-r})^g ≤ 20 Γ_{g,S}(k)3^{-(n-k)}.

Two elementary facts carry it. The power x ↦ x^g is subadditive for g ≤ 1, which separates the constant layer from the source layer; and the geometric series ζ_g = (1-3^{-(1-g)})^{-1} is at most 2(1-g)^{-1}, because t ↦ 3^{-t} is convex and therefore below its chord on [0,1]. The second is what turns the raw series into the printed gauge Γ_{g,S}(k) = (1-g)^{-1}(1+K^23^{-k})^g, whose prefactor is exactly one power of (1-g)^{-1}: a comparison that spent two powers of (1-g)^{-1} would not be the printed one.

The bound is uniform in the lower cutoff of the sum, which is what lets it survive the limit the filling exhaustion takes.

There are no definitions in this file.

theorem HCPolySupport.HighContrast.Entry.zetaG_le_two_div {g : ℝ} (hg0 : 0 ≤ g) (hg1 : g < 1) : zetaG g ≤ 2 / (1 - g)

The geometric series is at most 2(1-g)^{-1}. The map t ↦ 3^{-t} is convex, so on [0,1] it lies below its chord 1 - 2t/3; hence 1 - 3^{-(1-g)} ≥ 2(1-g)/3, which is the one power of (1-g)^{-1} the printed gauge carries.

theorem HCPolySupport.HighContrast.Entry.sum_belowSplit_le {g K : ℝ} (hg0 : 0 ≤ g) (hg1 : g < 1) (k n J : ℤ) : ∑ r ∈ Finset.Ico J k, 3 ^ (r - n) * (1 + 9 * K ^ 2 * 3 ^ (-r)) ^ g ≤ 20 * transferGauge g K k * 3 ^ (k - n)

The below-split series of the comparison. The layers below the comparison generation, weighted by the cross-grid row 3^{r-n} and bounded by the Euclidean cell bound, total at most twenty times the printed gauge times the printed rate — uniformly in the lower cutoff of the sum.