Moment recurrence bound for histogram recursions

Let $h$ be a finite list of pairs $(w, c)$ (child width $w$ with multiplicity $c$) with $0 < w < m$, $m \ge 2$, $W > 0$, $0 < \tau \le 1$, and suppose the moment condition $\mu_\tau(h; m) < W$ (histMoment h m τ < W). If $c : \mathbb N \to \mathbb R$ is monotone and satisfies, for all $f \ge 1$,

then there is $A$ with $c(x) \le A\, x^{\tau}$ for all $x \ge 1$.

This is the cost recurrence of a recursive interchange network whose children are described by the histogram $h$.

In Lean:

theorem R6.MomentRec.moment_recurrence_bound (h : List (ℕ × ℕ)) (m W : ℕ) (τ K : ℝ) (c : ℕ → ℝ)
    (hm : 2 ≤ m) (hτ0 : 0 < τ) (hτ1 : τ ≤ 1)
    (hw : ∀ p ∈ h, 0 < p.1 ∧ p.1 < m) (hW : 0 < W)
    (hmom : histMoment h m τ < W) (hmono : Monotone c)
    (hrec : ∀ f : ℕ, 1 ≤ f →
      c (m * f) ≤ (h.map fun p => (p.2 : ℝ) * c (p.1 * f)).sum / W + K) :
    ∃ A : ℝ, ∀ x : ℕ, 1 ≤ x → c x ≤ A * (x : ℝ) ^ τ

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).