Scalar closure of the normalized all-order recurrence in l.V. This module is algebraic: application to the actual iterates additionally requires derivation of the recurrence from their differentiated equations.

theorem AVenhance.Infra.Section4.iterate_geometric_kernel_le_two {r : ℝ} (hr : 0 ≤ r) (hrhalf : r ≤ 1 / 2) (n : ℕ) : ∑ k ∈ Finset.range n, r ^ k ≤ 2

The two geometric convolution kernels in the source have mass at most two.