gradient_eq_deriv — Mathlib

English

gradient_eq_deriv: ∇ g u = starRingEnd 𝕜 (deriv g u) with standard caveats about differentiability.

Русский

Градиент функции g в точке u равен сопряжению производной: ∇ g u = starRingEnd 𝕜 (deriv g u), если дифференцируема; в противном случае обе стороны равны 0.

LaTeX

$$$\\nabla g u = \\starRingEnd 𝕜\\ (\\ deriv\\ g\\ u)$$$

Lean4

theorem gradient_eq_deriv : ∇ g u = starRingEnd 𝕜 (deriv g u) :=
  by
  by_cases h : DifferentiableAt 𝕜 g u
  · rw [h.hasGradientAt.hasDerivAt.deriv, RCLike.conj_conj]
  · rw [gradient_eq_zero_of_not_differentiableAt h, deriv_zero_of_not_differentiableAt h, map_zero]

Похожие утверждения