Alphabeta MathHow 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.
A nonzero smooth compactly supported bump
Example
Let be The one-sided flat function is with identically zero Taylor series and define . Then is smooth, positive on , and zero outside ; its support is .
Facts & Assumptions
Given: The displayed composite.
is smooth and flat at (The one-sided flat function is with identically zero Taylor series).
Products and composites preserve smoothness (The chain rule, in one line from Carathéodory: if is differentiable at and is differentiable at , then is differentiable at with , Sums, scalar multiples, products and quotients: , , , and when , A power-series sum is infinitely differentiable inside its radius and satisfies at its centre).
Closure, boundary, and interior are Interior, closure, boundary, limit point, isolated point and dense subset of a metric space.
Verification
On , , so ; on , , so .
Away from , smoothness follows from [L2]. At , every one-sided derivative from inside is a finite sum of derivatives of at , all zero by [L1], matching the zero function outside.
Thus is smooth and its nonzero set is , whose closure is ; this is its support.
Depends on
- The one-sided flat function is $C^\infty$ with identically zero Taylor series
- The exponential function is smooth and $(\exp)'=\exp$
- 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)$
- Sums, scalar multiples, products and quotients: $(f+g)'(c) = f'(c) + g'(c)$, $(\alpha f)'(c) = \alpha f'(c)$, $(fg)'(c) = f'(c)g(c) + f(c)g'(c)$, and $(f/g)'(c) = \bigl(f'(c)g(c) - f(c)g'(c)\bigr)/g(c)^{2}$ when $g(c) \ne 0$
- A power-series sum is infinitely differentiable inside its radius and satisfies $a_n=f^{(n)}(c)/\iota(n!)$ at its centre
- Interior, closure, boundary, limit point, isolated point and dense subset of a metric space
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 97 results over 22 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- MIT OpenCourseWare 18.100B Real Analysis, Spring 2025 full lecture notes (standard reference, not scraped)
- J. Lebl, Basic Analysis, Analytic Functions (standard reference, not scraped)
- S. Dyatlov, MIT 18.155 lecture notes (standard reference, not scraped)
- MIT 18.102, Chapter 4 notes (standard reference, not scraped)