Scalar absorption of the actual endpoint source coefficients. The same estimate includes the terminal one-letter level; there is no extra derivative or time-zero regularity assumption.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_endpoint_coefficient_le {a e κ ν τ τP Cq Cg K L S : ℝ} (he : 0 < e) (hκ : 0 < κ) (hν : 0 < ν) (hτ : 0 < τ) (hτP : 0 < τP) (hCq : 0 ≤ Cq) (hCg : 0 ≤ Cg) (hL : 0 ≤ L) (hS : 0 ≤ S) (hRatio : e ^ 2 / (κ * τ) ≤ 1) (hTime : 8 * τ / τP ≤ 1) (hX : a ^ 2 * e ^ 4 / κ ≤ K * ν) (n r : ℕ) : 8 * (Cq * (a ^ 2 * e ^ 2) * (e ^ 2 / (κ * τ)) ^ n * (8 * τ) ^ r) * (Cg * S * (e ^ 2 / κ) / √ν * L * τP⁻¹ ^ r) ≤ 8 * Cq * Cg * K * √ν * L * S

Each endpoint coefficient is bounded uniformly in both finite indices.

theorem AVenhance.Infra.Section5.RelativeError.relative_initial_endpoint_coefficient_sum_le {a e κ ν τ τP Cq Cg K L S : ℝ} (he : 0 < e) (hκ : 0 < κ) (hν : 0 < ν) (hτ : 0 < τ) (hτP : 0 < τP) (hCq : 0 ≤ Cq) (hCg : 0 ≤ Cg) (hL : 0 ≤ L) (hS : 0 ≤ S) (hRatio : e ^ 2 / (κ * τ) ≤ 1) (hTime : 8 * τ / τP ≤ 1) (hX : a ^ 2 * e ^ 4 / κ ≤ K * ν) (N r : ℕ) : ∑ n ∈ Finset.range N, ENNReal.ofReal (8 * (Cq * (a ^ 2 * e ^ 2) * (e ^ 2 / (κ * τ)) ^ n * (8 * τ) ^ r) * (Cg * S * (e ^ 2 / κ) / √ν * L * τP⁻¹ ^ r)) ≤ ENNReal.ofReal (↑N * (8 * Cq * Cg * K * √ν * L * S))

The finite endpoint source coefficient sum has a constant independent of r.