LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

A rectangular second difference equals a mixed partial times the side lengths

Statement

Let $R$ be a closed axis-parallel rectangle and suppose that $f_{x}$ and $f_{x y}$ exist on an open neighbourhood of $R$ . If $(x_{0}, y_{0}), (x_{1}, y_{1})$ are opposite corners of a nondegenerate subrectangle of $R$ , then some $ξ$ strictly between $x_{0}, x_{1}$ and some $η$ strictly between $y_{0}, y_{1}$ satisfy

$f (x_{1}, y_{1}) - f (x_{1}, y_{0}) - f (x_{0}, y_{1}) + f (x_{0}, y_{0}) = (x_{1} - x_{0}) (y_{1} - y_{0}) f_{x y} (ξ, η) .$

Facts & Assumptions

Given: The stated open-neighbourhood hypotheses and a nondegenerate subrectangle of $R$ .

[L1]

After ordering its two endpoints, the one-variable mean-value theorem gives $g (v) - g (u) = (v - u) g^{'} (c)$ for a function continuous on the closed interval and differentiable on its interior, with $c$ strictly between the endpoints (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ).

Proof

technique · direct

1.1

Apply [L1] in the $x$ variable to $x \mapsto f (x, y_{1}) - f (x, y_{0})$ . The stated existence of $f_{x}$ on an open neighbourhood gives the required one-variable regularity, and the rectangle difference is $(x_{1} - x_{0}) (f_{x} (ξ, y_{1}) - f_{x} (ξ, y_{0}))$ .

L1givenchoose

2.1

Apply [L1] in the $y$ variable to $y \mapsto f_{x} (ξ, y)$ . Since $f_{x y}$ exists on an open neighbourhood, this one-variable map is continuous on the closed interval and differentiable on its interior. This yields $(y_{1} - y_{0}) f_{x y} (ξ, η)$ and proves the formula.

step 1.1L1givenchoose∎

Depends on

Used by

Peano's mixed-partial theorem from continuity of one mixed partial Theorem

Dependency tree · two levels

11 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

Mixed partial derivatives (Eremenko) (standard reference, not scraped)