LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-07-31

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.

At a zero of a real-analytic function, either some first nonzero coefficient makes the zero isolated or every local coefficient vanishes

Statement

Let $f$ be real analytic near $c$ and suppose $f (c) = 0$ . Exactly one of the following local alternatives holds:

every coefficient in a power-series expansion of $f$ about $c$ is zero, so $f$ vanishes on a neighbourhood of $c$ ;
there is a least $m \geq 1$ with $f^{(m)} (c) \neq 0$ , and $c$ is an isolated zero of $f$ .

Facts & Assumptions

Given: A real-analytic $f$ (A real-analytic function on an open subset of $R$ is locally represented by a convergent real power series) with $f (c) = 0$ and a local expansion $f (x) = \sum_{n \geq 0} a_{n} (x - c)^{n}$ .

[L1]

The coefficients are $a_{n} = f^{(n)} (c) / ι (n!)$ (A power-series sum is infinitely differentiable inside its radius and satisfies $a_{n} = f^{(n)} (c) / ι (n!)$ at its centre).

[L2]

Every nonempty subset of $N$ has a least member (The well-ordering principle).

[L3]

Power-series sums are continuous inside their radius. If a function has a nonzero limit at a limit point, it is nonzero on a sufficiently small punctured neighbourhood of that point (The sum of a real power series is continuous at every point strictly inside its interval of convergence, If $\lim_{x \to c} f (x) = L \neq 0$ then $∣ f ∣ > ∣ L ∣ / 2$ on a punctured neighbourhood of $c$ ; in particular if $L > 0$ then $f > L / 2 > 0$ there).

[L4]

A power series converges absolutely at every point strictly inside its radius (A real power series converges absolutely inside its radius and diverges outside it, while either behaviour may occur at an endpoint).

Proof

technique · cases

1.1

If every $a_{n} = 0$ , the local expansion gives $f = 0$ throughout its neighbourhood.

assume-case allzerogiven

1.2

Otherwise, [L2] gives a least $m$ with $a_{m} \neq 0$ . Since $a_{0} = f (c) = 0$ , one has $m \geq 1$ .

assume-case nonzerogivenL2choose

2.1

In the second case, write $f (x) = (x - c)^{m} g (x)$ , where $g (x) : = \sum_{j \geq 0} a_{m + j} (x - c)^{j}$ . At every nonzero point strictly inside the original local radius, the absolute series for $g$ is the corresponding absolute tail for $f$ multiplied by $∣ x - c ∣^{- m}$ ; it also converges at $c$ . Thus $g$ has positive local radius and $g (c) = a_{m} \neq 0$ .

step 1.2L4algebra

3.1

The alternatives in steps 1.1 and 1.2 are exhaustive. In the second, $g$ is continuous at $c$ and therefore has limit $g (c) = a_{m} \neq 0$ there; [L3] makes $g$ nonzero on a smaller punctured neighbourhood, while it is already nonzero at $c$ . Hence $f (x) = 0$ there only when $x = c$ , and the coefficient formula [L1] translates the least nonzero coefficient into the stated least nonzero derivative.

step 1.1step 1.2step 2.1L1L3cases-exhaustive∎

Depends on

Used by

Two real-analytic functions on an open interval that agree on a set with an accumulation point in that interval agree throughout the interval Theorem

Dependency tree · two levels

35 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

Analytic function, Encyclopedia of Mathematics (standard reference, not scraped)
Power series, Encyclopedia of Mathematics (standard reference, not scraped)
Northwestern Math 320-2 lecture notes (standard reference, not scraped)