Characteristic function of the gamma distribution

This file computes the characteristic function of a gamma law with positive shape a and positive rate r:

charFun (gammaMeasure a r) t = (1 - I * t / r) ^ (-a).

The power is the principal complex power. Its base stays in the open right half-plane, so there is no branch-cut ambiguity. The proof analytically continues the moment-generating function from the real interval (-∞, r) to the half-plane re z < r, then evaluates the continuation on the imaginary axis.

Main result

• TauCeti.Probability.charFun_gammaMeasure gives the characteristic function of the gamma law.

References

• Roadmap: TauCetiRoadmap/StandardDistributions/README.md, Layer 1, Gamma.
• The continuation step is TauCeti.eqOn_complexMGF_of_eqOn_mgf.
• N. L. Johnson, S. Kotz, N. Balakrishnan, Continuous Univariate Distributions, vol. 1, 2nd ed., Wiley, 1994, ch. 17.

@[simp]

theorem TauCeti.Probability.charFun_gammaMeasure {a r : ℝ} (ha : 0 < a) (hr : 0 < r) (t : ℝ) : MeasureTheory.charFun (ProbabilityTheory.gammaMeasure a r) t = (1 - Complex.I * ↑t / ↑r) ^ (-↑a)

The characteristic function of a gamma law with positive shape a and positive rate r.

The right-hand side uses the principal complex power. Since r > 0, the real part of 1 - I * t / r is 1, so its value never meets the branch cut.