Iterate Bounds Imply the Final Criterion

This formalizes the final real-sequence argument of Bizeul–Klartag–Lehec (arXiv:2610.05474v1), p. 17, in the operator route.

Let $C,c,R\in\mathbb R$, sequences $v,p,\chi,L,\alpha:\mathbb N\to\mathbb R$, and $t:\mathbb N\to\mathbb N\to\mathbb R$ be given. Assume:

1. $C>0$, $c\ge1$, and $R\ge1$; $v_k\ge0$, $C^{-1}\le v_0$, and $v_k\to0$.
2. For every $N$, $v_0=v_N+\sum_{k<N}p_k$.
3. $\chi_k\ge0$, $\sum_{k<N}\chi_k\le L_0$, and $L_0\le((11/10)C^{-1})^2$.
4. $L_{k+1}\le L_k$ and $L_{k+1}=\alpha_k^2v_{k+1}$.
5. $\alpha_k\ge0$, $\alpha_k=0$ implies $v_{k+1}=0$, and $\alpha_k>0$ implies $C^{-1}\le\alpha_k^2$.
6. $t_{d,k}\ge0$, $t_{d,k}\le R^{2d}v_{k+1}$ for $d\ge1$, and the recursion bound from (63) holds whenever $2d\le k+1$ and all earlier scales are positive with square at most $3/C$.
7. For every $N$, if $\alpha_j^2\le3/C$ whenever $j+1<N$, then

Then

This is the scalar terminal estimate that converts the iterate identities, Taylor bounds, and defect recursion into a Poincaré-constant bound.

Original Lean declaration header

Within namespace FunctionalInequalities.KLS.LogConcave.PoissonIterate. Shown in its original module context. Proof omitted.

theorem le_of_iterate_bounds {C c R : ℝ} {v p χ L α : ℕ → ℝ} {t : ℕ → ℕ → ℝ}
    (hC : 0 < C) (hc : 1 ≤ c) (hR : 1 ≤ R)
    (hv : ∀ k, 0 ≤ v k) (hv0 : C⁻¹ ≤ v 0) (hvlim : Tendsto v atTop (𝓝 0))
    (h36 : ∀ N, v 0 = v N + ∑ k ∈ range N, p k)
    (hχ : ∀ k, 0 ≤ χ k) (hχsum : ∀ N, ∑ k ∈ range N, χ k ≤ L 0)
    (hL0 : L 0 ≤ (11 / 10 * C⁻¹) ^ 2) (hL : ∀ k, L (k + 1) ≤ L k)
    (h46 : ∀ k, L (k + 1) = α k ^ 2 * v (k + 1))
    (hα : ∀ k, 0 ≤ α k) (hα0 : ∀ k, α k = 0 → v (k + 1) = 0)
    (h32 : ∀ k, 0 < α k → C⁻¹ ≤ α k ^ 2)
    (ht : ∀ d k, 0 ≤ t d k)
    (htaylor : ∀ d k, 1 ≤ d → t d k ≤ R ^ (2 * d) * v (k + 1))
    (hJ1 : ∀ k d, 1 ≤ d → 2 * d ≤ k + 1 → (∀ j < k, 0 < α j ∧ α j ^ 2 ≤ 3 / C) →
      t d k ≤ (c / C) ^ d * t (2 * d) (k - d) +
        c ^ d * R ^ (2 * d) * C * ∑ j ∈ Ico (k + 1 - 2 * d) k, χ j)
    (hJ2 : ∀ N, (∀ j, j + 1 < N → α j ^ 2 ≤ 3 / C) →
      ∑ k ∈ range N, p k ≤ L 0 + 3 / C * ∑ k ∈ range (N - 1), t 1 k) :
    C ≤ 100 * c ^ 2 * R ^ 2

Module navigation

Module: KLS/BKL/PoissonIterate/Criterion.

Supporting theorems: recursion.

Previous: recursion · Next: norm_taylorField_sq_le.

Source excerpt, lines 278–294 · Frozen source 408915f.