The derivative of a function of one variable is a number. For a function of two variables it cannot be: moving east and moving north give different rates, and so does every direction in between. The honest definition is a linear map, the differential, that approximates the change in the function, and everything else in this chapter is read off it.
Take f(x, y) = x2y + y3. Freeze y and vary x: the quotient (f(x+h, y) − f(x, y))/h is exactly 2xy + yh, so the partial derivative in x is 2xy. Freeze x and vary y: the quotient is x2 + 3y2 + 3yk + k2, so the partial in y is x2 + 3y2. The script prints both identities in exact fractions at five points.
The partials say how f changes along two axes. The differential says more: there is one linear map L(h, k) = fx h + fy k so that f(x+h, y+k) − f(x, y) − L(h, k) is small compared with the size of (h, k). For this f the remainder is exactly y h2 + 2x hk + h2k + 3y k2 + k3, and for |h|, |k| ≤ 1 it is at most (4|y| + 2|x| + 2)(|h| + |k|)2. Since (|h|+|k|)2/(|h|+|k|) = |h|+|k| goes to 0, the remainder is smaller than the step by as much as you like. The script checks the formula and the bound on 300 random steps at each of five points.
In Loomis and Sternberg this is the definition of the differential (§ 6, p.140), and Theorem 9.2 (p.157) says that for a map on ℝn the partial derivatives are the skeleton of the differential: the value of the differential on a vector (y1, …, yn) is Σ yj ∂F/∂xj. In Lean the plane case is differential_is_partials_combination, and partial_x_eq_differential says the partial in x is the differential applied to (1, 0). The two worked derivatives above are partial_x_example and partial_y_example.
Move from (x, y) in direction (a, b): the quotient (f(x+ta, y+tb) − f(x, y))/t tends to a fx + b fy. For our f the gap between the two is exactly t(y a2 + 2x ab + 3y b2) + t2(a2b + b3), which the script checks for fifteen point-and-direction pairs. This is Theorem 7.1 (p.147): when the differential exists, the directional derivative is the differential applied to the direction. In Lean it is directional_derivative_eq_differential, stated for any normed space, not only the plane, and proved from Mathlib's chain rule.
Now ask which direction makes f grow fastest. Write the gradient as (a, b) = (fx, fy) and the direction as a unit vector (u, v). The rate is a u + b v, and (au + bv)2 + (av − bu)2 = (a2 + b2)(u2 + v2) = a2 + b2. So a u + b v ≤ √(a2 + b2), with equality exactly when (u, v) points along (a, b). At (1, 2) the gradient is (4, 13), so the steepest rate is √185. The script checks that (4u+13v)2 ≤ 185 for several thousand rational unit vectors and that some come within 10−4 of it. The two Lean statements are directional_derivative_le_gradient_norm and directional_derivative_attains. This is a consequence of Theorem 9.2 and the Schwarz inequality, not a theorem the book states in this form.
Differentiate f in x and then in y, or the other way round. For nice functions you get the same thing: ∂2f/∂y∂x = ∂2f/∂x∂y. Loomis and Sternberg state it as Theorem 16.3 (p.187): the second differential is a symmetric function of its two arguments, and Theorem 16.2 says it exists when all second partials exist and are continuous. In Lean this is second_differential_symmetric, for any twice continuously differentiable function on a normed space, proved by Mathlib's own symmetry theorem.
The hypothesis is not decoration. Let f(x, y) = xy(x2 − y2)/(x2 + y2) and f(0, 0) = 0. Along the column x = 0, fx(0, y) = −y, because (f(h, y) − f(0, y))/h = y(h2 − y2)/(h2 + y2), which is within 2h2/|y| of −y. Along the row y = 0, fy(x, 0) = x. So the mixed partial at the origin is −1 one way and +1 the other. The script shows the mixed quotient f(h, k)/(hk) = (h2 − k2)/(h2 + k2) exactly, then gives values within 10−6 of −1 and of +1 depending on which step is taken to 0 first. The Lean file proves this as cf_dx, cf_dy and mixed_partials_differ. Here the second partials exist at the origin but are not continuous there, so the theorem does not apply, and it correctly gives no answer.
To integrate f(x, y) over a rectangle, integrate in x with y held fixed, then integrate the result in y. For a polynomial on [0, 2] × [1, 3] the script does this in both orders with exact antiderivatives and gets the same fraction. It also shows the midpoint sum on an n × n grid approaching that value, with the error falling by about a factor of 4 each time n doubles (n = 5, 10, 20, 40). Loomis and Sternberg treat this in § 12 (p.346): a contented function is contented relative to a splitting ℝn = ℝk × ℝl when the inner integrals exist and the result is again integrable, and then the integral is the iterated one. This is not in the Lean file. The page shows exact examples only, and that is not a proof of the theorem.
Apply the matrix with rows (A, B) and (C, D) to a rectangle. The image is a parallelogram, and its area is |AD − BC| times the rectangle’s. The script computes the area of the image of a 3 × 2 rectangle by the shoelace formula for every integer matrix with entries from −3 to 3 (2401 of them, including the singular ones) and finds 6|AD − BC| each time. In Loomis and Sternberg this is Theorem 8.1 (p.335): the content of L(A) is |det L| times the content of A, for every contented set. In Lean it is area_scales_by_det, a direct call to Mathlib’s Haar-measure scaling lemma on the plane, so it covers every measurable set and not only rectangles.
The next chapter, Foundations of Analysis, is where the completeness steps used here and in chapter 7 are examined.