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 increasing integrand discontinuous at every rational has an integral function nondifferentiable at every rational in
Example
There is a bounded nondecreasing function whose discontinuity set is exactly . On every nondegenerate compact interval , the restriction of is Riemann integrable. Its integral function is differentiable at every irrational point, but at every rational its left and right derivatives exist and are unequal. Thus is nondifferentiable on the dense countable set .
Facts & Assumptions
Given: A nondegenerate interval .
The rationals are countably infinite ( is countably infinite).
For every at-most-countable set there is a bounded nondecreasing function whose discontinuity set is exactly , with unequal finite left and right limits at every point of (Converse to Froda: for every at most countable there is a bounded nondecreasing whose set of discontinuities is exactly , every one of them a jump).
Every monotone function on a compact interval is bounded and Riemann integrable (A monotone function on is Riemann integrable: for the uniform partition into parts the upper minus lower sum telescopes to ).
At a continuity point the integral function has derivative equal to the integrand (The first fundamental theorem: if is integrable on and continuous at , then ; in particular a continuous has as a primitive); at a point with one-sided limits, its one-sided derivatives equal those limits (For an integrable , the one-sided derivatives of equal the corresponding one-sided limits of ; at a jump they are unequal).
The rationals are dense in the reals (Both and are dense in , and every nonempty open subset of is uncountable).
Verification
Apply [L2] to , which is permitted by [L1], and call the resulting function .
Its restriction to is nondecreasing and therefore integrable by [L3].
At every irrational point of , is continuous, so [L4] gives .
At every rational , [L2] gives unequal left and right limits. By [L4] these are the left and right derivatives of , so the two-sided derivative does not exist.
The rational points in are countable by [L1] and dense in every nondegenerate real interval by [L5], so the asserted nondifferentiability set is dense and countable.
Depends on
- $\mathbb{Q}$ is countably infinite
- Both $\mathbb{Q}$ and $\mathbb{R} \setminus \mathbb{Q}$ are dense in $\mathbb{R}$, and every nonempty open subset of $\mathbb{R}$ is uncountable
- Converse to Froda: for every at most countable $E \subseteq \mathbb{R}$ there is a bounded nondecreasing $f : \mathbb{R} \to \mathbb{R}$ whose set of discontinuities is exactly $E$, every one of them a jump
- A monotone function on $[a,b]$ is Riemann integrable: for the uniform partition into $N$ parts the upper minus lower sum telescopes to $|f(b) - f(a)|\,(b-a)/\iota(N)$
- For an integrable $f$, the one-sided derivatives of $F(x)=\int_a^x f$ equal the corresponding one-sided limits of $f$; at a jump they are unequal
- The first fundamental theorem: if $f$ is integrable on $[a,b]$ and continuous at $c$, then $F'(c) = f(c)$; in particular a continuous $f$ has $F$ as a primitive
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: 153 results over 30 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
- J. Lebl, Basic Analysis I & II, Exercise 5.3.12 (standard reference, not scraped)