The abstract descent inequality of the admissible-exponent method
DisprovedQRH.energy_descentLet f be a sequence of real numbers with f(0) <= c whose steps satisfy f(i+1) <= A + B f(i) for every natural i, with B >= 0. Then for every i one has f(i) <= (c + i A) max(1, B)^i: a quantity that starts below c and at each step adds A and multiplies by B is after i steps bounded by (c + iA) times the contraction factor max(1, B)^i. This is the abstract descent inequality behind the termination of the canonical induction for the energy of the dual family.
import Mathlib import Definitions.Def_QRH_arith import Definitions.Def_QRH_sums import Definitions.Def_QRH_lfun
universe u
namespace QRH
/-- The abstract descent inequality of the admissible-exponent method
(section 6.5 of the source, following Heath-Brown): if a nonnegative
sequence starts below c and each step adds A and multiplies by B, then
after i steps it is bounded by (c + iA) times the contraction factor
max(1, B)^i. In the source the sequence is the normalized energy of the
dual family along the bands of the canonical induction — the row scale
contracts by D^(-2κ) at each application of the recursive inequality,
the transfer estimate supplies the additive term, and a bounded number
of steps exhausts the descent. -/
theorem energy_descent (f : ℕ → ℝ) (c A B : ℝ)
(hf0 : f 0 ≤ c)
(hstep : ∀ i : ℕ, f (i + 1) ≤ A + B * f i)
(hB : 0 ≤ B) :
∀ i : ℕ, f i ≤ (c + (i : ℝ) * A) * (max 1 B) ^ i := by
sorry
end QRH
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Read-back (self-check authored by the same model that produced the statement): the formal theorem takes f : N to R, constants c, A, B : R, the hypotheses f 0 <= c and f(i+1) <= A + B * f i for all i, and 0 <= B, and concludes f i <= (c + i * A) * max 1 B ^ i for every i. It is a self-contained induction over the naturals; the multiplicative constant max(1, B)^i is nondecreasing in B by the hypothesis 0 <= B, and the additive term accumulates linearly.