Dyadic Recursion Estimate

This technical lemma establishes the recursion used in the operator-route criterion.

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

1. $C>0$, $c\ge1$, $R\ge1$, and $d\ge1$.
2. $v_{k+1}\le(121/100)C^{-1}$ and $\chi_k\ge0$ for every $k$.
3. Every partial sum of $\chi$ is at most $L_0$, and $L_0\le( (11/10)C^{-1})^2$.
4. Whenever $j+1<N$, $0<\alpha_j$ and $\alpha_j^2\le3/C$.
5. $t_{d,k}\ge0$, $t_{d,k}\le R^{2d}v_{k+1}$, and, whenever $2d\le k+1$ and the preceding scale bounds hold,

Then

This is a neutral auxiliary estimate that packages the finite-index decomposition into the indices where the Taylor recursion applies and the at most $2d$ remaining indices.

Original Lean declaration header

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

private theorem recursion {C c R : ℝ} {v χ L α : ℕ → ℝ} {t : ℕ → ℕ → ℝ} {N d : ℕ}
    (hC : 0 < C) (hc : 1 ≤ c) (hR : 1 ≤ R) (hd : 1 ≤ d)
    (hvk : ∀ k, v (k + 1) ≤ 121 / 100 * C⁻¹)
    (hχ : ∀ k, 0 ≤ χ k) (hχsum : ∀ N, ∑ k ∈ range N, χ k ≤ L 0)
    (hL0 : L 0 ≤ (11 / 10 * C⁻¹) ^ 2)
    (hαN : ∀ j, j + 1 < N → 0 < α j ∧ α j ^ 2 ≤ 3 / C)
    (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) :
    ∑ k ∈ range (N - d), t d k ≤
      (c / C) ^ d * ∑ k ∈ range (N - 2 * d), t (2 * d) k +
        5 * d * c ^ d * C⁻¹ * R ^ (2 * d)

Module navigation

Module: KLS/BKL/PoissonIterate/Criterion.

Next: le_of_iterate_bounds.

Source excerpt, lines 151–164 · Frozen source 408915f.