Pipeline-generated

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.

✓ 11 results · all verified · 9 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 2 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Oscillatory integrals and filon levin methods

1 · Prerequisites

2 · Summary

Objective

For $a < b$ , continuous complex amplitude $f$ , real phase $g$ , and nonzero real frequency $ω$ , this page defines $I_{ω} (f, g; [a, b])$ . Its nonstationary branch assumes $∣ g^{'} ∣ \geq c > 0$ . The local operator $T_{g} h = (h / g^{'})^{'}$ gives the complete repeated integration-by-parts endpoint expansion and explicit $O (∣ ω ∣^{- r})$ remainder.

The Filon procedure interpolates $f$ at distinct nodes including both endpoints, then combines the interpolation values with exact or certified phase moments. Exact Fourier moments are computed by a finite recurrence. For a general nonstationary phase, the page returns a moment expansion together with a derivative-based remainder certificate. The proved endpoint-interpolation error is $O (∣ ω ∣^{- 2})$ for fixed data and exact moments; moment approximation adds its own explicit error budget.

The Levin procedure collocates $p^{'} + i ω g^{'} p = f$ . On a nonsingular collocation branch it returns the endpoint difference $p (b) e^{i ω g (b)} - p (a) e^{i ω g (a)}$ , obtained directly by differentiating $p e^{i ω g}$ . Its residual theorem controls the continuous residual integral through nonstationary derivative bounds and includes $∥ A^{- 1} ∥$ (equivalently the collocation condition number) for both coefficient size and solve residual amplification. All statements use exact arithmetic; the required finite-precision-direct-factorizations page supplies separate rounded residual tools.

At one simple interior stationary point, a local Morse coordinate reduces the phase to a signed quadratic. The Fresnel moment gives the leading term, the proof controls the $O (∣ ω ∣^{- 3 / 2})$ remainder, and a separate nonstationary calculation retains the endpoint term. Stationary endpoints and coalescing points are outside this branch and require separate endpoint or Airy-type analysis. The declared composite-quadrature-rules prerequisite is retained as page-level context; no composite-rule theorem is a logical premise of this pair.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Finite-interval oscillatory integral and phase convention

Definition

Let $a < b$ , $ω \in R ∖ {0}$ , $f : [a, b] \to C$ be continuous, and $g : [a, b] \to R$ be continuous. Define $I_{ω} (f, g; [a, b]) : = \int_{a}^{b} f (x) e^{i ω g (x)} d x .$ The complex Riemann integral here means the real Riemann integral of the real part plus $i$ times the real Riemann integral of the imaginary part. Euler's formula $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ and continuity of sine and cosine, which follows from The derivatives of sine and cosine are cosine and minus sine and differentiability implying continuity A function differentiable at $c$ is continuous at $c$ , make $e^{i ω g}$ continuous. The product is continuous, so both component integrals exist by A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion. A function is in $C^{r} [a, b]$ when it and its derivatives through order $r$ are continuous on $[a, b]$ , with one-sided endpoint derivatives. A phase is nonstationary on $[a, b]$ when $g \in C^{1} [a, b]$ and $∣ g^{'} (x) ∣ \geq c$ everywhere for some fixed $c > 0$ . For such a phase and differentiable $h$ , put $T_{g}^{0} h = h$ and $T_{g}^{j + 1} h = (T_{g}^{j} h / g^{'})^{'}$ whenever that derivative exists.

This is an exact-real definition. A later numerical implementation must separately state its moment errors and any floating-point solve error.

Remarks

The page uses real-valued $g$ , complex-valued $f$ , and real nonzero frequency $ω$ . A simple stationary point is treated in a separate local branch; it is not declared nonstationary by deleting the point where $g^{'} = 0$ .

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Lagrange interpolation at distinct real nodes

Statement

Let $n \geq 1$ and let $c_{0}, \dots, c_{n}$ be distinct real numbers. For arbitrary values $y_{0}, \dots, y_{n} \in C$ , define $ℓ_{j} (x) = \prod_{\begin{array}{c} 0 \leq k \leq n \\ k \neq j \end{array}} \frac{x - c_{k}}{c_{j} - c_{k}}, p (x) = \sum_{j = 0}^{n} y_{j} ℓ_{j} (x) .$ Then $p$ is the unique polynomial of degree at most $n$ satisfying $p (c_{j}) = y_{j}$ . In particular, interpolation reproduces every polynomial of degree at most $n$ .

Facts & Assumptions

Given: The stated distinct nodes and complex data.

[F1]

A nonzero real polynomial of degree $n$ has no more than $n$ distinct real roots: a nonzero real polynomial of degree at most $n$ has at most $n$ distinct real roots. Applied to real and imaginary parts, the same root bound holds for complex polynomials.

Proof

1.1givenconstructalgebra

Since $c_{j} - c_{k} \neq 0$ for $j \neq k$ , every denominator in $ℓ_{j}$ is nonzero. At $x = c_{m}$ , the factor for $k = m$ makes $ℓ_{j} (c_{m}) = 0$ when $j \neq m$ , while every factor in $ℓ_{m} (c_{m})$ equals $1$ ; hence $ℓ_{j} (c_{m}) = 1$ exactly when $j = m$ . The displayed $p$ has degree at most $n$ and $p (c_{m}) = y_{m}$ .

2.1givenF1algebra∎

If $q$ is another such polynomial, then $q - p$ has degree at most $n$ and vanishes at the $n + 1$ distinct nodes. Its real and imaginary parts each have those roots, so [F1] forces both parts to be zero polynomials. Thus $q = p$ . If the data are values of a polynomial of degree at most $n$ , uniqueness identifies that polynomial with $p$ .

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

Local quadratic coordinate at a simple stationary point

Statement

Let $g \in C^{7} (J, R)$ on an open interval $J$ , and let $x_{0} \in J$ satisfy $g^{'} (x_{0}) = 0$ and $g^{''} (x_{0}) \neq 0$ . Then some open interval $J_{0} \subset J$ about $x_{0}$ admits a $C^{5}$ increasing diffeomorphism $Φ : J_{0} \to Φ (J_{0})$ such that $g (x) = g (x_{0}) + \frac{σ}{2} Φ (x)^{2}, Φ (x_{0}) = 0, Φ^{'} (x_{0}) = \sqrt{∣ g^{''} (x_{0}) ∣}, σ = sgn (g^{''} (x_{0})) .$

Facts & Assumptions

Given: The stated real $C^{7}$ phase and simple stationary point.

[F1]

The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ : the integral of a continuous derivative on a compact interval equals the endpoint increment.

[F2]

Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ : product and quotient rules hold for differentiable real functions wherever denominators are nonzero.

[F3]

Mean value theorem on a closed real interval: a continuous function differentiable in the open interval has an interior mean-value point.

[F4]

The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ : for differentiable real functions with compatible domains, the derivative of a composition is the product of the outer derivative and inner derivative, provided the evaluation point and its image are limit points of their respective domains. Here the domains are intervals and the outer functions are differentiable on open intervals containing the inner images.

[F5]

Heine-Cantor in $R$ : a continuous real function on a compact subset of $R$ is uniformly continuous: every continuous real function on a compact interval is uniformly continuous; apply componentwise to the derivatives of $g$ on the chosen compact neighborhood.

[F6]

Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ : every nonnegative real number has a unique nonnegative square root, which is positive when the number is positive.

[F7]

Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a, b]$ takes every value between $f (a)$ and $f (b)$ : a continuous real function on a closed interval attains every value between its endpoint values.

Proof

1.1givenF1F2F3F4F5constructalgebra

Put $h = x - x_{0}$ , $G (t) = g (x_{0} + t h)$ , and $J (t) = G^{'} (t)$ . By [F1], [F2], [F4], and $g^{'} (x_{0}) = 0$ , $J (0) = 0$ , $J^{'} (t) = G^{''} (t) = h^{2} g^{''} (x_{0} + t h)$ , and $g (x) - g (x_{0}) = G (1) - G (0) = \int_{0}^{1} J (t) d t$ . Applying [F1] to $J$ and to $t J (t)$ , with $(t J)^{'} = J + t J^{'}$ , gives $\int_{0}^{1} J (t) d t = \int_{0}^{1} (1 - t) J^{'} (t) d t$ . Hence $g (x) - g (x_{0}) = (x - x_{0})^{2} \int_{0}^{1} (1 - t) g^{''} (x_{0} + t (x - x_{0})) d t$ . Set $q (x) = 2 \int_{0}^{1} (1 - t) g^{''} (x_{0} + t (x - x_{0})) d t$ . For $0 \leq j \leq 5$ , repeated differentiation gives $q^{(j)} (x) = 2 \int_{0}^{1} (1 - t) t^{j} g^{(j + 2)} (x_{0} + t (x - x_{0})) d t$ ; each difference quotient converges uniformly in $t$ by [F3] and [F5], since the next derivative through $g^{(7)}$ is uniformly continuous on a compact neighborhood. Thus $q \in C^{5}$ and $q (x_{0}) = g^{''} (x_{0})$ .

2.1givenF2F6step 1.1constructalgebra

Put $σ = sgn (g^{''} (x_{0}))$ . Shrink the neighborhood so $σ q (x) > 0$ , and define $v (x) = \sqrt{σ q (x)} > 0$ by [F6]. For a fixed point $z$ in this neighborhood, $∣ v (x) - v (z) ∣ = ∣ q (x) - q (z) ∣ / (v (x) + v (z)) \leq ∣ q (x) - q (z) ∣ / v (z)$ , so $v$ is continuous at $z$ . For $x \neq z$ , rationalization gives $(v (x) - v (z)) / (x - z) = σ (q (x) - q (z)) / ((x - z) (v (x) + v (z))) \to σ q^{'} (z) / (2 v (z))$ . Thus $v^{'} = σ q^{'} / (2 v)$ exists and is continuous. Since $q^{'} \in C^{4}$ , repeated product and quotient rules [F2] applied to this identity inductively give $v \in C^{5}$ . Define $Φ (x) = (x - x_{0}) v (x)$ . Then $Φ \in C^{5}$ , $g = g (x_{0}) + σ Φ^{2} / 2$ , $Φ (x_{0}) = 0$ , and $Φ^{'} (x_{0}) = \sqrt{∣ g^{''} (x_{0}) ∣} > 0$ .

3.1givenF2F3F4F7step 2.1algebra∎

By continuity of $Φ^{'}$ , shrink to an open interval $J_{0}$ about $x_{0}$ where $Φ^{'} \geq m > 0$ . For $x < y$ in $J_{0}$ , [F3] gives $Φ (y) - Φ (x) = Φ^{'} (ξ) (y - x) \geq m (y - x)$ , so $Φ$ is strictly increasing. Applying [F7] between points on either side of each $x \in J_{0}$ shows that $Φ (J_{0})$ is open. Its inverse $Ψ$ satisfies $∣ Ψ (u) - Ψ (w) ∣ \leq ∣ u - w ∣ / m$ , hence is continuous. At $u = Φ (x)$ , the inverse difference quotient is the reciprocal of the difference quotient of $Φ$ , and therefore $Ψ^{'} (u) = 1 / Φ^{'} (Ψ (u))$ . This is continuous and nonzero; applying [F2] and [F4] repeatedly to this identity gives $Ψ \in C^{5}$ , since $Φ^{'} \in C^{4}$ and never vanishes. Thus $Φ$ is the asserted diffeomorphism.

AlgorithmAlgorithm: Literature-sourcedProof: Not applicableOpen item page →

Exact recurrence for polynomial Fourier moments

Definition

Input real endpoints $a < b$ , a real frequency $ω \neq 0$ , and an integer $m \geq 0$ . Set $μ_{0} = (e^{i ω b} - e^{i ω a}) / (i ω) .$ For $k = 1, \dots, m$ in increasing order, set $μ_{k} = (b^{k} e^{i ω b} - a^{k} e^{i ω a}) / (i ω) - k μ_{k - 1} / (i ω) .$ Return the complex list $(μ_{0}, \dots, μ_{m})$ . The divisions are defined by $ω \neq 0$ . The procedure works in exact real and complex arithmetic; its exact moment identities are stated and proved separately on this page.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

Derivative of a complex oscillatory phase

Statement

If $a < b$ , $g \in C^{1} [a, b]$ is real-valued and $ω \in R$ , then $x \mapsto e^{i ω g (x)}$ is continuously differentiable and $\frac{d}{d x} e^{i ω g (x)} = i ω g^{'} (x) e^{i ω g (x)} .$

Facts & Assumptions

Given: $a < b$ , a real $C^{1}$ function $g$ on $[a, b]$ , and a real number $ω$ .

[F1]

$\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ : for real $y$ , $e^{i y} = \cos y + i \sin y$ .

[F2]

The derivatives of sine and cosine are cosine and minus sine: $(\sin y)^{'} = \cos y$ and $(\cos y)^{'} = - \sin y$ .

[F3]

The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ : if $v : A \to B \subseteq R$ is differentiable at a limit point $x \in A$ of $A$ , and $u : B \to R$ is differentiable at the limit point $v (x)$ of $B$ , then $(u \circ v)^{'} (x) = u^{'} (v (x)) v^{'} (x)$ .

Proof

1.1givenF1construct

Set $θ (x) = ω g (x)$ . By [F1], $e^{i θ (x)} = \cos (θ (x)) + i \sin (θ (x))$ .

2.1givenF2F3step 1.1algebra∎

The scalar difference quotient gives $θ^{'} (x) = ω g^{'} (x)$ . Apply [F3] with $A = [a, b]$ , $B = R$ , $v = θ$ , and $u = \sin$ or $\cos$ : every $x \in [a, b]$ is a limit point of $[a, b]$ since $a < b$ , and $θ (x)$ is a limit point of $R$ , where both outer functions are differentiable by [F2]. Thus [F2] and step 1.1 give the componentwise derivative $- ω g^{'} (x) \sin (θ (x)) + i ω g^{'} (x) \cos (θ (x)) = i ω g^{'} (x) e^{i θ (x)}$ , including the one-sided endpoint derivatives. Continuity follows from continuity of $g^{'}$ , $g$ , and the trigonometric functions.

AlgorithmAlgorithm: Literature-sourcedProof: Not applicableOpen item page →

Levin collocation for a nonstationary oscillatory integral

Definition

Input $a < b$ , $ω \in R ∖ {0}$ , real $g \in C^{1} [a, b]$ with $∣ g^{'} ∣ \geq c > 0$ , complex $f \in C [a, b]$ , an integer $n \geq 2$ , and complex-valued $C^{1}$ functions $ψ_{1}, \dots, ψ_{n} : [a, b] \to C$ linearly independent over $C$ . Also input distinct collocation nodes $a = x_{1} < \dots < x_{n} = b$ . Define $L_{ω} ψ = ψ^{'} + i ω g^{'} ψ$ , form $A_{j k} = L_{ω} ψ_{k} (x_{j})$ and $y_{j} = f (x_{j})$ . If $A$ is singular, return failure status and no quadrature value. Otherwise solve $A c = y$ in exact arithmetic, put $p = \sum_{k = 1}^{n} c_{k} ψ_{k}$ , and return $Q_{L} = p (b) e^{i ω g (b)} - p (a) e^{i ω g (a)}$ with $A, c$ , and $κ_{2} (A) = ∥ A ∥_{2} ∥ A^{- 1} ∥_{2}$ , where vector norms are Euclidean and $∥ A ∥_{2} = \sup_{∥ v ∥_{2} = 1} ∥ A v ∥_{2}$ is the induced matrix norm. This is a finite collocation procedure; residual and conditioning claims for the nonsingular branch are stated separately on this page. Rounded factorization error is outside this exact-arithmetic definition.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Fresnel whole-line moment from the damped complex Gaussian

Statement

For $Re α > 0$ , the absolutely convergent componentwise complex integral $F (α) = \int_{- \infty}^{\infty} e^{- α u^{2}} d u$ equals $\sqrt{π} α^{- 1 / 2}$ , where $α^{- 1 / 2}$ uses the continuous square-root branch with $\arg α \in (- π / 2, π / 2)$ . Consequently, for every $λ > 0$ and $σ \in {- 1, 1}$ , the ordinary two-sided improper Fresnel integral exists and $\int_{- \infty}^{\infty} e^{i σ λ u^{2} / 2} d u = \sqrt{\frac{2 π}{λ}} e^{i σ π / 4} .$

Facts & Assumptions

Given: The stated $α$ , the componentwise finite-interval convention of Finite-interval oscillatory integral and phase convention, and the same componentwise convention for the Jordan-set integrals below.

[F1]

Change of variables for an injective $C^{1}$ map on a compact Jordan set: an injective $C^{1}$ map with invertible derivative on a neighborhood of a compact Jordan set transforms the integral by the absolute Jacobian determinant.

[F2]

The subtraction formulas for sine and cosine: the subtraction identities express sine and cosine of $u - v$ in terms of the sine and cosine of $u$ and $v$ .

[F3]

The zero sets of sine and cosine and the least positive common period 2 pi: $\sin t = 0$ exactly when $t = m π$ for some integer $m$ , and both trigonometric functions have period $2 π$ .

[F4]

Quarter-turn values and shifts by pi/2 and pi: $\sin (t + π / 2) = \cos t$ and $\cos (t + π) = - \cos t$ for every real $t$ .

[F5]

Parity and the Pythagorean identity for sine and cosine: sine is odd, cosine is even, and $\sin^{2} t + \cos^{2} t = 1$ .

[F6]

Pi is the first positive zero of sine: $\sin t > 0$ for $0 < t < π$ and $\sin π = 0$ .

[F7]

[F8]

The graph of a continuous function on a closed nondegenerate rectangle in $R^{m}$ has content zero in $R^{m + 1}$ : the graph of a continuous real function on a closed nondegenerate rectangle has content zero in the next Euclidean dimension.

[F9]

Measure zero and content zero in $R^{m}$ by countable and finite cube covers: content zero means that every positive volume allowance has a finite cube cover whose total volume is at most that allowance; content zero passes to subsets.

[F10]

Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line: a closed bounded subset of Euclidean space is compact.

[F11]

A bounded set in $R^{m}$ is Jordan measurable iff its boundary is null, equivalently of content zero: a bounded set is Jordan measurable exactly when its boundary has content zero.

[F12]

Changing a bounded integrand on a content-zero set does not change its Riemann integral: changing a bounded real integrand on a content-zero subset of a bounded Jordan set preserves integrability and its integral; apply componentwise to complex integrands.

[F13]

The Riemann integral of a bounded function over a bounded Jordan measurable set: integrate over a bounded Jordan set by integrating the zero extension over a bounding rectangle.

[F14]

A continuous real function on a compact Jordan measurable set is Riemann integrable over that set: every continuous real function on a compact Jordan set is Riemann integrable over it.

[F15]

Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in $R^{m}$ : rectangular Riemann integrals are linear, monotone, and satisfy the absolute-value estimate.

[F16]

Riemann--Fubini on product rectangles, with lower and upper section integrals and content-zero exceptional sections: for an integrable real function on a product rectangle with integrable sections, either iterated integral equals the multiple integral.

[F17]

The Gaussian integral $\int_{- \infty}^{\infty} e^{- x^{2}} d x = \sqrt{π}$ : $\int_{- \infty}^{\infty} e^{- x^{2}} d x = \sqrt{π}$ .

[F18]

A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion: a continuous real function on a compact interval is Riemann integrable.

[F19]

$\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential: $e^{z + w} = e^{z} e^{w}$ for complex $z, w$ .

[F20]

$\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ : $e^{x + i y} = e^{x} (\cos y + i \sin y)$ and $∣ e^{x + i y} ∣ = e^{x}$ for real $x, y$ .

[F21]

The derivatives of sine and cosine are cosine and minus sine: $(\sin t)^{'} = \cos t$ and $(\cos t)^{'} = - \sin t$ .

[F22]

The exponential function is smooth and $(\exp)^{'} = \exp$ : $(e^{t})^{'} = e^{t}$ for real $t$ .

[F23]

[F24]

Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ : products of differentiable real functions obey the product rule.

[F25]

A function differentiable at $c$ is continuous at $c$ : a real function differentiable at a point is continuous there.

[F26]

Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ : every nonnegative real has a unique nonnegative square root.

[F27]

Derivative of a complex oscillatory phase: for real differentiable $θ$ , $(e^{i θ})^{'} = i θ^{'} e^{i θ}$ .

[F28]

If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ : the real $C^{1}$ integration-by-parts identity holds on compact intervals; applying it to real and imaginary parts gives its complex version.

[F29]

The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ : if a differentiable real function has integrable derivative on a compact interval, the integral of that derivative is its endpoint increment.

[F30]

$t \mapsto (\cos t, \sin t)$ is a bijection from $[0, 2 π)$ onto the real unit circle: every point on the real unit circle has a unique representation $(\cos t, \sin t)$ with $0 \leq t < 2 π$ .

[F31]

Every nonzero complex number has a unique polar form $r (\cos θ + i \sin θ)$ with $r > 0$ and $- π < θ \leq π$ : every nonzero complex number has a unique polar form $r (\cos θ + i \sin θ)$ with $r > 0$ and $- π < θ \leq π$ .

[F32]

Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function: finite sums and products of continuous real functions are continuous, constant and identity functions are continuous, and a quotient is continuous where its denominator is nonzero.

[F33]

The exponential function is strictly increasing and The power-series, product-limit, IVP, functional-equation, and Picard definitions agree: the real exponential is positive, strictly increasing, and satisfies $e^{0} = 1$ .

[F34]

Axis-parallel rectangles in $R^{m}$ and their volume: a rectangle has volume equal to the product of its side lengths.

[F35]

$C = R [x] / (x^{2} + 1)$ is a field, every element is uniquely $a + b i$ , and every nonzero element has inverse $(a - b i) / (a^{2} + b^{2})$ : complex addition and multiplication have their real-coordinate formulas, and every nonzero complex number has an inverse.

[F36]

The exponential tends to $+ \infty$ at $+ \infty$ and to $0$ at $- \infty$ : $e^{t} \to 0$ as $t \to - \infty$ , and $e^{t} > 0$ for every real $t$ .

[F37]

Improper integrals over unbounded intervals: each one-sided improper Riemann integral is the finite limit of its proper truncations.

[F38]

Improper integrals with several singular ends: a whole-line improper integral is the sum of its two separately convergent one-sided tails; cancellation between divergent tails is not allowed.

[F39]

Absolute and conditional convergence of improper integrals: absolute convergence means that the improper integral of the modulus converges separately on every one-ended piece.

[F40]

For a continuous complex function $z$ on a compact Jordan set $E$ , $∣ \int_{E} z ∣ \leq \int_{E} ∣ z ∣$ . If $Z = \int_{E} z \neq 0$ , the conjugation and modulus laws Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive give $∣ \overline{Z} / ∣ Z ∣ ∣ = 1$ ; set $ζ = \overline{Z} / ∣ Z ∣$ . Componentwise linearity from Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in $R^{m}$ under the stated convention gives $∣ Z ∣ = Re (ζ Z) = \int_{E} Re (ζ z)$ , while $Re (ζ z) \leq ∣ z ∣$ pointwise; apply the same theorem after the zero-extension definition The Riemann integral of a bounded function over a bounded Jordan measurable set. The conjugation and modulus laws also give $∣ z + w ∣ \leq ∣ z ∣ + ∣ w ∣$ for complex scalars. The interval convention is Finite-interval oscillatory integral and phase convention. The case $Z = 0$ is immediate.

[F41]

Cauchy criterion for improper integrals: a real one-sided improper integral converges if and only if its proper tail integrals satisfy the Cauchy condition; apply this separately to real and imaginary parts.

[F42]

Comparison tests for improper integrals: if $∣ f ∣ \leq g$ eventually and the nonnegative improper integral of $g$ converges, then $f$ converges absolutely on that tail.

Proof

1.1givenF1F14F15F16F17F18F19F20F21F22F25F32F35F37F38F39F42construct

Write $u_{0} = Re α > 0$ . For finite $R$ , the substitution $y = \sqrt{u_{0}} x$ in [F1] gives $\int_{- R}^{R} e^{- u_{0} x^{2}} d x = u_{0}^{- 1 / 2} \int_{- \sqrt{u_{0}} R}^{\sqrt{u_{0}} R} e^{- y^{2}} d y$ ; letting $R \to \infty$ and using [F17] shows that the real Gaussian majorant has finite one-sided integrals. Since $∣ e^{- α x^{2}} ∣ = e^{- u_{0} x^{2}}$ by [F20], [F42] gives absolute convergence of each real and imaginary tail; [F37] and [F39] specify these one-sided limits and [F38] defines their two-sided sum $F (α)$ . By [F18], every finite-interval complex integral exists; the cut-additivity clause of [F15], applied componentwise at $0$ , shows $F_{R} (α) = \int_{- R}^{R} e^{- α x^{2}} d x \to F (α)$ . On $S_{R} = [- R, R]^{2}$ , the integrand is continuous by Euler's formula [F20], differentiability and continuity of sine, cosine and the real exponential [F21], [F22], [F25], and polynomial continuity [F32]; also $e^{- α (x^{2} + y^{2})} = e^{- α x^{2}} e^{- α y^{2}}$ by [F19]. Its real and imaginary parts are integrable by [F14]. Expanding the complex product into four real products, applying [F16] to each, using the complex-coordinate formulas [F35], and using linearity [F15] yields $F_{R} (α)^{2} = \int_{S_{R}} e^{- α (x^{2} + y^{2})} d (x, y)$ .

1.2F1F2F3F4F5F6F8F9F10F11F12F13F14F15F16F20F21F24F26F29F30F32F33F34F40algebra

Put $D_{s} = {(x, y) : x^{2} + y^{2} \leq s^{2}}$ and $A_{ε, R} = D_{R} ∖ int D_{ε}$ . On $K_{+} = [ε, R] \times [0, π]$ and $K_{-} = [ε, R] \times [- π, 0]$ , the polar map $P (r, θ) = (r \cos θ, r \sin θ)$ has determinant $r$ by [F21] and [F5]. Each rectangle has an open rectangular neighborhood with positive radial coordinate and angular width strictly below $2 π$ . If two points there have the same image, equal Euclidean norms give equal radii; after division by that radius, their trigonometric pairs agree. [F2] then gives sine of the angle difference zero and cosine equal to one. By [F3], the difference is $m π$ ; repeated use of [F4], with evenness from [F5] when $m < 0$ , gives cosine $(- 1)^{m}$ , so $m$ is even. The neighborhood's angular width below $2 π$ forces the difference to be zero. Thus each map is injective on a neighborhood and its derivative is invertible there because the determinant is positive. By [F30], every point in the upper half-annulus has a canonical polar angle in $[0, 2 π)$ ; if the second coordinate is positive, [F6], [F5], and [F3] rule out an angle in $(π, 2 π)$ , while if it is zero [F3] leaves only $0$ or $π$ . For a lower-half point with negative second coordinate, its canonical angle is in $(π, 2 π)$ by the same sign facts, and subtracting $2 π$ places it in $(- π, 0)$ without changing its trigonometric pair; points with zero second coordinate use angle $0$ or $- π$ . These arguments prove that the images are exactly the upper and lower closed half-annuli. For $s > 0$ , their curved boundary arcs are graphs of $\pm \sqrt{s^{2} - x^{2}}$ ; the radicand is continuous by [F32], and for nonnegative $u, v$ one has $∣ \sqrt{u} - \sqrt{v} ∣^{2} \leq ∣ u - v ∣$ by [F26] and algebra, proving continuity of those graphs. Each radial segment is a constant-function graph after exchanging coordinates if needed. Each graph has content zero by [F8]; their finite unions do as well by combining finite covers from [F9]. Thus the half-annuli are bounded with content-zero boundary and hence Jordan by [F11]; they are compact by [F10]. Now apply [F1] separately to the real and imaginary parts on each. By componentwise Fubini [F16], each transformed integral is $π \int_{ε}^{R} e^{- α r^{2}} r d r$ . Writing $α = A + i B$ and differentiating the Euler representation with [F20]--[F24] gives $(e^{- α r^{2}})^{'} = - 2 α r e^{- α r^{2}}$ ; componentwise [F29] therefore evaluates this radial integral as $(e^{- α ε^{2}} - e^{- α R^{2}}) / (2 α)$ . Their intersection is two radial segments, content-zero by the same graph argument. On a bounding rectangle, the zero extensions of the two half-annulus integrands sum to the annulus integrand off those segments and to twice it on them; [F12] removes this content-zero difference, while linearity [F15] adds the componentwise integrals. Thus $\int_{A_{ε, R}} e^{- α (x^{2} + y^{2})} d (x, y) = π (e^{- α ε^{2}} - e^{- α R^{2}}) / α$ . The same circle-graph argument makes $D_{ε}$ compact Jordan; [F14] integrates the continuous real and imaginary parts there. For $h = e^{- α (x^{2} + y^{2})}$ , [F20] and [F33] give $∣ h ∣ = e^{- u_{0} (x^{2} + y^{2})} \leq 1$ ; the containing square has area $4 ε^{2}$ by [F34], and [F13], [F15], [F40] give $∣ \int_{D_{ε}} h ∣ \leq \int_{D_{ε}} ∣ h ∣ \leq 4 ε^{2}$ . On the containing square, the zero extensions over $D_{ε}$ and $A_{ε, R}$ sum to $h$ off the boundary circle and to $2 h$ on it; [F12] removes this content-zero difference and linearity [F15] gives $\int_{D_{R}} h = \int_{D_{ε}} h + \int_{A_{ε, R}} h$ . Letting $ε ↓ 0$ therefore gives $\int_{D_{R}} h = π (1 - e^{- α R^{2}}) / α$ .

2.1F1F8F9F10F11F12F13F14F15F16F17F19F20F33F37F40step 1.1step 1.2

Set $E_{R} = S_{R} ∖ int D_{R}$ . It is closed and bounded, hence compact by [F10]; its boundary is contained in $\partial S_{R} \cup \partial D_{R}$ . The square boundary is a finite union of line graphs and the circle boundary is the pair of continuous semicircle graphs proved in step 1.2, so [F8] and [F9] make this union content zero and [F11] makes $E_{R}$ Jordan. Both $E_{R}$ and $D_{R}$ are compact Jordan subsets of $S_{R}$ , so their zero extensions are integrable by [F13] and [F14]. On $S_{R}$ these extensions sum to $h$ off $\partial D_{R}$ and to $2 h$ on the content-zero circle; [F12] and linearity [F15] therefore give $\int_{E_{R}} h + \int_{D_{R}} h = \int_{S_{R}} h$ . Every point of $E_{R}$ has $x^{2} + y^{2} \geq R^{2}$ , so $∣ x ∣ \geq R / \sqrt{2}$ or $∣ y ∣ \geq R / \sqrt{2}$ . Put $G = \int_{R} e^{- u_{0} x^{2}} d x < \infty$ and $H (t) = \int_{∣ x ∣ \geq t} e^{- u_{0} x^{2}} d x$ ; $H (t) \to 0$ by [F37] and the convergent nonnegative improper Gaussian integral [F17]. By [F19], the majorant factors as $e^{- u_{0} x^{2}} e^{- u_{0} y^{2}}$ . On finite bounding rectangles, [F13], [F15], and [F16] bound its integral over the vertical and horizontal tail strips by $2 H (R / \sqrt{2}) G$ . For $h (x, y) = e^{- α (x^{2} + y^{2})}$ , [F40] bounds the complex integral's modulus by the integral of $∣ h ∣$ , so it is at most $2 H (R / \sqrt{2}) G$ . The integrand is continuous on the compact Jordan set $E_{R}$ , so its components are integrable by [F14]. Passing to the one-dimensional Gaussian tail limits preserves this bound. It tends to zero, so the square and disc integrals have the same limit. Also $∣ e^{- α R^{2}} ∣ = e^{- u_{0} R^{2}} \to 0$ : [F33] makes this nonnegative function decreasing in $R$ , and a positive limiting lower bound would contradict the finite Gaussian integral [F1], [F17]. Steps 1.1 and 1.2, with $e^{- α R^{2}} \to 0$ , now give $F (α)^{2} = π / α$ .

3.1givenF1F4F5F6F7F17F18F20F21F22F23F24F26F29F31F32F35F37F39F40step 2.1

The function $F$ is continuous on the right half-plane. Fix a compact neighborhood with $Re α, Re β \geq c_{0} > 0$ . On $[- R, R]$ , differentiating $e^{- (β + t (α - β)) x^{2}}$ in $t$ by [F20]--[F24] and applying [F29] gives $∣ e^{- α x^{2}} - e^{- β x^{2}} ∣ \leq R^{2} ∣ α - β ∣$ . By [F40], the finite-interval contribution to $∣ F (α) - F (β) ∣$ is therefore at most $2 R^{3} ∣ α - β ∣$ . Each omitted tail is bounded by $\int_{∣ x ∣ > R} e^{- c_{0} x^{2}} d x$ , which tends to zero as $R \to \infty$ by [F37], [F39], and the scaled Gaussian integral [F1], [F17]; choosing $R$ and then $∣ α - β ∣$ proves continuity. To justify the branch continuously, write $α = x + i y$ , $q = \sqrt{x^{2} + y^{2}}$ , $u = \sqrt{(q + x) / 2} > 0$ , and $v = y / (2 u)$ . For nonnegative $s, t$ , $∣ \sqrt{s} - \sqrt{t} ∣^{2} \leq ∣ s - t ∣$ , so [F26] and [F32] make $q, u, v$ continuous. Also $2 u v = y$ and $u^{2} - v^{2} = ((q + x)^{2} - y^{2}) / (2 (q + x)) = x$ since $q^{2} = x^{2} + y^{2}$ , hence $(u + i v)^{2} = α$ . Let $θ = \arg α \in (- π, π]$ from [F31]. Since $x = ∣ α ∣ \cos θ > 0$ , $\cos θ > 0$ . On $[- π, - π / 2]$ , [F4] writes $\cos θ = \sin (θ + π / 2) \leq 0$ by [F5], [F6]; on $[π / 2, π]$ , put $t = θ - π / 2 \in [0, π / 2]$ and use period $2 π$ , oddness, and [F6] to get $\cos θ = \sin (π + t) = \sin (t - π) = - \sin (π - t) \leq 0$ . Hence $- π / 2 < θ < π / 2$ . Then the specified square root has positive real part because its argument is $θ / 2 \in (- π / 4, π / 4)$ and cosine is positive there by [F4], [F6]. Both it and $u + i v$ square to $α$ ; since complex numbers form a field [F35], any two roots differ only by sign, and their positive real parts force equality. Thus $H (α) = F (α) (u + i v) / \sqrt{π}$ is continuous; steps 2.1 and $(u + i v)^{2} = α$ give $H (α)^{2} = (F (α)^{2} / π) α = 1$ . On any line segment, if the endpoint values of $H$ were $1$ and $- 1$ , [F7] applied to its continuous real part would force that part to vanish somewhere, impossible for a value in ${- 1, 1}$ . Therefore $H$ is constant along every segment. At $α = 1$ , [F17] gives $H (1) = 1$ , so $F (α) = \sqrt{π} α^{- 1 / 2}$ .

4.1givenF1F17F22F23F24F27F28F29F33F36F38F40F41step 3.1algebra∎

Fix $λ > 0$ and $σ = \pm 1$ , and for $ε > 0$ set $α = ε - i σ λ / 2$ . For any $ε \geq 0$ and $T > R > 0$ , [F27] gives the phase derivative and [F28] justifies integration by parts on $[R, T]$ . The amplitude derivative is $(e^{- ε u^{2}} / u)^{'} = - 2 ε e^{- ε u^{2}} - e^{- ε u^{2}} / u^{2}$ by [F22]--[F24]; the boundary terms are at most $2 / (λ R)$ . For $ε > 0$ , using $u \geq R$ and then [F22], [F23], [F29], and [F36] gives $\int_{R}^{\infty} 2 ε e^{- ε u^{2}} d u \leq R^{- 1} \int_{R}^{\infty} 2 ε u e^{- ε u^{2}} d u = e^{- ε R^{2}} / R \leq 1 / R$ ; when $ε = 0$ this derivative term is zero. Also $e^{- ε u^{2}} \leq 1$ by [F33], so $\int_{R}^{\infty} e^{- ε u^{2}} u^{- 2} d u \leq 1 / R$ . Including the factor $1 / λ$ gives $∣ \int_{R}^{T} e^{- ε u^{2}} e^{i σ λ u^{2} / 2} d u ∣ \leq 4 / (λ R)$ , and the negative tail has the same bound by $u \mapsto - u$ . For $ε = 0$ , [F40] makes each real and imaginary tail satisfy the Cauchy condition in [F41]; hence the one-sided limits exist, and [F38] defines the ordinary two-sided improper Fresnel integral. The estimate is uniform for $ε \geq 0$ ; on every finite interval the damped integrand converges uniformly as $ε ↓ 0$ . Given a tolerance, first choose $R$ so both tails are uniformly small and then pass to the limit on $[- R, R]$ ; this proves that the Abel limit equals the ordinary two-sided improper integral. As $ε ↓ 0$ , $∣ α ∣ \to λ / 2$ and $\arg α \to - σ π / 2$ , so step 3.1 gives $\sqrt{π} (λ / 2)^{- 1 / 2} e^{i σ π / 4} = \sqrt{2 π / λ} e^{i σ π / 4}$ .

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

One-dimensional quadratic oscillatory amplitude bound

Statement

Let $R > 0$ , $λ > 0$ , $σ \in {- 1, 1}$ , and $H \in C_{c}^{1} ((- R, R); C)$ . Then $∣ \int_{- R}^{R} H (u) e^{i σ λ u^{2} / 2} d u ∣ \leq \frac{6 ∥ H ∥_{\infty} + R ∥ H^{'} ∥_{\infty}}{\sqrt{λ}} .$

Facts & Assumptions

Given: The stated compactly supported complex amplitude, $R, λ, σ$ , and the componentwise complex integral convention of Finite-interval oscillatory integral and phase convention.

[F1]

Derivative of a complex oscillatory phase: $(e^{i σ λ u^{2} / 2})^{'} = i σ λ u e^{i σ λ u^{2} / 2}$ .

[F2]

If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ : integration by parts on a compact interval holds for real $C^{1}$ functions and hence componentwise for complex functions.

[F3]

Change of variables for an injective $C^{1}$ map on a compact Jordan set: an increasing affine map $t \mapsto R t$ on a compact interval changes a real integral by its positive derivative $R$ ; apply separately to the real and imaginary parts of a complex integrand.

[F4]

For a continuous complex $z$ on a compact interval, the componentwise definition of Finite-interval oscillatory integral and phase convention, the conjugation and modulus laws Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive, and real linearity and monotonicity from Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in $R^{m}$ give $∣ \int z ∣ \leq \int ∣ z ∣$ : if $Z = \int z \neq 0$ , set $ζ = \overline{Z} / ∣ Z ∣$ , so $∣ ζ ∣ = 1$ and $∣ Z ∣ = \int Re (ζ z) \leq \int ∣ z ∣$ . If $Z = 0$ the bound is immediate. The conjugation and modulus laws also give $∣ z + w ∣ \leq ∣ z ∣ + ∣ w ∣$ for complex scalars.

[F5]

The integral over an interval is additive across an interior cut by the coordinate-slice clause of Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in $R^{m}$ ; apply this to the real and imaginary parts of complex integrands.

Proof

1.1givenF3F4F5constructalgebra

Rescale $u = R t$ by [F3], put $Λ = λ R^{2}$ , and define $\tilde{H} (t) = H (R t)$ . If $Λ \leq 4$ , [F4] bounds the integral by $2 R ∥ H ∥_{\infty} \leq 4 ∥ H ∥_{\infty} / \sqrt{λ}$ , so the claim holds. Assume $Λ > 4$ , put $δ = 2 Λ^{- 1 / 2} < 1$ , and split $[- 1, 1]$ into $[- δ, δ]$ , $[δ, 1]$ , and $[- 1, - δ]$ . By [F5], the integral is the sum over these subintervals; the central integral in the rescaled variable is at most $2 δ ∥ H ∥_{\infty} = 4 ∥ H ∥_{\infty} / \sqrt{Λ}$ by [F4].

2.1givenF1F2F4F5step 1.1algebra∎

On $[δ, 1]$ , [F1] and [F2] integrate by parts using $(i σ Λ t)^{- 1}$ and $\tilde{H}$ ; the boundary at $1$ vanishes because $\tilde{H}$ is compactly supported in $(- 1, 1)$ . The remaining boundary is at most $∥ H ∥_{\infty} / (Λ δ)$ . The integral term is at most $\frac{1}{Λ} (R ∥ H^{'} ∥_{\infty} \int_{δ}^{1} t^{- 1} d t + ∥ H ∥_{\infty} \int_{δ}^{1} t^{- 2} d t) \leq \frac{R ∥ H^{'} ∥_{\infty} + ∥ H ∥_{\infty}}{Λ δ}$ , since both integrals are at most $1 / δ$ . [F4] justifies the complex integral norm bounds; the negative interval has the same estimates. With $δ = 2 Λ^{- 1 / 2}$ , each boundary is at most $∥ H ∥_{\infty} / (2 \sqrt{Λ})$ and each integral is at most $(R ∥ H^{'} ∥_{\infty} + ∥ H ∥_{\infty}) / (2 \sqrt{Λ})$ . By [F5], adding the central piece and two tails gives $(6 ∥ H ∥_{\infty} + R ∥ H^{'} ∥_{\infty}) / \sqrt{Λ}$ in the rescaled integral. Multiplication by $R$ and $Λ = λ R^{2}$ give the claimed bound.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Exact polynomial moments for the linear Fourier phase

Statement

For real endpoints $a < b$ , $ω \in R ∖ {0}$ , and an integer $m \geq 0$ , the output of Exact recurrence for polynomial Fourier moments satisfies $μ_{k} = \int_{a}^{b} x^{k} e^{i ω x} d x$ for every $0 \leq k \leq m$ , with $μ_{0} = \frac{e^{i ω b} - e^{i ω a}}{i ω}, μ_{k} = \frac{b^{k} e^{i ω b} - a^{k} e^{i ω a}}{i ω} - \frac{k}{i ω} μ_{k - 1} (k \geq 1) .$ Thus all polynomial moments for the Fourier phase $g (x) = x$ are obtained by a finite exact recurrence.

Facts & Assumptions

Given: Reals $a < b$ , $ω \neq 0$ , and the componentwise complex integral convention of Finite-interval oscillatory integral and phase convention.

[F1]

Exact recurrence for polynomial Fourier moments: $μ_{0} = (e^{i ω b} - e^{i ω a}) / (i ω)$ and $μ_{k} = (b^{k} e^{i ω b} - a^{k} e^{i ω a}) / (i ω) - k μ_{k - 1} / (i ω)$ .

[F2]

Derivative of a complex oscillatory phase: $(e^{i ω x})^{'} = i ω e^{i ω x}$ .

[F3]

If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ : $\int u v^{'} = [u v] - \int u^{'} v$ for real $C^{1}$ functions; the componentwise complex identity follows by applying it to real and imaginary parts.

[F4]

For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term: for $k \geq 1$ , $(x^{k})^{'} = k x^{k - 1}$ .

Proof

1.1givenF1F2F3algebra

The algorithm sets $μ_{0} = (e^{i ω b} - e^{i ω a}) / (i ω)$ . Since $(e^{i ω x} / (i ω))^{'} = e^{i ω x}$ by [F2], [F3] with $u = 1$ identifies this value with $\int_{a}^{b} e^{i ω x} d x$ .

2.1givenF1F2F3F4step 1.1algebra∎

For $k \geq 1$ , apply [F3] to $u = x^{k}$ and $v^{'} = e^{i ω x}$ . Using [F2] and [F4] gives $\int_{a}^{b} x^{k} e^{i ω x} d x = (b^{k} e^{i ω b} - a^{k} e^{i ω a}) / (i ω) - k \int_{a}^{b} x^{k - 1} e^{i ω x} d x / (i ω)$ . Starting from step 1.1, induction identifies each value returned by the algorithm with the corresponding moment.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Repeated integration by parts for a nonstationary oscillatory integral

Statement

Let $a < b$ , $r \geq 1$ , $ω \in R ∖ {0}$ , $g \in C^{r + 1} [a, b]$ be real-valued with $∣ g^{'} ∣ \geq c > 0$ , and $h \in C^{r} [a, b]$ be complex-valued. With $T_{g} h = (h / g^{'})^{'}$ and $T_{g}^{0} h = h$ as in Finite-interval oscillatory integral and phase convention, one has $I_{ω} (h, g; [a, b]) = \sum_{j = 0}^{r - 1} \frac{(- 1)^{j}}{(i ω)^{j + 1}} {[\frac{T_{g}^{j} h (x)}{g^{'} (x)} e^{i ω g (x)}]}_{a}^{b} + \frac{(- 1)^{r}}{(i ω)^{r}} I_{ω} (T_{g}^{r} h, g; [a, b]) .$ Consequently, $∣ I_{ω} (h, g; [a, b]) - \sum_{j = 0}^{r - 1} \frac{(- 1)^{j}}{(i ω)^{j + 1}} {[\frac{T_{g}^{j} h (x)}{g^{'} (x)} e^{i ω g (x)}]}_{a}^{b} ∣ \leq \frac{b - a}{∣ ω ∣^{r}} ∥ T_{g}^{r} h ∥_{\infty} .$ For fixed $h, g, r$ , the remainder is $O (∣ ω ∣^{- r})$ ; the constant is the displayed derivative norm, not a frequency-uniform assertion about varying $h$ or $g$ .

Facts & Assumptions

Given: $a < b$ , the hypotheses in the Statement, and the componentwise complex Riemann integral from Finite-interval oscillatory integral and phase convention.

[F1]

Derivative of a complex oscillatory phase: $(e^{i ω g})^{'} = i ω g^{'} e^{i ω g}$ .

[F2]

If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ : for real $C^{1}$ functions $u, v$ on a closed interval, $\int u v^{'} = [u v] - \int u^{'} v$ . Applying this to real and imaginary components gives the componentwise complex identity.

[F3]

Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ : sums, products, and quotients with nonzero denominator preserve differentiability and obey the stated derivative rules.

[F4]

For continuous complex $z$ on $[a, b]$ , the componentwise definition of Finite-interval oscillatory integral and phase convention and the conjugation and modulus laws Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive give $∣ \int_{a}^{b} z ∣ \leq \int_{a}^{b} ∣ z ∣$ . If $Z = \int z \neq 0$ , set $ζ = \overline{Z} / ∣ Z ∣$ , so $∣ ζ ∣ = 1$ and $∣ Z ∣ = \int Re (ζ z)$ . Since $Re (ζ z) \leq ∣ z ∣$ , monotonicity from Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in $R^{m}$ proves the bound; the zero case is immediate.

Proof

1.1givenF1F2F3algebra

Since $g^{'}$ is continuous and nowhere zero, [F3] makes $h / g^{'}$ differentiable with derivative $T_{g} h$ . Apply [F2] componentwise with $u = h / g^{'}$ and $v = e^{i ω g}$ . By [F1], $v^{'} = i ω g^{'} v$ , so rearranging gives $I_{ω} (h, g) = [(h / g^{'}) v]_{a}^{b} / (i ω) - I_{ω} (T_{g} h, g) / (i ω)$ .

2.1givenF1F4step 1.1algebra∎

Apply step 1.1 successively to $h, T_{g} h, \dots, T_{g}^{r - 1} h$ . At each application the final integral receives one further factor $- 1 / (i ω)$ and the next endpoint term receives the matching alternating sign, yielding the displayed finite sum and remainder. Since $∣ e^{i ω g (x)} ∣ = 1$ , [F4] bounds the remainder modulus by $∣ ω ∣^{- r} \int_{a}^{b} ∣ T_{g}^{r} h (x) ∣ d x \leq (b - a) ∣ ω ∣^{- r} ∥ T_{g}^{r} h ∥_{\infty}$ .

AlgorithmAlgorithm: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Bounded integration-by-parts expansion for an oscillatory moment

Definition

Input $a < b$ , $ω \in R ∖ {0}$ , a real phase $g \in C^{r + 1} [a, b]$ with $∣ g^{'} ∣ \geq c > 0$ , a complex amplitude $p \in C^{r} [a, b]$ , an integer $r \geq 1$ , and a certified real bound $M \geq ∥ T_{g}^{r} p ∥_{\infty}$ . Compute $S_{r} (p) = \sum_{j = 0}^{r - 1} \frac{(- 1)^{j}}{(i ω)^{j + 1}} {[\frac{T_{g}^{j} p (x)}{g^{'} (x)} e^{i ω g (x)}]}_{a}^{b}, ϵ_{r} = \frac{(b - a) M}{∣ ω ∣^{r}} .$ Return $(S_{r} (p), ϵ_{r})$ . The nonstationary recurrence and the need for the certified derivative bound are specified in Repeated integration by parts for a nonstationary oscillatory integral. If exact phase moments are available, they may instead be passed as exact moment data to a Filon rule; this algorithm makes no general closed-form claim for nonlinear phases.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Local stationary expansion for a quadratic phase

Statement

Let $R > 0$ , $λ \geq 1$ , $σ \in {- 1, 1}$ , and $A \in C_{c}^{4} ((- R, R); C)$ . Fix an even $χ \in C_{c}^{\infty} ((- R, R))$ equal to $1$ on a neighborhood of $0$ . With $∥ A ∥_{C^{4}} : = \max_{0 \leq j \leq 4} ∥ A^{(j)} ∥_{\infty}$ , there is a finite constant $C_{R, χ}$ , depending only on $R$ and $χ$ , such that $∣ \int_{- R}^{R} A (u) e^{i σ λ u^{2} / 2} d u - A (0) \sqrt{\frac{2 π}{λ}} e^{i σ π / 4} ∣ \leq C_{R, χ} ∥ A ∥_{C^{4}} λ^{- 3 / 2} .$

Facts & Assumptions

Given: $A, R, λ, σ, χ$ of the Statement.

[F1]

Fresnel whole-line moment from the damped complex Gaussian: $\int_{R} e^{i σ λ u^{2} / 2} d u = \sqrt{2 π / λ} e^{i σ π / 4}$ as an ordinary two-sided improper integral.

[F2]

One-dimensional quadratic oscillatory amplitude bound: for $H \in C_{c}^{1} ((- R, R))$ , $∣ \int H (u) e^{i σ λ u^{2} / 2} d u ∣ \leq (6 ∥ H ∥_{\infty} + R ∥ H^{'} ∥_{\infty}) λ^{- 1 / 2}$ .

[F3]

The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ : continuous derivatives integrate to endpoint increments; applying it twice gives the integral Taylor remainder.

[F4]

If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ : the real compact-interval identity extends componentwise to complex $C^{1}$ functions.

[F5]

Derivative of a complex oscillatory phase: $(e^{i σ λ u^{2} / 2})^{'} = i σ λ u e^{i σ λ u^{2} / 2}$ .

[F6]

Improper integrals over unbounded intervals, Improper integrals with several singular ends, and Absolute and conditional convergence of improper integrals: one-sided limits define improper integrals, whole-line integrals sum separately convergent tails, and absolute convergence is tested on each tail.

[F7]

The improper $p$ -test for rational exponents and Comparison tests for improper integrals: a continuous function bounded in modulus by $C ∣ u ∣^{- 4}$ on each tail has an absolutely convergent improper integral there.

[F8]

[F9]

The mean-value theorem Mean value theorem on a closed real interval and Heine--Cantor Heine-Cantor in $R$ : a continuous real function on a compact subset of $R$ is uniformly continuous: on compact $[- R, R]$ , the continuous derivatives $D^{(3)}$ and $D^{(4)}$ are uniformly continuous; componentwise mean-value estimates justify differentiating $B (u) = \int_{0}^{1} (1 - t) D^{''} (t u) d t$ twice, giving $B^{'} (u) = \int_{0}^{1} (1 - t) t D^{'''} (t u) d t$ and $B^{''} (u) = \int_{0}^{1} (1 - t) t^{2} D^{''''} (t u) d t$ .

[F10]

Reflection $u \mapsto - u$ preserves the compact interval integral by Change of variables for an injective $C^{1}$ map on a compact Jordan set; real interval linearity from Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in $R^{m}$ , applied componentwise, then makes the integral of an odd complex function on $[- R, R]$ zero.

Proof

1.1givenF3F9constructalgebra

Put $D (u) = A (u) - A (0) χ (u) - A^{'} (0) u χ (u)$ . Then $D (0) = D^{'} (0) = 0$ . Near zero, twice applying [F3] gives $D (u) = u^{2} B (u)$ with $B (u) = \int_{0}^{1} (1 - t) D^{''} (t u) d t$ ; differentiating this finite parameter integral twice is justified by [F9] and gives $B \in C^{2}$ . Away from zero set $B = D / u^{2}$ . These definitions agree near zero, $B$ is compactly supported, and $∥ B ∥_{C^{2}} \leq C_{R, χ} ∥ A ∥_{C^{4}}$ . Thus $A = A (0) χ + A^{'} (0) u χ + u^{2} B$ .

2.1givenF1F4F5F6F7F8F10step 1.1algebra

By [F10], the integral of $u χ (u) e^{i σ λ u^{2} / 2}$ is zero: the integrand is odd and vanishes outside $[- R, R]$ . Let $S = 1 - χ$ . Since $S = 0$ near $0$ , apply [F4] and [F5] twice on finite truncations of each half-line. All boundary terms vanish at the inner endpoints because $S = 0$ there, and at infinity because $S / u \to 0$ and $((S / u)^{'} / u) \to 0$ . The final amplitude $K (u) = {(\frac{(S / u)^{'}}{u})}^{'}$ is continuous, vanishes near $0$ , and is $O (∣ u ∣^{- 4})$ on both tails; [F7] makes its phase-weighted improper integral absolutely convergent. Taking one-sided limits in the finite integration-by-parts identities and using [F6] gives $\int_{R} S (u) e^{i σ λ u^{2} / 2} d u = \frac{1}{(i σ λ)^{2}} \int_{R} K (u) e^{i σ λ u^{2} / 2} d u$ . Apply [F8] on finite truncations and pass to the limits from [F7] to bound the latter modulus by $λ^{- 2} \int_{R} ∣ K (u) ∣ d u = C_{χ} λ^{- 2}$ .

3.1givenF1F2F8step 1.1step 2.1algebra∎

Since $χ = 1$ near zero, [F1] and step 2.1 give $A (0) \int χ (u) e^{i σ λ u^{2} / 2} d u = A (0) \sqrt{\frac{2 π}{λ}} e^{i σ π / 4} + O (C_{χ} ∥ A ∥_{C^{4}} λ^{- 2}) .$ For the last term in step 1.1, one integration by parts gives $\int u^{2} B e^{i σ λ u^{2} / 2} = - (i σ λ)^{- 1} \int (B + u B^{'}) e^{i σ λ u^{2} / 2}$ ; the boundary term vanishes by compact support. Apply [F2] to $H = B + u B^{'} \in C_{c}^{1}$ and the bound on $∥ B ∥_{C^{2}}$ to obtain $O (C_{R, χ} ∥ A ∥_{C^{4}} λ^{- 3 / 2})$ . Since $λ^{- 2} \leq λ^{- 3 / 2}$ for $λ \geq 1$ , adding the three contributions and applying the complex scalar triangle inequality in [F8] proves the stated estimate.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Levin endpoint identity and conditioned residual bound

Statement

Let $a < b$ , $s \geq 1$ , $ω \in R ∖ {0}$ , complex-valued $f \in C^{s} [a, b]$ , and real-valued $g \in C^{s + 1} [a, b]$ with $∣ g^{'} ∣ \geq c > 0$ . Use a nonsingular collocation system from Levin collocation for a nonstationary oscillatory integral, with complex-valued basis functions $ψ_{k} : [a, b] \to C$ in $C^{s + 1} [a, b]$ . Write $A_{j k} = L_{ω} ψ_{k} (x_{j})$ , $y_{j} = f (x_{j})$ , $c = A^{- 1} y$ , $p = \sum_{k} c_{k} ψ_{k}$ , $Q = p (b) e^{i ω g (b)} - p (a) e^{i ω g (a)}$ , and $r = f - L_{ω} p$ . Then $I_{ω} (f, g; [a, b]) - Q = I_{ω} (r, g; [a, b]) = \sum_{j = 0}^{s - 1} \frac{(- 1)^{j}}{(i ω)^{j + 1}} {[\frac{T_{g}^{j} r (x)}{g^{'} (x)} e^{i ω g (x)}]}_{a}^{b} + \frac{(- 1)^{s}}{(i ω)^{s}} I_{ω} (T_{g}^{s} r, g; [a, b]) .$ Put $E_{j} = ∣ T_{g}^{j} f (a) / g^{'} (a) ∣ + ∣ T_{g}^{j} f (b) / g^{'} (b) ∣$ , $V_{j} = ∥ v_{j} (a) ∥_{2} + ∥ v_{j} (b) ∥_{2}$ for $v_{j, k} (x) = T_{g}^{j} (L_{ω} ψ_{k}) (x) / g^{'} (x)$ , and $K_{s} = (\sum_{k} ∥ T_{g}^{s} (L_{ω} ψ_{k}) ∥_{\infty}^{2})^{1 / 2}$ . Then $∣ I_{ω} (f, g) - Q ∣ \leq \sum_{j = 0}^{s - 1} \frac{E_{j} + ∥ A^{- 1} ∥_{2} ∥ y ∥_{2} V_{j}}{∣ ω ∣^{j + 1}} + \frac{b - a}{∣ ω ∣^{s}} (∥ T_{g}^{s} f ∥_{\infty} + ∥ A^{- 1} ∥_{2} ∥ y ∥_{2} K_{s}) .$ If an approximate coefficient vector $\hat{c}$ has exact residual $ρ = A \hat{c} - y$ and endpoint vector $d_{k} = ψ_{k} (b) e^{i ω g (b)} - ψ_{k} (a) e^{i ω g (a)}$ , its output satisfies $∣ Q (\hat{c}) - Q ∣ \leq ∥ d ∥_{2} ∥ A^{- 1} ∥_{2} ∥ ρ ∥_{2} = ∥ d ∥_{2} \frac{κ_{2} (A)}{∥ A ∥_{2}} ∥ ρ ∥_{2} .$ If $B_{s}$ denotes the right-hand side of the preceding collocation bound, then $∣ I_{ω} (f, g) - Q (\hat{c}) ∣ \leq B_{s} + ∥ d ∥_{2} ∥ A^{- 1} ∥_{2} ∥ ρ ∥_{2} .$ All vector norms are Euclidean, $∥ A ∥_{2} = \sup_{∥ v ∥_{2} = 1} ∥ A v ∥_{2}$ is the induced matrix norm, and $κ_{2} (A) = ∥ A ∥_{2} ∥ A^{- 1} ∥_{2}$ . Thus a small nodal residual alone does not provide an integral-error bound; the smooth residual terms and inverse solve amplification are also required.

Facts & Assumptions

Given: The stated functions, nonzero frequency, nonstationary phase, nonsingular collocation matrix, and exact arithmetic residual $ρ$ when an approximate coefficient vector is considered.

[F1]

Levin collocation for a nonstationary oscillatory integral: $L_{ω} p = p^{'} + i ω g^{'} p$ , $A_{j k} = L_{ω} ψ_{k} (x_{j})$ , and the endpoint output is $p (b) e^{i ω g (b)} - p (a) e^{i ω g (a)}$ .

[F2]

Derivative of a complex oscillatory phase: $(e^{i ω g})^{'} = i ω g^{'} e^{i ω g}$ .

[F3]

If $u, v$ are differentiable on $[a, b]$ with $u^{'}, v^{'}$ integrable, then $\int_{a}^{b} u v^{'} = u (b) v (b) - u (a) v (a) - \int_{a}^{b} u^{'} v$ : for real $C^{1}$ functions, $\int u v^{'} = [u v] - \int u^{'} v$ ; the complex identity follows componentwise.

[F4]

Repeated integration by parts for a nonstationary oscillatory integral: the $s$ -step expansion and its remainder bound apply to every $C^{s}$ amplitude when $∣ g^{'} ∣ \geq c > 0$ .

[F5]

Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs: for finite real or complex vectors, $∣ ⟨ z, w ⟩ ∣ \leq ∥ z ∥_{2} ∥ w ∥_{2}$ .

[F6]

Real Riemann integrals on an interval are linear by Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in $R^{m}$ with $m = 1$ ; the componentwise complex convention Finite-interval oscillatory integral and phase convention extends this to complex integrands.

[F7]

The complex modulus is subadditive, $∣ z + w ∣ \leq ∣ z ∣ + ∣ w ∣$ (Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive).

[F8]

On $C^{n}$ the Euclidean inner product is $⟨ x, y ⟩ = \sum_{k} x_{k} \overline{y_{k}}$ , linear in the first argument, and $∥ \overline{d} ∥_{2} = ∥ d ∥_{2}$ by Real and complex inner-product spaces and their induced length and Conjugation is an involutive real-field automorphism, $z \overline{z} = ∣ z ∣^{2}$ , and modulus is definite, multiplicative, and subadditive.

Proof

1.1givenF1F2F3F6algebra

For any $p \in C^{1} [a, b]$ , [F2] gives $(p e^{i ω g})^{'} = (L_{ω} p) e^{i ω g}$ . Apply [F3] to the real and imaginary components of $p$ and $e^{i ω g}$ ; the product rule and cancellation of the two $i ω g^{'} p$ terms yield $I_{ω} (L_{ω} p, g) = [p e^{i ω g}]_{a}^{b}$ . With $p$ from [F1] and $r = f - L_{ω} p$ , componentwise linearity [F6] gives $I_{ω} (f, g) - Q = I_{ω} (r, g)$ .

1.2F1givenalgebra

The coefficient equations imply $A (\hat{c} - c) = ρ$ , so $\hat{c} - c = A^{- 1} ρ$ . The endpoint formula is linear in the coefficient vector, hence $Q (\hat{c}) - Q = d^{⊤} A^{- 1} ρ$ .

2.1givenF4step 1.1

The hypotheses on $f, g, ψ_{k}$ make $r \in C^{s} [a, b]$ . Apply [F4] to $r$ to obtain the displayed exact expansion and bound its integral remainder by $(b - a) ∣ ω ∣^{- s} ∥ T_{g}^{s} r ∥_{\infty}$ .

2.2F1F5F8step 1.2algebra

With $x = A^{- 1} ρ$ , [F8] gives $d^{⊤} x = ⟨ x, \overline{d} ⟩$ and $∥ \overline{d} ∥_{2} = ∥ d ∥_{2}$ ; Cauchy--Schwarz [F5] therefore gives $∣ d^{⊤} A^{- 1} ρ ∣ \leq ∥ d ∥_{2} ∥ A^{- 1} ∥_{2} ∥ ρ ∥_{2}$ . The definition $κ_{2} (A) = ∥ A ∥_{2} ∥ A^{- 1} ∥_{2}$ and nonsingularity give the displayed condition-number form.

3.1givenF4F5F7step 2.1algebra

Since $c = A^{- 1} y$ , $∥ c ∥_{2} \leq ∥ A^{- 1} ∥_{2} ∥ y ∥_{2}$ . Linearity of $T_{g}$ gives $T_{g}^{j} r = T_{g}^{j} f - \sum_{k} c_{k} T_{g}^{j} (L_{ω} ψ_{k})$ . At each endpoint, [F5] bounds the corresponding divided sum by $∥ c ∥_{2} ∥ v_{j} (a) ∥_{2}$ or $∥ c ∥_{2} ∥ v_{j} (b) ∥_{2}$ ; [F7] combines it with the amplitude term. On the interval [F5] bounds $∥ \sum_{k} c_{k} T_{g}^{s} (L_{ω} ψ_{k}) ∥_{\infty}$ by $∥ c ∥_{2} K_{s}$ , and [F7] gives $∥ T_{g}^{s} r ∥_{\infty} \leq ∥ T_{g}^{s} f ∥_{\infty} + ∥ c ∥_{2} K_{s}$ . Substitution in the expansion from step 2.1 gives the stated $E_{j}, V_{j}, K_{s}$ bound.

4.1F7step 3.1step 2.2algebra∎

The complex triangle inequality [F7] combines the exact-collocation bound in step 3.1 with step 2.2, giving the stated integral bound for $Q (\hat{c})$ .

Remarks

The residual $ρ$ in the theorem is the exact residual of the stated matrix equation. If matrix products and solves are rounded, this theorem alone does not certify that exact residual or a rounded solve.

AlgorithmAlgorithm: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Filon quadrature from nodal interpolation and phase moments

Definition

Input $a < b$ , $ω \in R ∖ {0}$ , continuous $f : [a, b] \to C$ , continuous real $g : [a, b] \to R$ , an integer $n \geq 1$ , distinct nodes $a = c_{0} < \dots < c_{n} = b$ , and for each Lagrange basis polynomial $ℓ_{j}$ a complex moment estimate ${\hat{μ}}_{j} \in C$ with real error bound $ϵ_{j} \geq 0$ satisfying $∣ {\hat{μ}}_{j} - \int_{a}^{b} ℓ_{j} (x) e^{i ω g (x)} d x ∣ \leq ϵ_{j}$ . Put $f_{j} = f (c_{j})$ . Form $p_{n} = \sum_{j = 0}^{n} f_{j} ℓ_{j}$ using Lagrange interpolation at distinct real nodes, then return $Q_{n} = \sum_{j = 0}^{n} f_{j} {\hat{μ}}_{j}, η_{n} = \sum_{j = 0}^{n} ∣ f_{j} ∣ ϵ_{j} .$ For $g (x) = x$ , expand each real-node Lagrange polynomial as $ℓ_{j} (x) = \sum_{k = 0}^{n} a_{j k} x^{k}$ , run Exact recurrence for polynomial Fourier moments through $k = n$ , and set ${\hat{μ}}_{j} = \sum_{k = 0}^{n} a_{j k} μ_{k}$ and $ϵ_{j} = 0$ . For general nonstationary $g$ , a user may obtain bounded moments by applying Bounded integration-by-parts expansion for an oscillatory moment to each $ℓ_{j}$ with a certified derivative bound. The exact-moment branch for a general phase is conditional on supplied exact moments; no general exact moment solver for arbitrary nonlinear $g$ is asserted here.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Stationary-phase expansion at one simple interior critical point

Statement

Let $a < b$ , $f \in C^{4} [a, b]$ be complex-valued, and $g \in C^{7} [a, b]$ be real-valued. Suppose $g^{'} (x_{0}) = 0$ , $g^{''} (x_{0}) \neq 0$ for one $x_{0} \in (a, b)$ , and $g^{'}$ has no other zero on $[a, b]$ . Choose a coordinate $Φ : J \to (- R, R)$ from Local quadratic coordinate at a simple stationary point, after restricting its domain so $\overline{J} \subset (a, b)$ , and an even $η \in C_{c}^{\infty} ((- R, R))$ equal to $1$ near $0$ . Such a cutoff exists by symmetrizing a bump from A Euclidean bump for a compact set inside an open set. Extend $χ (x) = η (Φ (x))$ by $0$ outside $J$ , put $h = (1 - χ) f$ , $A (u) = η (u) f (Φ^{- 1} (u)) (Φ^{- 1})^{'} (u)$ , and $σ = sgn (ω g^{''} (x_{0}))$ . For $∣ ω ∣ \geq 1$ , $I_{ω} (f, g; [a, b]) = \frac{1}{i ω} {[\frac{f (x) e^{i ω g (x)}}{g^{'} (x)}]}_{a}^{b} + f (x_{0}) e^{i ω g (x_{0})} \sqrt{\frac{2 π}{∣ ω g^{''} (x_{0}) ∣}} e^{i σ π / 4} + R_{ω},$ where $∣ R_{ω} ∣ \leq (C_{R, η} ∥ A ∥_{C^{4}} + ∣ T_{g} h (a) / g^{'} (a) ∣ + ∣ T_{g} h (b) / g^{'} (b) ∣ + (b - a) ∥ T_{g}^{2} h ∥_{\infty}) ∣ ω ∣^{- 3 / 2} .$ On the neighborhood where $h = 0$ , define $T_{g} h$ and $T_{g}^{2} h$ to be $0$ ; elsewhere use the recurrence from Finite-interval oscillatory integral and phase convention. The nonstationary norm is taken over the two closed intervals away from that neighborhood.

Facts & Assumptions

Given: The stated interval, amplitude, phase, stationary point, chart, cutoff, and $∣ ω ∣ \geq 1$ .

[F1]

Local quadratic coordinate at a simple stationary point: $g (x) = g (x_{0}) + sgn (g^{''} (x_{0})) Φ (x)^{2} / 2$ and $Φ^{'} (x_{0}) = \sqrt{∣ g^{''} (x_{0}) ∣}$ .

[F2]

Local stationary expansion for a quadratic phase: for an even cutoff $η$ and compactly supported $C^{4}$ amplitude $A$ , the quadratic-phase integral has leading term $A (0) \sqrt{2 π / ∣ ω ∣} e^{i sgn (ω g^{''} (x_{0})) π / 4}$ and remainder at most $C_{R, η} ∥ A ∥_{C^{4}} ∣ ω ∣^{- 3 / 2}$ .

[F3]

Repeated integration by parts for a nonstationary oscillatory integral: the two-step expansion for $h$ applies on intervals where $∣ g^{'} ∣ \geq c > 0$ .

[F4]

Change of variables for an injective $C^{1}$ map on a compact Jordan set: an injective $C^{1}$ coordinate change transforms a real compact Jordan integral by its absolute derivative; apply separately to the real and imaginary parts of a complex amplitude.

[F5]

A Euclidean bump for a compact set inside an open set: a compact interval inside an open interval admits a smooth cutoff equal to $1$ on the compact interval and supported in the open interval.

[F6]

Real Riemann integrals on an interval are linear and additive across an interior cut by Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in $R^{m}$ with $m = 1$ ; apply componentwise using Finite-interval oscillatory integral and phase convention.

[F7]

Proof

1.1givenF1F5construct

Use [F5] for a compact neighborhood of $0$ inside $(- R, R)$ and symmetrize the resulting bump to obtain the even $η$ in the Statement. By [F1], $χ$ is $1$ near $x_{0}$ , vanishes near $a, b$ , and $A$ is compactly supported and $C^{4}$ ; moreover $A (0) = f (x_{0}) / \sqrt{∣ g^{''} (x_{0}) ∣}$ . Since $g^{'}$ has no other zero, its modulus has a positive minimum on the two closed intervals outside a smaller neighborhood where $χ = 1$ .

2.1givenF1F2F4F6step 1.1algebra

Choose $r < R$ with $supp η \subset (- r, r)$ and put $K = Φ^{- 1} ([- r, r])$ , a compact interval inside $J$ . Since $χ f$ vanishes off $K$ , interval additivity [F6] identifies its integral on $[a, b]$ with its integral on $K$ . Apply [F4] on $K$ separately to the real and imaginary parts. The transformed amplitude is $A (u)$ , supported in $(- r, r)$ , so [F6] also identifies its integral on $[- r, r]$ with that on $[- R, R]$ . The phase exponential factors as $e^{i ω g (x_{0})} e^{i sgn (ω g^{''} (x_{0})) ∣ ω ∣ u^{2} / 2}$ . Then [F2], with $λ = ∣ ω ∣$ and sign $σ$ , gives the stationary term in the Statement and a local remainder at most $C_{R, η} ∥ A ∥_{C^{4}} ∣ ω ∣^{- 3 / 2}$ .

2.2givenF3F6F7step 1.1

The complementary amplitude $h$ vanishes on a neighborhood of $x_{0}$ . Apply [F3] with $r = 2$ on each side of that neighborhood; interval additivity [F6] combines the two formulas, and the internal endpoint terms vanish because $h$ and its derivatives are zero there. Since $χ$ vanishes near $a, b$ , the first endpoint term is exactly $\frac{1}{i ω} [f e^{i ω g} / g^{'}]_{a}^{b}$ . The complex triangle inequality [F7] combines the remaining side estimates into a total modulus at most $(∣ T_{g} h (a) / g^{'} (a) ∣ + ∣ T_{g} h (b) / g^{'} (b) ∣ + (b - a) ∥ T_{g}^{2} h ∥_{\infty}) ∣ ω ∣^{- 2} .$

3.1F6F7step 2.1step 2.2algebra∎

By componentwise linearity [F6], the localized and complementary integrals sum to $I_{ω} (f, g; [a, b])$ . The complex triangle inequality [F7] and $∣ ω ∣^{- 2} \leq ∣ ω ∣^{- 3 / 2}$ for $∣ ω ∣ \geq 1$ combine the two remainder bounds and give the stated $R_{ω}$ bound and endpoint term.

Remarks

This theorem treats one interior simple stationary point and keeps the endpoint contribution explicit. Stationary endpoints and coalescing critical points are excluded; an endpoint or Airy-type uniform treatment requires a separate coordinate and remainder argument. Levin collocation in this pair remains on the nonstationary branch.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Nonstationary error bound for endpoint Filon interpolation

Statement

Let $a < b$ , $ω \in R ∖ {0}$ , $f \in C^{2} [a, b]$ be complex-valued, and $g \in C^{3} [a, b]$ be real-valued with $∣ g^{'} ∣ \geq c > 0$ . Use the endpoint Lagrange rule from Filon quadrature from nodal interpolation and phase moments and put $r = f - p_{n}$ . If $μ_{j} = \int_{a}^{b} ℓ_{j} e^{i ω g}$ and the rule uses ${\hat{μ}}_{j}$ with $∣ {\hat{μ}}_{j} - μ_{j} ∣ \leq ϵ_{j}$ , then $∣ I_{ω} (f, g; [a, b]) - Q_{n} ∣ \leq \frac{∣ T_{g} r (a) / g^{'} (a) ∣ + ∣ T_{g} r (b) / g^{'} (b) ∣ + (b - a) ∥ T_{g}^{2} r ∥_{\infty}}{∣ ω ∣^{2}} + η_{n} .$ With exact moments $η_{n} = 0$ , this is an $O (∣ ω ∣^{- 2})$ endpoint-interpolation error bound. The constant depends on the fixed amplitude, phase, nodes, and derivative norms.

Facts & Assumptions

Given: The hypotheses in the Statement, the integral convention on Finite-interval oscillatory integral and phase convention, and the endpoint nodes $c_{0} = a, c_{n} = b$ .

[F1]

Lagrange interpolation at distinct real nodes: $p_{n} = \sum_{j = 0}^{n} f (c_{j}) ℓ_{j}$ and $p_{n} (c_{j}) = f (c_{j})$ .

[F2]

Filon quadrature from nodal interpolation and phase moments: $Q_{n} = \sum_{j} f (c_{j}) {\hat{μ}}_{j}$ and $η_{n} = \sum_{j} ∣ f (c_{j}) ∣ ϵ_{j}$ .

[F3]

Repeated integration by parts for a nonstationary oscillatory integral: the two-step identity for $I_{ω} (h, g)$ has first boundary term $[(h / g^{'}) e^{i ω g}]_{a}^{b} / (i ω)$ , second term $- [(T_{g} h / g^{'}) e^{i ω g}]_{a}^{b} / (i ω)^{2}$ , and remainder $I_{ω} (T_{g}^{2} h, g) / (i ω)^{2}$ .

[F4]

[F5]

Real Riemann integrals on an interval are linear by Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in $R^{m}$ with $m = 1$ ; the componentwise complex definition Finite-interval oscillatory integral and phase convention extends this to complex integrands.

Proof

1.1givenF1F2F4F5algebra

Let $Q_{n}^{*} = \sum_{j} f (c_{j}) μ_{j}$ . By [F1] and [F5], linearity of the integral gives $Q_{n}^{*} = I_{ω} (p_{n}, g)$ ; by [F2] and the finite-sum triangle inequality [F4], $∣ Q_{n}^{*} - Q_{n} ∣ \leq η_{n}$ . The same linearity gives $I_{ω} (f, g) - Q_{n} = I_{ω} (r, g) + (Q_{n}^{*} - Q_{n})$ .

1.2givenF1F3algebra

The endpoint nodes and [F1] give $r (a) = r (b) = 0$ , so the first boundary term in [F3] vanishes. Applying [F3] to $r$ leaves $I_{ω} (r, g) = - \frac{[(T_{g} r / g^{'}) e^{i ω g}]_{a}^{b}}{(i ω)^{2}} + \frac{I_{ω} (T_{g}^{2} r, g)}{(i ω)^{2}} .$

2.1givenF2F3F4step 1.1step 1.2algebra∎

Since $∣ e^{i ω g} ∣ = 1$ , the complex triangle inequality [F4] bounds the displayed boundary term by $∣ T_{g} r (a) / g^{'} (a) ∣ + ∣ T_{g} r (b) / g^{'} (b) ∣$ , and the integral term is at most $(b - a) ∥ T_{g}^{2} r ∥_{\infty}$ by [F3]. Combine these bounds with step 1.1 and $∣ (i ω)^{2} ∣ = ∣ ω ∣^{2}$ using [F4] to obtain the assertion.

5 · Examples, counterexamples and false statements

None yet.

Oscillatory integrals and filon levin methods

1 · Prerequisites

2 · Summary

Objective

3 · Logical flowchart

4 · Definitions, theorems and proofs

Finite-interval oscillatory integral and phase convention

Definition

Remarks

Lagrange interpolation at distinct real nodes

Statement

Facts & Assumptions

Proof

Local quadratic coordinate at a simple stationary point

Statement

Facts & Assumptions

Proof

Exact recurrence for polynomial Fourier moments

Definition

Derivative of a complex oscillatory phase

Statement

Facts & Assumptions

Proof

Levin collocation for a nonstationary oscillatory integral

Definition

Fresnel whole-line moment from the damped complex Gaussian

Statement

Facts & Assumptions

Proof

One-dimensional quadratic oscillatory amplitude bound

Statement

Facts & Assumptions

Proof

Exact polynomial moments for the linear Fourier phase

Statement

Facts & Assumptions

Proof

Repeated integration by parts for a nonstationary oscillatory integral

Statement

Facts & Assumptions

Proof

Bounded integration-by-parts expansion for an oscillatory moment

Definition

Local stationary expansion for a quadratic phase

Statement

Facts & Assumptions

Proof

Levin endpoint identity and conditioned residual bound

Statement

Facts & Assumptions

Proof

Remarks

Filon quadrature from nodal interpolation and phase moments

Definition

Stationary-phase expansion at one simple interior critical point

Statement

Facts & Assumptions

Proof

Remarks

Nonstationary error bound for endpoint Filon interpolation

Statement

Facts & Assumptions

Proof

5 · Examples, counterexamples and false statements

Sources