hasLineDerivAt — Mathlib

English

For every quadratic map f, there is a HasLineDerivAt at any pair (a, b) with value equal to the polar form.

Русский

Для квадратичного отображения f существует HasLineDerivAt в любой паре (a, b), значение равно полярной форме.

LaTeX

$$$ HasLineDerivAt 𝕜 f (polar f a b) a b$$$

Lean4

theorem hasLineDerivAt (f : QuadraticMap 𝕜 E F) (a b : E) : HasLineDerivAt 𝕜 f (polar f a b) a b := by
  simpa [HasLineDerivAt, QuadraticMap.map_add, f.map_smul] using
    ((hasDerivAt_const (0 : 𝕜) (f a)).add <|
          ((hasDerivAt_id 0).mul (hasDerivAt_id 0)).smul (hasDerivAt_const 0 (f b))).add
      ((hasDerivAt_id 0).smul (hasDerivAt_const 0 (polar f a b)))

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