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.
One-dimensional quadratic oscillatory amplitude bound
Statement
Let , , , and . Then
Facts & Assumptions
Given: The stated compactly supported complex amplitude, , and the componentwise complex integral convention of Finite-interval oscillatory integral and phase convention.
If are differentiable on with integrable, then : integration by parts on a compact interval holds for real functions and hence componentwise for complex functions.
Change of variables for an injective map on a compact Jordan set: an increasing affine map on a compact interval changes a real integral by its positive derivative ; apply separately to the real and imaginary parts of a complex integrand.
For a continuous complex 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, , 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 give : if , set , so and . If the bound is immediate. The conjugation and modulus laws also give for complex scalars.
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 ; apply this to the real and imaginary parts of complex integrands.
Proof
Rescale by [F3], put , and define . If , [F4] bounds the integral by , so the claim holds. Assume , put , and split into , , and . By [F5], the integral is the sum over these subintervals; the central integral in the rescaled variable is at most by [F4].
On , [F1] and [F2] integrate by parts using and ; the boundary at vanishes because is compactly supported in . The remaining boundary is at most . The integral term is at most , since both integrals are at most . [F4] justifies the complex integral norm bounds; the negative interval has the same estimates. With , each boundary is at most and each integral is at most . By [F5], adding the central piece and two tails gives in the rescaled integral. Multiplication by and give the claimed bound.
Depends on
- Finite-interval oscillatory integral and phase convention
- Derivative of a complex oscillatory phase
- 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$
- Change of variables for an injective $C^1$ map on a compact Jordan set
- Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in $\mathbb{R}^m$
- Conjugation is an involutive real-field automorphism, $z\overline z=|z|^2$, and modulus is definite, multiplicative, and subadditive
Used by
Dependency tree · two levels
49 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
- NIST Digital Library of Mathematical Functions, §2.3(iv) (standard reference, not scraped)
- A. Iserles, S. P. Nørsett, and S. Olver, Highly oscillatory quadrature: The story so far, §4 (standard reference, not scraped)