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.
The sine and cosine power series converge absolutely for every real argument
Statement
For every real , both series converge absolutely. Equivalently, both power series have infinite radius of convergence.
Facts & Assumptions
Given: A real .
The two displayed series are real power series with the absolute terms and ; factorial denominators are positive (A real power series about a centre, its interval of convergence, and its radius in , Integer powers , The factorial and the falling factorial , defined by recursion in , Canonical naturals are positive and strictly increasing).
The ratio test proves absolute convergence when the ratio of successive absolute terms tends to a limit less than one (Ratio test: gives absolute convergence and hence convergence, and gives divergence).
Proof
If , the sine series is identically zero and the cosine series has only its initial term ; both converge absolutely.
If , every absolute term is nonzero. The successive sine-term ratio is , and the successive cosine-term ratio is ; both tend to .
For , the ratio test proves absolute convergence of both series. Together with step 1.1 this covers every real .
Depends on
- A real power series about a centre, its interval of convergence, and its radius in $[0,+\infty]$
- Integer powers $a^m$
- The factorial $n!$ and the falling factorial $n^{\underline{k}}$, defined by recursion in $\mathbb{N}$
- Canonical naturals are positive and strictly increasing
- Ratio test: $\limsup |a_{k+1}/a_k| < 1$ gives absolute convergence and hence convergence, and $\liminf |a_{k+1}/a_k| > 1$ gives divergence
Used by
- Buffered certified rational phase approximation Algorithm
- Hadamard instability despite analytic solvability Counterexample
- Sine and cosine defined by their real power series Definition
- Minimum nonshrinkable loops, radial vertex cones, and the excursion of length π Lemma
- Spherical Bessel and outgoing Hankel recurrences solve the radial Helmholtz equation Lemma
- Correctness and arithmetic resource bound for buffered phase approximation Theorem
- The derivatives of sine and cosine are cosine and minus sine Theorem
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, Chapter 4 (standard reference, not scraped)
- C. Schmeiser, Introduction to Analysis (standard reference, not scraped)