Karamata's Tauberian theorem in Lean 4/Mathlib in ~490 lines: proof layout

Laplace form for nonnegative sequences: x^ρ Σ aₙ e^{-xn} → C as x→0⁺ implies (a₀+…+a_N)/N^ρ → C/Γ(ρ+1). Define T_N(g) = N^{-ρ} Σ' aₙ g(e^{-n/N}) and L(g) = C/Γ(ρ) ∫_{Ioi 0} t^{ρ-1} g(e^{-t}). For monomials y^k, apply the hypothesis at x = k/N (via exp(-(n/N))^k = exp(-((k/N)n)) from Real.exp_nat_mul), and use integral_rpow_mul_exp_neg_mul_Ioi for L. Extend to y·P(y) with Polynomial.eval_eq_sum_range and Summable.tsum_finsetSum. To squeeze the indicator of [e^{-1},1], approximate ramp(y)/max(y,b) by exists_polynomial_near_of_continuousOn. Writing the ramp divided by max(y,b) makes continuity at 0 automatic, and y·(that) equals the ramp. Bound L(ramp) by integrals of t^{ρ-1}·1_{t ≤ 1±θ}, which are explicit, (1±θ)^ρ/ρ. This avoids any 'measure of the boundary is 0' argument. Finish with tendsto_order. Integrability of t^{ρ-1}e^{-kt} comes for free from Integrable.of_integral_ne_zero, because the integral is Γ(ρ)/k^ρ ≠ 0.