CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-02

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.

$x^{2} y / (x^{2} + y^{2})$ has every directional derivative at the origin but is not totally differentiable there

Statement refuted

If every directional derivative of a real function exists at a point, then the function is totally differentiable there.

Facts & Assumptions

Given: $f (0, 0) = 0$ and $f (x, y) = x^{2} y / (x^{2} + y^{2})$ away from the origin.

[L1]

The directional derivative is the derivative of $t \mapsto f (a + t v)$ at zero (Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ ).

[L2]

A total derivative computes every directional derivative, so $v \mapsto D_{v} f (a)$ would be the linear map $D f (a)$ applied to $v$ (A total derivative computes every directional derivative, and its matrix is the Jacobian).

Counterexample

technique · direct

1.1

For $v = (a, b) \neq 0$ , $f (t a, t b) = t a^{2} b / (a^{2} + b^{2})$ , so [L1] gives $D_{v} f (0, 0) = a^{2} b / (a^{2} + b^{2})$ ; for $v = 0$ it is $0$ .

L1L2

2.1

This direction map has value $0$ at $(1, 0)$ and $(0, 1)$ but value $1 / 2$ at their sum $(1, 1)$ , so it is not additive.

step 1.1L2algebra

3.1

By [L2], total differentiability would make the directional-derivative map linear, contradicting step 2.1. Thus $f$ is not totally differentiable at the origin.

step 1.1step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

10 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, §8.3.3 (standard reference, not scraped)

x2y/(x2+y2)x2y/(x2+y2) has every directional derivative at the origin but is not totally differentiable there