Multivariable calculus

Functions on R^n: partial derivatives, gradients, Jacobians, Hessians, implicit functions, regular level sets and tangent spaces, curve length, Green's theorem, multivariable Taylor expansions and counterexamples about mixed partials or continuity at the origin.

• Continuity and differentiability at the origin in the plane
• Existence of mixed partial derivatives
• Gradient
• Hessian matrix
• Jacobian matrix
• Length of a curve
• Partial derivatives and symmetry of mixed partials
• Tangent spaces of level sets

TheoremA unit-norm curve in \(\mathbb{R}^3\) is orthogonal to its derivative#●ready to prove

Let \(f : \mathbb{R} \to \mathbb{R}^3\) be a differentiable map such that \(\|f(t)\| = 1\) for every real \(t\), where \(\|\cdot\|\) is the Euclidean norm. Then \(\langle f'(t), f(t) \rangle = 0\) for every real \(t\), where \(\langle \cdot, \cdot \rangle\) is the standard inner product on \(\mathbb{R}^3\).

public theorem_wanted inner_deriv_self_eq_zero_of_norm_eq_one
    (f : ℝ → EuclideanSpace ℝ (Fin 3)) (hf : Differentiable ℝ f) (hnorm : ∀ t : ℝ, ‖f t‖ = 1) :
    ∀ t : ℝ, ⟪deriv f t, f t⟫_ℝ = 0

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Functions of one variable), problem ma_proofbench_l1_49.

TheoremAn implicit function for \(x^2y_1+e^x+y_2=0\) near \((1,-1)\)#●ready to prove

Let \(f(x,y_1,y_2)=x^2y_1+e^x+y_2\) on \(\mathbb{R}^3\). Then there are an open set \(U\subseteq\mathbb{R}^2\) containing \((1,-1)\) and a function \(g : \mathbb{R}^2 \to \mathbb{R}\), differentiable on \(U\), with \(g(1,-1)=0\) and \(f(g(y_1,y_2),y_1,y_2)=0\) for all \((y_1,y_2)\in U\).

public theorem_wanted exists_implicit_function_sq_mul_add_exp_add
    (f : ℝ → ℝ → ℝ → ℝ) (hf : f = fun x y₁ y₂ => x ^ 2 * y₁ + Real.exp x + y₂) :
    ∃ (U : Set (ℝ × ℝ)), IsOpen U ∧ ((1, -1) ∈ U) ∧
      ∃ g : (ℝ × ℝ) → ℝ,
        DifferentiableOn ℝ g U ∧ g (1, -1) = 0 ∧ ∀ y ∈ U, f (g y) y.1 y.2 = 0

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Functions of several variables), problem ma_proofbench_l1_43.

TheoremChange of variables to spherical coordinates#●ready to prove

Let \(E\) be a real Banach space and let \(f \colon \mathbb{R}^3 \to E\) be any function. Then the integral of \(f\) over \(\mathbb{R}^3\) equals the integral over the set of \((r, \theta, \varphi) \in \mathbb{R}^3\) with \(r > 0\), \(0 < \theta < 2\pi\) and \(0 < \varphi < \pi\) of \(r^2 \sin\varphi \cdot f(r \sin\varphi \cos\theta,\, r \sin\varphi \sin\theta,\, r \cos\varphi)\), both integrals being Bochner integrals with respect to Lebesgue measure.

No integrability hypothesis is assumed; as usual for Bochner integrals, a non-integrable function has integral \(0\). This is the three-dimensional analogue of the polar-coordinate change of variables.

public theorem_wanted integral_comp_spherical_symm
    {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
    (f : ℝ × ℝ × ℝ → E) :
    (∫ p in {p : ℝ × ℝ × ℝ |
        0 < p.1 ∧ 0 < p.2.1 ∧ p.2.1 < 2 * Real.pi ∧ 0 < p.2.2 ∧ p.2.2 < Real.pi},
      (p.1 ^ 2 * Real.sin p.2.2 : ℝ) •
        f (p.1 * Real.sin p.2.2 * Real.cos p.2.1,
          p.1 * Real.sin p.2.2 * Real.sin p.2.1, p.1 * Real.cos p.2.2)) =
      ∫ p, f p

Sources

• W. Rudin, Real and Complex Analysis, 3rd ed., Ch. 8, Exercise 4 (spherical coordinates in ℝ³).
• https://en.wikipedia.org/wiki/Spherical_coordinate_system#Integration_and_differentiation_in_spherical_coordinates

TheoremEqual partial derivatives give a factor \(x+y\)#●ready to prove

Let \(f : \mathbb{R}^2 \to \mathbb{R}\) be continuously differentiable with \(\partial_1 f = \partial_2 f\) on \(\mathbb{R}^2\) and \(f(0,0)=0\). Then there is a continuous \(g : \mathbb{R}^2 \to \mathbb{R}\) with \(f(x,y)=g(x,y)\,(x+y)\) for all \((x,y)\in\mathbb{R}^2\).

public theorem_wanted exists_continuous_mul_add_of_fderiv_eq {f : ℝ × ℝ → ℝ} (hf : ContDiff ℝ 1 f)
    (hpar : ∀ p : ℝ × ℝ, (fderiv ℝ f p) (1, 0) = (fderiv ℝ f p) (0, 1))
    (h0 : f (0, 0) = 0) :
    ∃ g : ℝ × ℝ → ℝ, Continuous g ∧
      ∀ x y : ℝ, f (x, y) = g (x, y) * (x + y)

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level I (Real functions; Functions of several variables), problem ma_proofbench_l1_02.

TheoremGreen's theorem#●ready to prove

Let \(U \subseteq \mathbb{R}^2\) be open, let \(D \subseteq U\) be bounded and measurable, and let \(L, M : \mathbb{R}^2 \to \mathbb{R}\) be continuously differentiable on \(U\). Let \(a\lt b\) and let \(\gamma=(\gamma_1,\gamma_2) : \mathbb{R} \to \mathbb{R}^2\) be continuous on \([a,b]\), with \(\gamma(a)=\gamma(b)\), injective on \([a,b)\), with \(\gamma(t)\ne\gamma(a)\) for \(a\lt t\lt b\), with image \(\gamma([a,b])\) equal to the boundary of \(D\), and with \(\gamma(t)\in U\) for all \(t\in[a,b]\). Suppose there is a finite set \(S\subseteq[a,b]\) containing \(a\) and \(b\) such that \(\gamma\) is continuously differentiable on \([a,b]\setminus S\) and on \([u,v]\) for any two consecutive points \(u\lt v\) of \(S\), and such that for every \(t\in(a,b)\setminus S\) we have \(\gamma'(t)\ne0\) and, for some \(\delta>0\), \(\gamma(t)+\varepsilon(-\gamma_2'(t),\gamma_1'(t))\in D\) for all \(0\lt \varepsilon\lt \delta\) (so \(D\) lies to the left of the curve). Then

\[ \int_a^b \bigl(L(\gamma(t))\,\gamma_1'(t)+M(\gamma(t))\,\gamma_2'(t)\bigr)\,dt =\int_D \Bigl(\frac{\partial M}{\partial x}-\frac{\partial L}{\partial y}\Bigr)\,d(x,y). \]

MetaMathlibExt.greens_theorem · 31 lines

theorem_wanted greens_theorem
    (U D : Set (ℝ × ℝ))
    (a b : ℝ)
    (γ : ℝ → ℝ × ℝ)
    (L M : ℝ × ℝ → ℝ)
    (hU : IsOpen U)
    (hDU : D ⊆ U)
    (hD_bdd : Bornology.IsBounded D)
    (hD_meas : MeasurableSet D)
    (hL : ContDiffOn ℝ 1 L U)
    (hM : ContDiffOn ℝ 1 M U)
    (hab : a < b)
    (hγcont : ContinuousOn γ (Set.Icc a b))
    (hγclosed : γ a = γ b)
    (hγinj : Set.InjOn γ (Set.Ico a b))
    (hγsimple : ∀ t ∈ Set.Ioo a b, γ t ≠ γ a)
    (hγtrace : γ '' Set.Icc a b = frontier D)
    (hγU : ∀ t ∈ Set.Icc a b, γ t ∈ U)
    (hγpw : ∃ S : Finset ℝ, a ∈ S ∧ b ∈ S ∧ ↑S ⊆ Set.Icc a b ∧
      ContDiffOn ℝ 1 γ (Set.Icc a b \ ↑S) ∧
      (∀ u v : ℝ, u ∈ S → v ∈ S → u < v → Set.Ioo u v ∩ ↑S = ∅ →
        ContDiffOn ℝ 1 γ (Set.Icc u v)) ∧
      ∀ t ∈ Set.Ioo a b \ ↑S, deriv γ t ≠ 0 ∧
        ∃ δ > 0, ∀ ε : ℝ, 0 < ε → ε < δ →
          γ t + ε • (-(deriv γ t).2, (deriv γ t).1) ∈ D) :
    (∫ t in a..b,
      (L (γ t) * deriv (fun t => (γ t).1) t +
        M (γ t) * deriv (fun t => (γ t).2) t)) =
    ∫ p in D,
      (deriv (fun x => M (x, p.2)) p.1 -
        deriv (fun y => L (p.1, y)) p.2) ∂volume

Sources

• https://en.wikipedia.org/wiki/Green%27s_theorem.

TheoremSmooth functions vanishing on the axes are \(O(|x|\,|y|)\) near the origin#●ready to prove

Let \(f : \mathbb{R}^2 \to \mathbb{R}\) be infinitely differentiable with \(f(x,y) = 0\) whenever \(xy = 0\). Then there is a constant \(C > 0\) such that \(|f(x,y)| \le C\,|x|\,|y|\) for all real \(x\) and \(y\) with \(|x| < 1\) and \(|y| < 1\), that is, on the open unit ball of \(\mathbb{R}^2\) for the maximum norm.

public theorem_wanted exists_abs_le_mul_abs_mul_abs_of_contDiff_of_eq_zero_on_axes
    (f : ℝ × ℝ → ℝ)
    (hf : ContDiff ℝ (⊤ : ℕ∞) f)
    (hzero : ∀ x y : ℝ, x * y = 0 → f (x, y) = 0) :
    ∃ C : ℝ, 0 < C ∧
      ∀ x y : ℝ, (x, y) ∈ Metric.ball (0 : ℝ × ℝ) 1 →
        |f (x, y)| ≤ C * |x| * |y|

Sources

• MA-ProofBench (L. Pu et al., arXiv:2606.13782), Level II (Real functions; Functions of several variables), problem ma_proofbench_l2_01.

TheoremTaylor's theorem with little-o remainder in several variables#●ready to prove

Let \(E\) and \(F\) be normed vector spaces over \(\mathbb{R}\), let \(n\) be a natural number, and let \(f : E \to F\) be \(n\) times continuously differentiable on a neighbourhood of a point \(x_0 \in E\). Write \(D^k f(x_0)\) for the \(k\)-th Fréchet derivative of \(f\) at \(x_0\), a continuous \(k\)-linear map from \(E^k\) to \(F\). Then, as \(x\) tends to \(x_0\),

\[f(x) - \sum_{k=0}^{n} \frac{1}{k!}\, D^k f(x_0)(x - x_0, \ldots, x - x_0) = o\bigl(\|x - x_0\|^n\bigr).\]

public theorem_wanted taylor_isLittleO_multivariable
    {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
    [NormedAddCommGroup F] [NormedSpace ℝ F]
    {f : E → F} {x₀ : E} {n : ℕ} (hf : ContDiffAt ℝ n f x₀) :
    (fun x ↦ f x - ∑ k ∈ Finset.range (n + 1),
      ((Nat.factorial k : ℝ))⁻¹ •
        iteratedFDeriv ℝ k f x₀ (fun _ ↦ x - x₀)) =o[nhds x₀]
      fun x ↦ ‖x - x₀‖ ^ n

Sources

• The integral-remainder form exists as map_add_eq_sum_add_integral_iteratedFDeriv.
• H. Cartan, Differential Calculus, Ch. III, Taylor's formula with remainder.
• https://en.wikipedia.org/wiki/Taylor%27s_theorem#Taylor's_theorem_in_several_variables

7 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.