Exponential Decay Integrability Lemmas (Tail Regime)

This file provides pure real analysis lemmas for integrability of exponentially decaying functions in the tail regime (t → ∞), particularly polynomial × exponential patterns.

These lemmas are designed to be reusable for contour integral analysis where:

• For r > 2, exponential decay beats polynomial growth in vertical ray integrands

Main results

Asymptotic behavior

• tendsto_exp_neg_atTop: exp(-a*t) → 0 as t → ∞ for a > 0
• tendsto_mul_exp_neg_atTop: t * exp(-a*t) → 0 as t → ∞ for a > 0
• tendsto_sq_mul_exp_neg_atTop: t² * exp(-a*t) → 0 as t → ∞ for a > 0

Integrability

• integrableOn_exp_mul_Ici: exp(c*t) is integrable on [1,∞) for c < 0
• integrableOn_mul_exp_neg_Ici: t * exp(-a*t) is integrable on [1,∞) for a > 0
• integrableOn_sq_mul_exp_neg_Ici: t² * exp(-a*t) is integrable on [1,∞) for a > 0

References

These patterns appear in the magic function integrability proofs for sphere packing, specifically for vertical ray integrands in ContourEndpoints.lean.

Integrability Lemmas

theorem integrableOn_exp_mul_Ici (c : ℝ) (hc : c < 0) : MeasureTheory.IntegrableOn (fun (t : ℝ) => Real.exp (c * t)) (Set.Ici 1) MeasureTheory.volume

exp(c*t) is integrable on [1,∞) for c < 0.

theorem tendsto_mul_exp_neg_atTop (a : ℝ) (ha : 0 < a) : Filter.Tendsto (fun (t : ℝ) => t * Real.exp (-a * t)) Filter.atTop (nhds 0)

t * exp(-a*t) → 0 as t → ∞ for a > 0.

theorem tendsto_sq_mul_exp_neg_atTop (a : ℝ) (ha : 0 < a) : Filter.Tendsto (fun (t : ℝ) => t ^ 2 * Real.exp (-a * t)) Filter.atTop (nhds 0)

t² * exp(-a*t) → 0 as t → ∞ for a > 0.

theorem tendsto_exp_neg_atTop (a : ℝ) (ha : 0 < a) : Filter.Tendsto (fun (t : ℝ) => Real.exp (-a * t)) Filter.atTop (nhds 0)

exp(-a*t) → 0 as t → ∞ for a > 0.

theorem integrableOn_mul_exp_neg_Ici (a : ℝ) (ha : 0 < a) : MeasureTheory.IntegrableOn (fun (t : ℝ) => t * Real.exp (-a * t)) (Set.Ici 1) MeasureTheory.volume

t * exp(-a*t) is integrable on [1,∞) for a > 0.

theorem integrableOn_sq_mul_exp_neg_Ici (a : ℝ) (ha : 0 < a) : MeasureTheory.IntegrableOn (fun (t : ℝ) => t ^ 2 * Real.exp (-a * t)) (Set.Ici 1) MeasureTheory.volume

t² * exp(-a*t) is integrable on [1,∞) for a > 0.