partialGamma when arguments are real

Stream: Is there code for X?

[Josha Dekker]

We have

def partialGamma (s : ℂ) (X : ℝ) : ℂ :=
  ∫ x in (0)..X, (-x).exp * x ^ (s - 1)

I'm interested in the case where $s \in \mathbb{R},~s \geq 0$, in which case partialGamma maps into $\mathbb{R}$. Is there something like a Real.partialGamma that takes care of this? I couldn't find it in the docs.
I'm effectively interested in showing that the CDF of a Gamma distribution equals a constant multiplied by a partialGamma evaluated at some choice of s and X. I'm just curious whether there is something useful out there, or whether I should just program this by hand?

[Kevin Buzzard]

You can just take the real part

[Josha Dekker]

Thank you!

[Kevin Buzzard]

This is a standard trick, see e.g. docs#Real.cos

[Josha Dekker]

Thank you!