hasStrictFDerivAt_piLp — Mathlib

English

There is a canonical strict derivative from ToLp to an appropriate PiLp representation; the derivative is given by the continuous linear equivalence.

Русский

Существует каноническая строгая производная от ToLp к соответствующему представлению PiLp; производная задается непрерывно-линейным эквалентом.

LaTeX

$$$$ HasStrictFDerivAt\\bigl( WithLp.toLp p \\bigr)\\Big( (PiLp.continuousLinearEquiv p 𝕜 E).toContinuousLinearMap f \\Bigr). $$$$

Lean4

theorem hasStrictFDerivAt_piLp :
    HasStrictFDerivAt f f' y ↔ ∀ i, HasStrictFDerivAt (fun x => f x i) (PiLp.proj _ _ i ∘L f') y :=
  by
  rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_hasStrictFDerivAt_iff, hasStrictFDerivAt_pi']
  rfl

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