Exponential integral

DefinitionTerms of the series for the entire exponential integral#✓fully proved

For a natural number \(n\) and a complex number \(z\), this is the complex number \(\frac{(-1)^n z^{n+1}}{(n+1) \cdot (n+1)!}\), the term of index \(j = n + 1\) in the series \(\operatorname{Ein}(z) = \sum_{j \ge 1} \frac{(-1)^{j+1} z^j}{j \cdot j!}\).

def einTerm (n : ℕ) (z : ℂ) : ℂ :=
  (-1 : ℂ) ^ n * z ^ (n + 1) /
    (((n + 1 : ℕ) : ℂ) * ((n + 1).factorial : ℂ))

Used by 5

Used byDifferentiability of the entire exponential integral · The entire exponential integral Ein · Derivative of the entire exponential integral · Totalized principal \(E_1\) kernel at zero · Two-term remainder bound for \(E_1\) in the outer sector

DefinitionThe entire exponential integral Ein#✓fully proved

The entire exponential integral is the function \(\operatorname{Ein} : \mathbb{C} \to \mathbb{C}\) defined by \(\operatorname{Ein}(z) = \sum_{j \ge 1} \frac{(-1)^{j+1} z^j}{j \cdot j!}\).

def ein (z : ℂ) : ℂ :=
  ∑' n : ℕ, einTerm n z

Uses 1 · Used by 6

Statement usesTerms of the series for the entire exponential integral

Used byAnalyticity of the entire exponential integral · Differentiability of the entire exponential integral · Derivative of the entire exponential integral · Totalized principal exponential integral · Totalized principal \(E_1\) kernel at zero · Two-term remainder bound for \(E_1\) in the outer sector

TheoremDifferentiability of the entire exponential integral#✓fully proved

The entire exponential integral \(\operatorname{Ein}\) is complex differentiable at every point of \(\mathbb{C}\).

theorem differentiable_ein : Differentiable ℂ ein

Uses 2 · Used by 2

Statement usesThe entire exponential integral Ein

Proof usesTerms of the series for the entire exponential integral

Used byAnalyticity of the entire exponential integral · Two-term remainder bound for \(E_1\) in the outer sector

TheoremAnalyticity of the entire exponential integral#✓fully proved

The entire exponential integral \(\operatorname{Ein}\) is complex analytic at every point of \(\mathbb{C}\).

theorem analyticOnNhd_ein : AnalyticOnNhd ℂ ein univ

Uses 2

Statement usesThe entire exponential integral Ein

Proof usesDifferentiability of the entire exponential integral

TheoremDerivative of the entire exponential integral#✓fully proved

For every complex number \(z\), the entire exponential integral \(\operatorname{Ein}\) satisfies \(z \operatorname{Ein}'(z) = 1 - e^{-z}\).

This is the identity \(\operatorname{Ein}'(z) = (1 - e^{-z})/z\) multiplied through by \(z\), a form that remains valid at \(z = 0\).

theorem mul_deriv_ein (z : ℂ) :
    z * deriv ein z = 1 - Complex.exp (-z)

Uses 2 · Used by 1

Statement usesThe entire exponential integral Ein

Proof usesTerms of the series for the entire exponential integral

Used byTwo-term remainder bound for \(E_1\) in the outer sector

DefinitionTotalized principal exponential integral#✓fully proved

For every complex number \(z\), this is \(\operatorname{Ein}(z) - \operatorname{Log} z - \gamma\), where \(\operatorname{Ein}(z) = \sum_{j \ge 1} (-1)^{j+1} z^j / (j \cdot j!)\) is the entire exponential integral, \(\operatorname{Log}\) is the principal branch of the complex logarithm (imaginary part in \((-\pi, \pi]\)) extended by \(\operatorname{Log} 0 = 0\), and \(\gamma\) is the Euler–Mascheroni constant.

At \(z = 0\) the value is therefore \(-\gamma\). This is a convention, not a value of the classical principal \(E_1\), which has a logarithmic singularity at \(0\).

def principalExponentialIntegralE1Raw (z : ℂ) : ℂ :=
  ein z - Complex.log z - (Real.eulerMascheroniConstant : ℂ)

Uses 1 · Used by 5

Statement usesThe entire exponential integral Ein

Used byTotalized remainder of the \(E_1\) asymptotic expansion · Totalized \(E_1\) remainder at zero · The principal exponential integral · Totalized principal \(E_1\) kernel at zero · Two-term remainder bound for \(E_1\) in the outer sector

DefinitionThe principal exponential integral#✓fully proved

For a nonzero complex number \(z\), the principal exponential integral is \(E_1(z) = \operatorname{Ein}(z) - \operatorname{Log} z - \gamma\), where \(\operatorname{Ein}(z) = \sum_{j \ge 1} (-1)^{j+1} z^j / (j \cdot j!)\) is the entire exponential integral, \(\operatorname{Log}\) is the principal branch of the complex logarithm (imaginary part in \((-\pi, \pi]\)) and \(\gamma\) is the Euler–Mascheroni constant.

This is the connection formula DLMF 6.2.4, taken as the definition. On the branch cut, the negative real axis, the value is the one given by the principal logarithm.

def principalExponentialIntegralE1 (z : ℂ) (_hz : z ≠ 0) : ℂ :=
  principalExponentialIntegralE1Raw z

Uses 1 · Used by 2

Statement usesTotalized principal exponential integral

Used byRemainder of the \(E_1\) asymptotic expansion · Two-term remainder bound for \(E_1\) in the outer sector

DefinitionTotalized asymptotic term of \(E_1\)#✓fully proved

For \(n \in \mathbb{N}\) and every complex number \(z\), the \(n\)-th term of the asymptotic expansion of \(E_1\) is \(\frac{e^{-z}}{z} \cdot \frac{(-1)^n \, n!}{z^n}\), with division by zero read as \(0\).

At \(z = 0\) this gives \(0\), a value with no classical meaning; the domain-safe term requires \(z \neq 0\).

def e1AsymptoticTermRaw (n : ℕ) (z : ℂ) : ℂ :=
  Complex.exp (-z) / z *
    ((-1 : ℂ) ^ n * (n.factorial : ℂ) / z ^ n)

Used by 4

Used byTotalized partial sum of the \(E_1\) asymptotic expansion · Totalized partial sums of the \(E_1\) expansion vanish at zero · Asymptotic term of \(E_1\) · Totalized \(E_1\) asymptotic terms vanish at zero

DefinitionAsymptotic term of \(E_1\)#✓fully proved

For \(n \in \mathbb{N}\) and a nonzero complex number \(z\), the \(n\)-th term of the asymptotic expansion of the exponential integral \(E_1\) is \(\frac{e^{-z}}{z} \cdot \frac{(-1)^n \, n!}{z^n}\).

def e1AsymptoticTerm (n : ℕ) (z : ℂ) (_hz : z ≠ 0) : ℂ :=
  e1AsymptoticTermRaw n z

Uses 1 · Used by 3

Statement usesTotalized asymptotic term of \(E_1\)

Used byPartial sum of the \(E_1\) asymptotic expansion · Outer-sector bound for the quadratic integral remainder · Two-term remainder bound for \(E_1\) in the outer sector

DefinitionTotalized partial sum of the \(E_1\) asymptotic expansion#✓fully proved

For \(n \in \mathbb{N}\) and every complex number \(z\), this is \(\sum_{j < n} t_j(z)\), where \(t_j(z) = \frac{e^{-z}}{z} \cdot \frac{(-1)^j \, j!}{z^j}\) with division by zero read as \(0\).

At \(z = 0\) every term, hence the sum, is \(0\); this value has no classical meaning, and the domain-safe partial sum requires \(z \neq 0\).

def e1AsymptoticPartialRaw (n : ℕ) (z : ℂ) : ℂ :=
  ∑ j ∈ Finset.range n, e1AsymptoticTermRaw j z

Uses 1 · Used by 3

Statement usesTotalized asymptotic term of \(E_1\)

Used byTotalized partial sums of the \(E_1\) expansion vanish at zero · Totalized remainder of the \(E_1\) asymptotic expansion · Totalized \(E_1\) remainder at zero

DefinitionPartial sum of the \(E_1\) asymptotic expansion#✓fully proved

For \(n \in \mathbb{N}\) and a nonzero complex number \(z\), the sum of the first \(n\) terms of the asymptotic expansion of the exponential integral \(E_1\) is \(\sum_{j < n} \frac{e^{-z}}{z} \cdot \frac{(-1)^j \, j!}{z^j}\).

def e1AsymptoticPartial (n : ℕ) (z : ℂ) (hz : z ≠ 0) : ℂ :=
  ∑ j ∈ Finset.range n, e1AsymptoticTerm j z hz

Uses 1 · Used by 2

Statement usesAsymptotic term of \(E_1\)

Used byRemainder of the \(E_1\) asymptotic expansion · Two-term remainder bound for \(E_1\) in the outer sector

DefinitionTotalized remainder of the \(E_1\) asymptotic expansion#✓fully proved

For \(n \in \mathbb{N}\) and every complex number \(z\), this is \(\operatorname{Ein}(z) - \operatorname{Log} z - \gamma - S_n(z)\), where \(\operatorname{Ein}\) is the entire exponential integral, \(\operatorname{Log}\) is the principal logarithm extended by \(\operatorname{Log} 0 = 0\), \(\gamma\) is the Euler–Mascheroni constant and \(S_n\) is the totalized sum of the first \(n\) terms of the asymptotic expansion of \(E_1\).

At \(z = 0\) this equals \(-\gamma\), a value with no classical meaning; the domain-safe remainder requires \(z \neq 0\).

def e1AsymptoticRemainderRaw (n : ℕ) (z : ℂ) : ℂ :=
  principalExponentialIntegralE1Raw z - e1AsymptoticPartialRaw n z

Uses 2 · Used by 1

Statement usesTotalized partial sum of the \(E_1\) asymptotic expansion · Totalized principal exponential integral

Used byTotalized \(E_1\) remainder at zero

DefinitionRemainder of the \(E_1\) asymptotic expansion#✓fully proved

For \(n \in \mathbb{N}\) and a nonzero complex number \(z\), the remainder after \(n\) terms is \(E_1(z) - \sum_{j < n} \frac{e^{-z}}{z} \cdot \frac{(-1)^j \, j!}{z^j}\), where \(E_1\) is the principal exponential integral.

def e1AsymptoticRemainder (n : ℕ) (z : ℂ) (hz : z ≠ 0) : ℂ :=
  principalExponentialIntegralE1 z hz - e1AsymptoticPartial n z hz

Uses 2 · Used by 1

Statement usesPartial sum of the \(E_1\) asymptotic expansion · The principal exponential integral

Used byTwo-term remainder bound for \(E_1\) in the outer sector

TheoremTotalized principal \(E_1\) kernel at zero#✓fully proved

The totalized kernel \(\operatorname{Ein}(z) - \operatorname{Log} z - \gamma\), where \(\operatorname{Ein}\) is the entire exponential integral, \(\operatorname{Log}\) is the principal logarithm extended by \(\operatorname{Log} 0 = 0\) and \(\gamma\) is the Euler–Mascheroni constant, equals \(-\gamma\) at \(z = 0\).

This value comes from \(\operatorname{Ein}(0) = 0\) and the convention \(\operatorname{Log} 0 = 0\), not from analysis; the classical \(E_1\) is singular at \(0\).

theorem principalExponentialIntegralE1Raw_zero :
    principalExponentialIntegralE1Raw 0 = -(Real.eulerMascheroniConstant : ℂ)

Uses 3 · Used by 1

Statement usesTotalized principal exponential integral

Proof usesThe entire exponential integral Ein · Terms of the series for the entire exponential integral

Used byTotalized \(E_1\) remainder at zero

TheoremTotalized \(E_1\) asymptotic terms vanish at zero#✓fully proved

For every \(n \in \mathbb{N}\), the totalized \(n\)-th term \(\frac{e^{-z}}{z} \cdot \frac{(-1)^n \, n!}{z^n}\) of the asymptotic expansion of \(E_1\), with division by zero read as \(0\), equals \(0\) at \(z = 0\).

This value comes from the convention that division by zero gives \(0\), not from analysis.

theorem e1AsymptoticTermRaw_zero (n : ℕ) :
    e1AsymptoticTermRaw n 0 = 0

Uses 1 · Used by 1

Statement usesTotalized asymptotic term of \(E_1\)

Used byTotalized partial sums of the \(E_1\) expansion vanish at zero

TheoremTotalized partial sums of the \(E_1\) expansion vanish at zero#✓fully proved

For every \(n \in \mathbb{N}\), the totalized sum of the first \(n\) terms of the asymptotic expansion of \(E_1\) equals \(0\) at \(z = 0\).

This value comes from the convention that division by zero gives \(0\), not from analysis.

theorem e1AsymptoticPartialRaw_zero (n : ℕ) :
    e1AsymptoticPartialRaw n 0 = 0

Uses 3 · Used by 1

Statement usesTotalized partial sum of the \(E_1\) asymptotic expansion

Proof usesTotalized asymptotic term of \(E_1\) · Totalized \(E_1\) asymptotic terms vanish at zero

Used byTotalized \(E_1\) remainder at zero

TheoremTotalized \(E_1\) remainder at zero#✓fully proved

For every \(n \in \mathbb{N}\), the totalized remainder of the asymptotic expansion of \(E_1\) after \(n\) terms equals \(-\gamma\) at \(z = 0\), where \(\gamma\) is the Euler–Mascheroni constant.

This value comes from the conventions \(\operatorname{Log} 0 = 0\) and division by zero giving \(0\), not from analysis; the classical \(E_1\) is singular at \(0\).

theorem e1AsymptoticRemainderRaw_zero (n : ℕ) :
    e1AsymptoticRemainderRaw n 0 = -(Real.eulerMascheroniConstant : ℂ)

Uses 5

Statement usesTotalized remainder of the \(E_1\) asymptotic expansion

Proof usesTotalized partial sum of the \(E_1\) asymptotic expansion · Totalized partial sums of the \(E_1\) expansion vanish at zero · Totalized principal exponential integral · Totalized principal \(E_1\) kernel at zero

LemmaTwo-term expansion of \(1/(t + z)\)#✓fully proved

Let \(z \ne 0\) be a complex number and \(t\) a real number with \(t + z \ne 0\). Then \(\frac{1}{t + z} = \frac{1}{z} - \frac{t}{z^2} + \frac{t^2}{z^2 (t + z)}\).

lemma two_term_kernel_identity (z : ℂ) (t : ℝ) (hz : z ≠ 0)
    (htz : (t : ℂ) + z ≠ 0) :
    1 / ((t : ℂ) + z) =
      1 / z - (t : ℂ) / z ^ 2 + (t : ℂ) ^ 2 / (z ^ 2 * ((t : ℂ) + z))

Used by 1

Used byTwo-term remainder bound for \(E_1\) in the outer sector

TheoremIntegrability of \(e^{-t} t^n\) on \((0, \infty)\)#✓fully proved

For every natural number \(n\), the function \(t \mapsto e^{-t} t^n\) is Lebesgue integrable on the open interval \((0, \infty)\).

theorem integrableOn_exp_neg_mul_pow (n : ℕ) :
    MeasureTheory.IntegrableOn (fun t : ℝ => Real.exp (-t) * t ^ n) (Set.Ioi 0)

Used by 2

Used byOuter-sector bound for the quadratic integral remainder · Two-term remainder bound for \(E_1\) in the outer sector

TheoremThe moments of \(e^{-t}\) are factorials#✓fully proved

For every natural number \(n\), the integral of \(e^{-t} t^n\) over the open interval \((0, \infty)\) equals \(n!\).

theorem integral_exp_neg_mul_pow_Ioi (n : ℕ) :
    ∫ t : ℝ in Set.Ioi 0, Real.exp (-t) * t ^ n = (n.factorial : ℝ)

Used by 2

Used byOuter-sector bound for the quadratic integral remainder · Two-term remainder bound for \(E_1\) in the outer sector

LemmaPositivity of \(\sin |\arg z|\) in the outer sector#✓fully proved

Let \(z \ne 0\) be a complex number with \(\pi/2 \le |\arg z| < \pi\), where \(\arg z \in (-\pi, \pi]\) is the principal argument. Then \(\sin |\arg z| > 0\).

lemma outer_sector_sin_abs_arg_pos
    (z : ℂ) (_hz : z ≠ 0) (hargLower : Real.pi / 2 ≤ |z.arg|)
    (hargUpper : |z.arg| < Real.pi) :
    0 < Real.sin |z.arg|

Used by 1

Used byOuter-sector bound for the quadratic integral remainder

LemmaLower bound for \(|t + z|\) in the outer sector#✓fully proved

Let \(z \ne 0\) be a complex number with \(\pi/2 \le |\arg z| < \pi\), where \(\arg z \in (-\pi, \pi]\) is the principal argument, and let \(t \ge 0\) be a real number. Then \(|z| \sin |\arg z| \le |t + z|\).

lemma outer_sector_distance
    (z : ℂ) (t : ℝ) (_hz : z ≠ 0) (_ht : 0 ≤ t)
    (_hargLower : Real.pi / 2 ≤ |z.arg|)
    (_hargUpper : |z.arg| < Real.pi) :
    ‖z‖ * Real.sin |z.arg| ≤ ‖(t : ℂ) + z‖

Used by 1

Used byOuter-sector bound for the quadratic integral remainder

TheoremOuter-sector bound for the quadratic integral remainder#✓fully proved

Let \(z \ne 0\) be a complex number with \(\pi/2 \le |\arg z| < \pi\), where \(\arg z \in (-\pi, \pi]\) is the principal argument, and let \(T_2(z) = \frac{e^{-z}}{z} \cdot \frac{(-1)^2 \, 2!}{z^2}\) be the \(n = 2\) term of the asymptotic expansion of \(E_1\). Then

\[\left| \frac{e^{-z}}{z^2} \int_0^\infty \frac{e^{-t} t^2}{t + z} \, dt \right| \le \frac{|T_2(z)|}{\sin |\arg z|},\]

where the integral is taken over the open interval \((0, \infty)\).

theorem integral_remainder_bound
    (z : ℂ) (hz : z ≠ 0) (hargLower : Real.pi / 2 ≤ |z.arg|)
    (hargUpper : |z.arg| < Real.pi) :
    ‖Complex.exp (-z) / z^2 *
        ∫ t : ℝ in Set.Ioi 0,
          (Real.exp (-t) : ℂ) * (t : ℂ)^2 / ((t : ℂ) + z)‖
      ≤ (Real.sin |z.arg|)⁻¹ * ‖e1AsymptoticTerm 2 z hz‖

Uses 5 · Used by 1

Statement usesAsymptotic term of \(E_1\)

Proof usesIntegrability of \(e^{-t} t^n\) on \((0, \infty)\) · The moments of \(e^{-t}\) are factorials · Lower bound for \(|t + z|\) in the outer sector · Positivity of \(\sin |\arg z|\) in the outer sector

Used byTwo-term remainder bound for \(E_1\) in the outer sector

TheoremTwo-term remainder bound for \(E_1\) in the outer sector#✓fully proved

Let \(z \ne 0\) be a complex number with \(\pi/2 \le |\arg z| < \pi\), where \(\arg z \in (-\pi, \pi]\) is the principal argument. Let \(E_1(z)\) be the principal exponential integral, let \(T_n(z) = \frac{e^{-z}}{z} \cdot \frac{(-1)^n n!}{z^n}\) be the \(n\)-th term of its asymptotic expansion, and let \(R_2(z) = E_1(z) - T_0(z) - T_1(z)\) be the remainder after the first two terms. Then \(|R_2(z)| \le \frac{|T_2(z)|}{\sin |\arg z|}\).

theorem principal_exponential_integral_e1_two_term_remainder_dlmf
    (z : ℂ) (hz : z ≠ 0) (hargLower : Real.pi / 2 ≤ |z.arg|)
    (hargUpper : |z.arg| < Real.pi) :
    ‖e1AsymptoticRemainder 2 z hz‖ ≤
      (Real.sin |z.arg|)⁻¹ * ‖e1AsymptoticTerm 2 z hz‖

Sources

• DLMF 6.12.1 and the outer-sector remainder bound of DLMF §6.12(i), with \(n = 2\).

Uses 13

Statement usesRemainder of the \(E_1\) asymptotic expansion · Asymptotic term of \(E_1\)

Proof usesDifferentiability of the entire exponential integral · Partial sum of the \(E_1\) asymptotic expansion · The entire exponential integral Ein · Terms of the series for the entire exponential integral · Integrability of \(e^{-t} t^n\) on \((0, \infty)\) · The moments of \(e^{-t}\) are factorials · Outer-sector bound for the quadratic integral remainder · Derivative of the entire exponential integral · The principal exponential integral · Totalized principal exponential integral · Two-term expansion of \(1/(t + z)\)

24 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.