English
If h has a Taylor series up to order n with n≥1, then for any x∈s with h on s, the derivative within s exists and equals the first-order term of the series at x.
Русский
Если существует разложение Тейлора до порядка n с n≥1, то для любого x∈s производная внутри s существует и равна первому порядку ряда в точке x.
LaTeX
$$$$\text{HasFTaylorSeriesUpToOn}(n,f,p,s) \land 1\le n \Rightarrow \text{HasFDerivWithinAt}(f, \text{continuousMultilinearCurryFin1}(p\,x\,1), s, x).$$$$
Lean4
/-- If a function has a Taylor series at order at least `1`, then the term of order `1` of this
series is a derivative of `f`. -/
theorem hasFDerivWithinAt (h : HasFTaylorSeriesUpToOn n f p s) (hn : 1 ≤ n) (hx : x ∈ s) :
HasFDerivWithinAt f (continuousMultilinearCurryFin1 𝕜 E F (p x 1)) s x :=
by
have A : ∀ y ∈ s, f y = (continuousMultilinearCurryFin0 𝕜 E F) (p y 0) := fun y hy ↦ (h.zero_eq y hy).symm
suffices H :
HasFDerivWithinAt (continuousMultilinearCurryFin0 𝕜 E F ∘ (p · 0)) (continuousMultilinearCurryFin1 𝕜 E F (p x 1)) s
x
from H.congr A (A x hx)
rw [LinearIsometryEquiv.comp_hasFDerivWithinAt_iff']
have : ((0 : ℕ) : ℕ∞) < n := zero_lt_one.trans_le hn
convert h.fderivWithin _ this x hx
ext y v
change (p x 1) (snoc 0 y) = (p x 1) (cons y v)
congr with i
rw [Unique.eq_default (α := Fin 1) i]
rfl
