Exponential Laplace tails defeat any quadratic transform bound
ProvedAvramDividend.Classical.quadratic_exponential_tail_eventually_lt_oneasymptoticsavram-classicallaplace-transformm2m4strict-positivityunbounded-variation
For any positive tail threshold a and finite constants β0, C and K, there exists a Laplace parameter β≥β0 for which C(1+β²) exp(-(β-β0)a)K < 1. This is the quantitative contradiction needed to prove strictly positive scale functions from polynomial Lévy-exponent growth.
Preamble
import Mathlib open Filter
Formal statement
namespace AvramDividend.Classical
theorem quadratic_exponential_tail_eventually_lt_one
(a β0 C K : ℝ) (ha : 0 < a) :
∃ β : ℝ, β0 ≤ β ∧
C * (1 + β ^ 2) *
(Real.exp (-(β - β0) * a) * K) < 1 := by
sorry
end AvramDividend.ClassicalSource
Combination of Real.tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero and the positive-parameter exponential limit in the exact pinned Mathlib.