An integral formula for the filled exponential quotient #
This file identifies the filled quotient (1 - exp (-a)) / a with the integral of the
exponential along the line segment from 0 to -a. The formula remains valid when a is not
invertible.
Main result #
oneSubExpNegDivSelf_eq_integral_exp:oneSubExpNegDivSelf ℝ a = ∫ t in 0..1, exp (t • -a).
References #
- Lie groups and the Lie algebra correspondence roadmap, Deliverable A, Layer 1, "The conjugation formulas".
theorem
oneSubExpNegDivSelf_eq_integral_exp
{A : Type u_1}
[NormedRing A]
[NormedAlgebra ℝ A]
[CompleteSpace A]
(a : A)
:
The regularized exponential quotient is the integral of the exponential along the line
segment from 0 to -a.