RelativeError: abstract low/high frequency recombination

This module isolates the scalar part of the RelativeError trace/tail argument. The Fourier trace estimate, analytic tail estimate, and mean-zero energy estimate are inputs to e44_combine_low_mode_and_analytic_tail; the exponential absorption needed to use them is stated explicitly.

theorem AVenhance.Infra.Section5.RelativeError.e44_combine_low_mode_and_analytic_tail {n : ℕ} {r R A ν S N Cₚ Cₜ c : ℝ} (hr : 0 < r) (hR : r ≤ R) (hA : 1 ≤ A) (hν : 0 < ν) (hS : 0 ≤ S) (hN : 0 ≤ N) (hCp : 0 ≤ Cₚ) (hCt : 1 ≤ Cₜ) (habs : (√ν)⁻¹ * Real.exp (-c * R * (A / r)) ≤ 1) (hPoincare : N ≤ Cₚ * (√ν)⁻¹ * S) (low high total : ℝ) (hlow : low ≤ 2 * Real.exp 1 * (A / r) ^ n * S) (hhigh : high ≤ Cₜ * ↑n.factorial * (Cₜ / R) ^ n * Real.exp (-c * R * (A / r)) * N) (htotal : total ≤ low + high) : total ≤ (2 * Real.exp 1 + Cₜ * Cₚ) * ↑n.factorial * (max A Cₜ / r) ^ n * S

Combine a dissipation-controlled low-frequency estimate with an analytic high-frequency tail estimate. The hypothesis habs is the precise numeric absorption of the Poincare loss by the exponential tail. It is kept separate from any parameter-sequence instantiation, as in RelativeError (6)--(7).