Summability and Vanishing of an Energy Sequence

This formalizes the summation conclusion of Corollary 3.5 of Bizeul–Klartag–Lehec (arXiv:2610.05474v1).

Let $L,\chi,v:\mathbb N\to\mathbb R$ and let $a\in\mathbb R$. Assume:

1. $a>0$.
2. $L_i\ge0$, $\chi_i\ge0$, and $v_i\ge0$ for every $i\in\mathbb N$.
3. For every $i$,

Then both series $\sum_i v_i$ and $\sum_i\chi_i$ are summable, and

This is the abstract telescoping argument underlying the vanishing of the gradient-energy sequence in the tensor-energy iteration.

Original Lean declaration header

Within namespace FunctionalInequalities.Analysis.BakryEmery. Shown in its original module context. Proof omitted.

theorem summable_and_tendsto_zero_of_energy {L χ v : ℕ → ℝ} {a : ℝ} (ha : 0 < a)
    (hL : ∀ i, 0 ≤ L i) (hχ : ∀ i, 0 ≤ χ i) (hv : ∀ i, 0 ≤ v i)
    (h45 : ∀ i, L (i + 1) + χ i + a * v i ≤ L i) :
    Summable v ∧ Summable χ ∧ Tendsto v atTop (𝓝 0)

Module navigation

Module: Analysis/BakryEmery/TensorEnergy.

Source excerpt, lines 352–355 · Frozen source 408915f.