hasDerivAt_circleMap — Mathlib

English

For every c ∈ ℂ, R ∈ ℝ and θ ∈ ℝ, the map θ ↦ circleMap(c, R, θ) is differentiable at θ, and its derivative is i · circleMap(0, R, θ).

Русский

Для любых c ∈ ℂ, R ∈ ℝ и θ ∈ ℝ функция θ ↦ circleMap(c, R, θ) дифференцируема в точке θ, производная равна i · circleMap(0, R, θ).

LaTeX

$$$\displaystyle \frac{d}{d\theta}\bigl(circleMap(c,R,\theta)\bigr) = i\, circleMap(0,R,\theta).$$$

Lean4

theorem hasDerivAt_circleMap (c : ℂ) (R : ℝ) (θ : ℝ) : HasDerivAt (circleMap c R) (circleMap 0 R θ * I) θ := by
  simpa only [mul_assoc, one_mul, ofRealCLM_apply, circleMap, ofReal_one, zero_add] using
    (((ofRealCLM.hasDerivAt (x := θ)).mul_const I).cexp.const_mul (R : ℂ)).const_add c

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