The slope of the real exponential at zero

This file records the parameterized right-sided slope limit for t ↦ exp (a * t). It is a small shared calculus fact used by both semigroup generator shifts and resolvent calculations.

Main result

• TauCeti.tendsto_exp_mul_sub_one_div: (exp (a * t) - 1) / t tends to a as t → 0⁺.

theorem TauCeti.tendsto_exp_mul_sub_one_div (a : ℝ) : Filter.Tendsto (fun (t : ℝ) => (Real.exp (a * t) - 1) / t) (nhdsWithin 0 (Set.Ioi 0)) (nhds a)

The right-sided difference quotient of t ↦ exp (a * t) at zero tends to a.