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 bounded-variation function has at most countably many discontinuities, all of the first kind
Statement
If has bounded variation, every well-posed one-sided limit of exists. Consequently every discontinuity is of the first kind, and the set of discontinuities is at most countable.
Facts & Assumptions
Given: A bounded-variation function .
Jordan decomposition writes with nondecreasing (Jordan decomposition for functions of bounded variation).
Every well-posed one-sided limit of a monotone function exists, so all its discontinuities are of the first kind (A monotone function on an interval has no discontinuity of the second kind: at every point both relevant one-sided limits exist, and an interior point is a discontinuity exactly when , The left and right limits of at , as limits of the restrictions of to and ).
The discontinuity set of a monotone function on an interval is at most countable (Froda's theorem: the set of discontinuities of a monotone function on an interval is at most countable, the injection into being built from one fixed enumeration of the rationals by least index, so no choice principle is used).
Finite sums and differences preserve existing finite function limits (Sums, scalar multiples, products and quotients of function limits, the quotient under the hypothesis that the denominator limit is nonzero).
Proof
Apply [L2] to and . At every endpoint or interior point where a one-sided limit is defined, both component limits exist, and [L4] gives the corresponding one-sided limit of . Thus has no discontinuity of the second kind.
If both and are continuous at a point, [L4] makes continuous there. Hence the discontinuity set of is contained in the union of the two component discontinuity sets.
Each component discontinuity set is at most countable by [L3]. Given injections of them into , map the first set to the even naturals and the points belonging only to the second to the odd naturals; this injects their union into . Step 1.2 therefore makes the discontinuity set of at most countable, and step 1.1 makes every one of its discontinuities first-kind.
Depends on
- Jordan decomposition for functions of bounded variation
- A monotone function on an interval has no discontinuity of the second kind: at every point both relevant one-sided limits exist, and an interior point $c$ is a discontinuity exactly when $\lim_{x \to c^{-}} f(x) < \lim_{x \to c^{+}} f(x)$
- Froda's theorem: the set of discontinuities of a monotone function on an interval is at most countable, the injection into $\mathbb{N}$ being built from one fixed enumeration of the rationals by least index, so no choice principle is used
- The left and right limits of $f$ at $c$, as limits of the restrictions of $f$ to $A \cap (-\infty, c)$ and $A \cap (c, \infty)$
- Sums, scalar multiples, products and quotients of function limits, the quotient under the hypothesis that the denominator limit is nonzero
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 98 results over 19 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
- Christopher Heil, Absolute Continuity and the Banach-Zaretsky Theorem (standard reference, not scraped)
- William F. Trench, Introduction to Real Analysis, Ch. 3 (standard reference, not scraped)