LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Integral representations of the first two phi functions

Statement

For every $d \geq 1$ and $X \in M_{d} (C)$ , the series-defined functions The phi-function family by everywhere-convergent series satisfy $φ_{1} (X) = \int_{0}^{1} e^{(1 - θ) X} d θ, φ_{2} (X) = \int_{0}^{1} θ e^{(1 - θ) X} d θ .$ The integrals are componentwise. These formulas define the values at $X = 0$ directly and do not use division by $X$ .

Facts & Assumptions

Given: $d \geq 1$ and $X \in M_{d} (C)$ .

[F1]

The phi-function family by everywhere-convergent series: $φ_{1} (X) = \sum_{j \geq 0} X^{j} / (j + 1)!$ and $φ_{2} (X) = \sum_{j \geq 0} X^{j} / (j + 2)!$ .

[F2]

The scalar and matrix phi series converge absolutely: these series converge absolutely in operator norm.

[F3]

A bounded linear operator between normed spaces, The operator norm as the least bound and as the unit-sphere or unit-ball supremum, Every finite-dimensional normed space is Banach, and The exponential series of a bounded operator: a finite matrix acts as a bounded operator on the complete finite-dimensional space, and its exponential series converges locally uniformly in operator norm.

[F4]

The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, The standard formulas $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ and $\sum_{k < n} x_{k} \overline{y_{k}}$ on $C^{n}$ are inner products, Integrable functions on $[a, b]$ form a set closed under sums and scalar multiples, and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g$ , and For $a \leq b$ and $f : [a, b] \to R^{m}$ integrable when $a < b$ , $∥ \int_{a}^{b} f ∥_{2} \leq \int_{a}^{b} ∥ f ∥_{2}$ ; for $a < b$ , $∥ f ∥_{2}$ is integrable: componentwise complex-vector integrals agree with real integrals in $R^{2 d}$ , finite sums may be integrated termwise, and $∥ \int_{0}^{1} v (θ) d θ ∥_{2} \leq \int_{0}^{1} ∥ v (θ) ∥_{2} d θ$ .

[F5]

The operator norm is zero on the zero domain and otherwise is max_{||v||=1} ||Tv|| and The operator norm is submultiplicative and satisfies ||T^*T|| = ||T||^2: the matrix operator norm is the maximum over unit vectors and $∥ X^{j} v ∥_{2} \leq ∥ X ∥_{2}^{j} ∥ v ∥_{2}$ .

[F6]

$C$ is the real coordinate plane, with coordinate arithmetic, The standard formulas $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ and $\sum_{k < n} x_{k} \overline{y_{k}}$ on $C^{n}$ are inner products, and The norm $∥ v ∥ = \sqrt{⟨ v, v ⟩}$ induced by a real or complex inner product: for $v = (v_{0}, \dots, v_{d - 1})$ , the componentwise map $Φ_{d} (v) : = (Re v_{0}, Im v_{0}, \dots, Re v_{d - 1}, Im v_{d - 1})$ is real-linear and satisfies $∥ Φ_{d} (v) ∥_{R^{2 d}}^{2} = \sum_{j < d} ∣ v_{j} ∣^{2} = ∥ v ∥_{2}^{2}$ . Thus [F4] applies to these complex matrix-valued integrands with the stated Euclidean norm.

Proof

1.1F3F4F5F6algebra

By [F6], the componentwise complex integrals are the real vector integrals to which [F4] applies. For $0 \leq θ \leq 1$ , $v$ a unit vector, and either weight $w (θ) = 1$ or $w (θ) = θ$ , [F5] bounds the exponential-series tail applied to $v$ by $\sum_{j > J} ∥ X ∥_{2}^{j} / j!$ , which tends to zero by [F3]. By [F4], the norm of the integral of the weighted tail applied to $v$ is at most the same tail, uniformly in unit $v$ . Taking the maximum over unit $v$ by [F5] proves that the finite partial-sum integrals converge in operator norm to the corresponding matrix integral. The finite sums may be integrated term by term by componentwise linearity.

1.2algebra

Substituting $u = 1 - θ$ gives $\int_{0}^{1} θ (1 - θ)^{j} d θ = \int_{0}^{1} (1 - u) u^{j} d u = 1 / (j + 1) - 1 / (j + 2) = 1 / ((j + 1) (j + 2))$ .

2.1F1F2step 1.1algebra

For each integer $j \geq 0$ , $\int_{0}^{1} (1 - θ)^{j} d θ = 1 / (j + 1)$ . Therefore the first integral equals $\sum_{j \geq 0} X^{j} / (j! (j + 1)) = \sum_{j \geq 0} X^{j} / (j + 1)! = φ_{1} (X)$ by [F1]; the equality is legitimate because the phi series converges absolutely by [F2].

3.1F1F2step 1.1step 1.2algebra∎

The second integral is consequently $\sum_{j \geq 0} X^{j} / (j! (j + 1) (j + 2)) = \sum_{j \geq 0} X^{j} / (j + 2)! = φ_{2} (X)$ by [F1], with convergence justified by [F2]. At $X = 0$ the same series gives $I_{d}$ and $I_{d} / 2$ , respectively, so no quotient or invertibility assumption is involved.

Depends on

Used by

Dependency tree · two levels

90 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Jitse Niesen and Will M. Wright, A Krylov Subspace Algorithm for Evaluating the Phi-Functions Appearing in Exponential Integrators, arXiv:0907.4631v2 (standard reference, not scraped)
Marlis Hochbruck and Alexander Ostermann, Exponential Integrators, Acta Numerica 19 (2010) (standard reference, not scraped)