A factorial induction with the corrected factor two.
theorem
AVenhance.Infra.Section4.theta_analytic_bound_of_energy_recursion
{E M : ℕ → ℝ}
{B R L κ : ℝ}
(hB : 0 < B)
(hR : 0 < R)
(hL : 0 < L)
(hκ : 0 < κ)
(hE0 : E 0 ≤ B)
(hMnonneg : ∀ (q : ℕ), 0 ≤ M q)
(hLinitial : 2 / R ≤ L)
(hQ1scale : ∀ (n : ℕ), 1 ≤ n → 4 * √(↑n * M 2 / κ) * ↑(n - 1).factorial * L ^ (n - 1) ≤ 1 / 4 * ↑n.factorial * L ^ n)
(hHighscale :
∀ (n : ℕ),
1 ≤ n →
(4 * ∑ q ∈ Finset.range (n + 1),
if 2 ≤ q then ↑(n.choose q) * (M q / κ) * ↑(n - q).factorial * L ^ (n - q) else 0) ≤ 1 / 4 * ↑n.factorial * L ^ n)
(hrec :
∀ (n : ℕ),
1 ≤ n →
E n ≤ 2 * B * (↑n.factorial / R ^ n) + 4 * √(↑n * M 2 / κ) * E (n - 1) + 4 * ∑ q ∈ Finset.range (n + 1), if 2 ≤ q then ↑(n.choose q) * (M q / κ) * E (n - q) else 0)
(n : ℕ)
: