fderivPolarCoordSymm — Mathlib

English

The derivative of the inverse polar coordinate map at p = (r, θ) is given by the 2×2 matrix [[cos θ, -r sin θ], [sin θ, r cos θ]].

Русский

Производная обратной полярной карты в точке p=(r,θ) задаётся матрицей [[cos θ, -r sin θ], [sin θ, r cos θ]].

LaTeX

$$$$ D(\mathrm{polarCoord.symm})(p) = \begin{pmatrix} \cos p_2 & -p_1 \sin p_2 \\ \sin p_2 & p_1 \cos p_2 \end{pmatrix}. $$$$

Lean4

/-- The derivative of `polarCoord.symm`, see `hasFDerivAt_polarCoord_symm`. -/
def fderivPolarCoordSymm (p : ℝ × ℝ) : ℝ × ℝ →L[ℝ] ℝ × ℝ :=
  (Matrix.toLin (.finTwoProd ℝ) (.finTwoProd ℝ)
      !![cos p.2, -p.1 * sin p.2; sin p.2, p.1 * cos p.2]).toContinuousLinearMap

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