LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

A sufficiently high power regularizes finite logarithmic endpoint factors

Statement

Let $r, m$ be nonnegative integers and $γ > r$ . Define $u (t) = t^{γ} (\log t)^{m}$ for $0 < t \leq 1$ and $u (0) = 0$ . Then $u \in C^{r} ([0, 1])$ in the sense of Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ , and $u^{(j)} (0) = 0$ for $0 \leq j \leq r$ .

Facts & Assumptions

Given: Natural numbers $r, m$ , a real exponent $γ > r$ , and the function $u$ above.

[F1]

Real powers for positive bases, with the zero-base positive-exponent convention and The natural logarithm as the inverse of the exponential function: $t^{γ} = \exp (γ \log t)$ for $t > 0$ .

[F2]

Continuity and derivatives of positive-base real powers and The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t: $(t^{γ})^{'} = γ t^{γ - 1}$ and $(\log t)^{'} = 1 / t$ for $t > 0$ .

[F3]

Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ and 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)$ : products and compositions of differentiable functions obey the product and chain rules.

[F4]

The exponential tends to $+ \infty$ at $+ \infty$ and to $0$ at $- \infty$ : $e^{- y} \to 0$ as $y \to + \infty$ .

[F5]

Higher derivatives and the classes $C^{k}$ and $C^{\infty}$ : membership in $C^{r}$ means that derivatives through order $r$ exist and are continuous, with one-sided endpoint derivatives.

[F6]

The exponential dominates every fixed nonnegative integer power at $+ \infty$ : $y^{d} / e^{c y} \to 0$ as $y \to \infty$ for each nonnegative integer $d$ and $c > 0$ .

[F7]

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: $\log$ is strictly increasing; together with [F1], this gives $- \log t \to + \infty$ as $t ↓ 0$ .

Proof

1.1givenF1F2F3induction

For $t > 0$ , induction using [F2]–[F3] gives $u^{(j)} (t) = t^{γ - j} P_{j} (\log t)$ , where $P_{0} (z) = z^{m}$ and $P_{j + 1} (z) = (γ - j) P_{j} (z) + P_{j}^{'} (z)$ . Each $P_{j}$ is a polynomial of degree at most $m$ .

2.1F1F4F6F7step 1.1algebra

If $δ > 0$ and $P$ is a polynomial, put $y = - \log t$ . For every real $M$ , $0 < t < \exp (- M)$ implies $\log t < - M$ by [F1] and [F7], so $y \to + \infty$ as $t ↓ 0$ . Then $t^{δ} ∣ P (\log t) ∣ = e^{- δ y} ∣ P (- y) ∣$ : for some $C > 0$ and integer $d$ , $∣ P (- y) ∣ \leq C (1 + y^{d})$ for $y \geq 1$ , while [F4] and [F6] give $(1 + y^{d}) e^{- δ y} \to 0$ . Since $γ - j > 0$ for every $j \leq r$ , step 1.1 therefore shows $u^{(j)} (t) \to 0$ at zero.

3.1givenF5step 1.1step 2.1algebra∎

Set $u^{(j)} (0) = 0$ for $j \leq r$ . Continuity at zero follows from step 2.1. For $j < r$ , the difference quotient of this extension at zero is $t^{γ - j - 1} P_{j} (\log t)$ , which tends to zero by step 2.1 because $γ - j - 1 > 0$ ; hence the derivative at zero equals the defined $u^{(j + 1)} (0)$ . Thus the derivatives through order $r$ exist and are continuous on $[0, 1]$ by the definition [F5].

Depends on

Used by

Dependency tree · two levels

40 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 I, §5.4.1–5.4.2, The logarithm and the exponential (standard reference, not scraped)