fderivPiPolarCoordSymm — Mathlib

English

The derivative of polarCoord.symm with respect to a Pi-parameter is obtained componentwise from the derivatives fderivPolarCoordSymm(p_i).

Русский

Производная polarCoord.symm по координатам Пи-диапазона получается компонентно из производных fderivPolarCoordSymm(p_i).

LaTeX

$$$fderivPiPolarCoordSymm(p) = \pi_i\bigl( (fderivPolarCoordSymm(p_i)) \circ (\mathrm{proj}_i) \bigr).$$$

Lean4

/-- The derivative of `polarCoord.symm` on `ι → ℝ × ℝ`, see `hasFDerivAt_pi_polarCoord_symm`. -/
noncomputable def fderivPiPolarCoordSymm (p : ι → ℝ × ℝ) : (ι → ℝ × ℝ) →L[ℝ] ι → ℝ × ℝ :=
  pi fun i ↦ (fderivPolarCoordSymm (p i)).comp (proj i)

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