differentiable_piLp — Mathlib

English

The strict derivative of a PiLp-valued function is determined coordinatewise by the projections onto each E i via the inverse of the canonical equivalence.

Русский

Строгая производная функции с значением в PiLp задается по координатам через проекции на каждое E_i через обратное от канонического эквивалентного отображения.

LaTeX

$$$$ HasStrictFDerivAt\\bigl( WithLp.equiv p ((i) → E i) \\bigr)^{ -1} \\cdot f = \\cdot \\text{coordinatewise derivative via } PiLp.proj. $$$$

Lean4

theorem differentiable_piLp : Differentiable 𝕜 f ↔ ∀ i, Differentiable 𝕜 fun x => f x i :=
  by
  rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_differentiable_iff, differentiable_pi]
  rfl

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