The difference quotient of a complex exponential at 0, along the positive reals

For c : ℂ, the function t ↦ exp (c t) of a real variable has derivative c at 0. This file records that derivative in the one-sided difference-quotient form

t⁻¹ • (exp (c t) - 1) → c as t → 0⁺,

which is the shape a generator difference quotient takes: the semigroup parameter of a C₀-semigroup runs over the nonnegative reals, so its generator is a limit along 𝓝[>] 0.

Main results

• TauCeti.tendsto_inv_smul_exp_mul_ofReal_sub_one: the one-sided difference quotient of t ↦ exp (c t) at 0 tends to c.

theorem TauCeti.tendsto_inv_smul_exp_mul_ofReal_sub_one (c : ℂ) : Filter.Tendsto (fun (t : ℝ) => t⁻¹ • (Complex.exp (c * ↑t) - 1)) (nhdsWithin 0 (Set.Ioi 0)) (nhds c)

The difference quotient of t ↦ exp (c t) at 0, taken along the positive reals, tends to c: the derivative of a complex exponential at the origin, one-sidedly.