Partial derivative: deriving the partial-derivative formulas of a quadratic from the difference-quotient limit, and computing a gradient

Goal and scope

For a quadratic f with coefficients in the order [1,x,y,x²,xy,y²], prove from the difference-quotient limit that ∂f/∂x=c_1+2c_3x+c_4y and ∂f/∂y=c_2+c_4x+2c_5y. Then for c=(1,−2,3,1,2,−1) compute the partials and the gradient (4,1) at (1,2), and show that a single nonzero-h quotient (5 or 41/10) and moving both coordinates at once (limit 5) are not the x-partial.

Treats only the bivariate quadratic slice of G1 (MKO assumption a1), deriving the partials exactly from difference-quotient limits. The existence of partials is not used to infer continuity or total differentiability of general functions (a2); the non-polynomial examples in the error controls are only contrasts. The canonical MKO and its English edition are not changed.

Givens and symbols

• func_limit_def
• abs_rules
• order_basics
• distributive
• power_laws

• G1 — f(x,y)=c_0+c_1x+c_2y+c_3x²+c_4xy+c_5y² with integer coefficients in the fixed order [1,x,y,x²,xy,y²]; f is defined on all of ℝ² (MKO assumptions a1, a2).
• G2 — Instance: c=(1,−2,3,1,2,−1), that is f(x,y)=1−2x+3y+x²+2xy−y², at the point (1,2).

• c=(c_0,c_1,c_2,c_3,c_4,c_5) — coefficients in the order [1,x,y,x²,xy,y²]
• f(x,y) — the quadratic polynomial
• h — a nonzero increment
• q_x(h) — the x difference quotient (f(x+h,y)−f(x,y))/h
• f_x,\ f_y — the x- and y-partial derivatives
• \nabla f=(f_x,f_y) — the gradient: the ordered collection of partials

Rules and sources

• func_limit_def · prerequisite — Limit of a function: lim_{x→a} f(x)=L means that for every ε>0 there is δ>0 such that |f(x)−L|<ε for every domain point x with 0<|x−a|<δ (a must be a limit point of the domain).
• abs_rules · prerequisite — Absolute value (reals): |u|=u if u≥0 and |u|=−u if u<0; |u|≥0; |uv|=|u||v|; triangle inequality |u+v|≤|u|+|v|; |u|<r ⇔ −r<u<r.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• distributive · prerequisite — Distributivity: u(v+w)=uv+uw; with commutativity also (v+w)u=vu+wu.
• power_laws · prerequisite — Integer exponent laws (base nonzero, or exponents positive integers): a^m·a^n=a^{m+n}, (a^m)^n=a^{mn}, (ab)^n=a^n b^n, a^0=1.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• add_inverse · prerequisite — Additive inverse: every u has −u with u+(−u)=0; u−v means u+(−v).
• mul_comm · prerequisite — Commutativity of multiplication: uv=vu (in commutative number systems such as ℤ, ℚ, ℝ, ℂ).
• add_comm · prerequisite — Commutativity of addition: u+v=v+u.
• mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined.
• frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
• exists_intro · prerequisite — ∃-introduction: if some a∈D satisfies P(a), then ∃x∈D, P(x).
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• eq_replace · prerequisite — Replacement of equals: an expression inside a statement may be replaced by an equal expression without changing whether the statement is true.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_partial_def · cited — The x-partial derivative of a bivariate function f at (x,y) fixes y and is defined by the difference-quotient limit as nonzero h tends to 0; the y-partial is analogous. This slice differentiates quadratic polynomials symbolically and exactly, rather than replacing the limit with a single finite difference. · mko-partial-derivative
• mko_mvf_def · cited — Explicit slices of bivariate real polynomials f:ℝ²→ℝ, with coefficients ordered as [1,x,y,x²,x*y,y²]. · mko-multivariable-real-function
• L_numerator_x · lemma — For all reals x, y, h: f(x+h,y)−f(x,y)=h(c_1+2c_3x+c_4y)+c_3h².
• L_affine_limit · lemma — For real constants A, B, the function h↦A+Bh on h≠0 satisfies lim_{h→0}(A+Bh)=A.

Main derivation

f_x(x,y)

\lim_{h\to0,\ h\neq0}\frac{f(x+h,y)-f(x,y)}{h}

c=(c_0,c_1,c_2,c_3,c_4,c_5)

f(x,y)=c_0+c_1x+c_2y+c_3x^2+c_4xy+c_5y^2

f(x+h,y)-f(x,y)

h(c_1+2c_3x+c_4y)+c_3h^2

\frac{h(c_1+2c_3x+c_4y)+c_3h^2}{h}

q_x(h)=(c_1+2c_3x+c_4y)+c_3h\quad(h\neq0)

\lim_{h\to0}\big(A+Bh\big)

A

f_x(x,y)=\lim_{h\to0}q_x(h)

f_x(x,y)=c_1+2c_3x+c_4y

\frac{f(x,y+h)-f(x,y)}{h}=(c_2+c_4x+2c_5y)+c_5h

f_y(x,y)=c_2+c_4x+2c_5y

c=(1,-2,3,1,2,-1)

f_x=-2+2x+2y,\quad f_y=3+2x-2y

(x,y)=(1,2)

f_x(1,2)=4,\ \ f_y(1,2)=1,\ \ \nabla f(1,2)=(4,1)

\frac{f(1+h,2)-f(1,2)}{h}

\frac{4h+h^2}{h}=4+h\ \xrightarrow{h\to0}\ 4

q_x(h)=4+h

q_x(1)=5,\ \ q_x(\tfrac1{10})=\tfrac{41}{10},\ \ q_x(h)\neq4\ \text{for every}\ h\neq0

\frac{f(1+h,2+h)-f(1,2)}{h}

\frac{5h+2h^2}{h}=5+2h\ \xrightarrow{h\to0}\ 5\neq4=f_x(1,2)

\text{S06 to S12}

f_x=c_1+2c_3x+c_4y,\ f_y=c_2+c_4x+2c_5y;\ \nabla f(1,2)=(4,1)

Substeps and lemmas

c_0,\ c_1x,\ c_2y,\ c_3x^2,\ c_4xy,\ c_5y^2\ \text{at}\ (x+h,y)\ \text{minus at}\ (x,y)

0,\ c_1h,\ 0,\ c_3(2xh+h^2),\ c_4hy,\ 0

c_1h+c_3(2xh+h^2)+c_4hy

h(c_1+2c_3x+c_4y)+c_3h^2

\varepsilon>0

\delta=\frac{\varepsilon}{|B|+1}>0

0<|h|<\delta

|(A+Bh)-A|=|B||h|\le|B|\delta=\frac{|B|}{|B|+1}\varepsilon<\varepsilon

Reverse audits

• S13 · premise_audit · S06, S07, S09 — Only conjoins conclusions already proved; total differentiability or continuity of f is not claimed (true for polynomials, but not proved here).
• S12 · premise_audit · L_affine_limit, numeric_evaluation — Only shows that this limit is not f_x; 'directional derivative equals f_x+f_y' is merely a numerical observation for this example, and no general formula is proved here.
• S11 · premise_audit · S10, order_basics — 4+h=4 ⇔ h=0, and h=0 is excluded; this conclusion concerns this instance only.
• S10 · premise_audit · L_affine_limit, numeric_evaluation — Cross-checks the formula of S06; for this instance only.
• S09 · inverse_equivalence · numeric_evaluation — Exact integer evaluation.
• S08 · inverse_equivalence · eq_replace — Substitution of equals, valid both ways.
• S07 · premise_audit · L_affine_limit, distributive, mul_inverse_nonzero — The same four steps as S03 to S06 with the roles of x and y exchanged; N2 checks the numerator identity independently.
• S06 · premise_audit · S04, S05, S01 — Two functions that agree for h≠0 have the same limit; the value at h=0 plays no role.
• S05.2 · premise_audit · abs_rules, order_basics, forall_intro — Uses |uv|=|u||v|, that multiplying by a nonnegative number preserves ≤, and that multiplying by a positive number preserves <; only an upper bound is claimed.
• S05.1 · premise_audit · abs_rules, order_basics — A positive number divided by a positive number is positive; δ depends only on ε and B.
• S05 · premise_audit · L_affine_limit, func_limit_def — 0 is a limit point of ℝ∖{0}, so the function limit makes sense.
• S04 · inverse_equivalence · mul_inverse_nonzero, frac_rules — Multiplying by 1/h and by h undo each other, given h≠0.
• S03.2 · inverse_equivalence · distributive, mul_comm — Factoring and expanding undo each other.
• S03.1 · inverse_equivalence · distributive, power_laws, add_inverse — Each term is an identity expansion; only the terms containing x survive, which is exactly the effect of fixing y.
• S03 · inverse_equivalence · L_numerator_x, distributive — This is an algebraic identity valid for all x, y, h, so it holds both ways.
• S02 · premise_audit · mko_mvf_def — Coefficient order is part of the input contract. A permutation can change the polynomial and its partials, but not every permutation must do so: swapping equal coefficients changes nothing. The worked c_1=−2 and c_2=3 are unequal, and swapping them does change the displayed partials.
• S01 · premise_audit · mko_partial_def — Only unfolds the definition; h=0 is excluded because the quotient is undefined there.

Error controls and negative controls

Do not move both coordinates

One misconception named by the MKO is to change both coordinates at once. In S12, (f(1+h,2+h)−f(1,2))/h→5, while the x-partial is 4. The definition of the x-partial requires y to stay fixed, with h added to the first coordinate only.

One quotient is not the partial

Another misconception named by the MKO is to claim a partial exists from one nonzero-h quotient. Here q_x(h)=4+h is never 4 for nonzero h (h=1 gives 5, h=1/10 gives 41/10). Even when some finite difference happens to give the right number (for example the central difference (q_x(1)+q_x(−1))/2=(5+3)/2=4), that is a feature of quadratics, not a proof of existence: for u(x,y)=|x| at (0,0), the central difference (|h|−|−h|)/(2h)=0 for every h≠0, yet the x-partial does not exist (the right quotient is 1 and the left quotient is −1).

Existence of partials does not imply continuity

MKO assumption a2 warns that existing partials are not used to infer continuity of general functions. Example: g(x,y)=xy/(x²+y²) for (x,y)≠(0,0) and g(0,0)=0. g(x,0)=0 and g(0,y)=0 for all x, y, so both partials exist at the origin and equal 0; but along y=x, g(t,t)=1/2 for all t≠0, which does not tend to g(0,0)=0, so g is not continuous at the origin.

• q_x(1)=5, so f_x(1,2)=5 → reject — The partial is the limit as h→0: q_x(h)=4+h→4 (S10, S11).
• (f(1+h,2+h)−f(1,2))/h→5, so the x-partial is 5 → reject — This moves y as well; with y=2 fixed the limit is 4 (S12).
• If both partials of a function exist at a point, it is continuous there → reject — g(x,y)=xy/(x²+y²), g(0,0)=0 has both partials 0 at the origin, but g(t,t)=1/2 (error control 3).
• If the central difference (q(h)+q(−h))/2 gives a number for some h, the partial exists and equals it → reject — For u(x,y)=|x| at (0,0) the central difference is always 0, yet the x-partial does not exist (error control 2).

Result and limitations

For f=c_0+c_1x+c_2y+c_3x²+c_4xy+c_5y², the quotient is affine in h for h≠0, so f_x=c_1+2c_3x+c_4y and f_y=c_2+c_4x+2c_5y. For c=(1,−2,3,1,2,−1): f_x=−2+2x+2y, f_y=3+2x−2y, giving the gradient (4,1) at (1,2). q_x(h)=4+h differs from 4 for every nonzero h; moving both coordinates gives the limit 5.

• The non-polynomial examples of error controls 2 and 3 are argued in prose, not in numbered steps; the main conclusions do not depend on them.
• The geometric meaning of the gradient, total differentiability and higher partials (the MKO's formal next) are out of scope.

Verification and source binding

11 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: cec61d27ae749c4333888ce08539fdb4a14ce72bd62e3e9d85ee86ac92f9eab1
• original source SHA-256: 277ef1a5d5807fe90f5ab864bef246dbbc0d025aaa5183b9a9d7f44340c942e7
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)