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.
Continuity and derivatives of positive-base real powers
Statement
For , the function is continuous on and For , the function is continuous and differentiable on , with
Facts & Assumptions
Given: A positive base , a real exponent , and .
The chain rule and algebra of derivatives apply to differentiable real functions, and differentiability implies continuity (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 function differentiable at is continuous at ).
Proof
The chain rule applied to gives .
The chain rule applied to gives .
Both functions are continuous on their stated domains because the displayed derivatives exist there.
Depends on
- Real powers for positive bases, with the zero-base positive-exponent convention
- The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t
- 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 function differentiable at $c$ is continuous at $c$
Used by
- Every rational approximation to a real exponent gives the same limiting real power Corollary
- Lᵖ is uniformly convex for 1<p<∞ Corollary
- Cavalieri computes the area of the unit disc from its sections Example
- r² sin(1/r) is differentiable at the origin with a discontinuous gradient Example
- Strong law estimator of an integrable mean Example
- The arc length of one sine period is 4√2 E(1/√2) Example
- The inverse-square field is divergence free, and its flux through the sphere bounding the translated unit ball vanishes Example
- The scaled Gaussian integral and its parameter derivative Example
- The surface generated by rotating y=sin x on [0,π] has area 2π(√2+arsinh1) Example
- Tightness from a uniform moment bound Example
- x⁻ᵃ on (0,1) and on (1,∞) calibrates Lᵖ membership Example
- Absolute real powers are Borel measurable and convex Lemma
- Clarkson inequalities in both exponent ranges Lemma
- The sharp interval bound for Cantor measure Lemma
- A tau-critical graph has no wide pure blockade with cograph pattern Theorem
- An α-narrow graph contains a perfect induced subgraph of order at least |V(G)|^1/α Theorem
- Euler's Beta integral converges exactly for two positive parameters Theorem
- Euler's Gamma integral converges exactly for positive real parameters Theorem
- Finite variance logarithmic rate for iid sums Theorem
- For 0 < p < infinity, the layer-cake formula computes the integral of |f|ᵖ from the distribution function Theorem
- Hadamard three-lines theorem Theorem
- Logarithm formulas for inverse sinh, inverse cosh, and inverse tanh on their natural domains Theorem
- Standard Maclaurin expansions Theorem
- The p-series for a real exponent p converges exactly when p is greater than one Theorem
- The rational-supremum construction of real powers agrees with the exponential construction Theorem
- The real Gamma function is smooth and its derivatives are logarithmic moments Theorem
Dependency tree · two levels
28 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
- J. Lebl, Basic Analysis, Logarithm and Exponential (standard reference, not scraped)
- MIT OpenCourseWare 18.100B Real Analysis, Spring 2025 full lecture notes (standard reference, not scraped)