English
If a function has a power series within a set and is analytic on that set, then the derivative within the set at point is given by the derivative within the set and adjusted by analyticOn.
Русский
Если функция имеет степенную серию внутри множества и аналитична на этом множестве, то внутри множество производная даёт правильную аппроксимацию производной.
LaTeX
$$$h.fderivWithin_of_mem_of_analyticOn\\ (hr)\\ (h a) \\Rightarrow \\text{HasFDerivWithinAt } f f' (s) x$$$
Lean4
/-- If a function has a power series `p` within a set of unique differentiability, inside a ball,
and is differentiable at a point, then the derivative series of `p` is summable at a point, with
sum the given differential. Note that this theorem does not require completeness of the space. -/
theorem hasSum_derivSeries_of_hasFDerivWithinAt (h : HasFPowerSeriesWithinOnBall f p s x r) {f' : E →L[𝕜] F} {y : E}
(hy : (‖y‖₊ : ℝ≥0∞) < r) (h'y : x + y ∈ insert x s) (hf' : HasFDerivWithinAt f f' (insert x s) (x + y))
(hu : UniqueDiffOn 𝕜 (insert x s)) : HasSum (fun n ↦ p.derivSeries n (fun _ ↦ y)) f' := by
/- In the completion of the space, the derivative series is summable, and its sum is a derivative
of the function. Therefore, by uniqueness of derivatives, its sum is the image of `f'` under
the canonical embedding. As this is an embedding, it means that there was also convergence in
the original space, to `f'`. -/
let F' := UniformSpace.Completion F
let a : F →L[𝕜] F' := UniformSpace.Completion.toComplL
let b : (E →L[𝕜] F) →ₗᵢ[𝕜] (E →L[𝕜] F') := UniformSpace.Completion.toComplₗᵢ.postcomp
rw [← b.isEmbedding.hasSum_iff]
have : HasFPowerSeriesWithinOnBall (a ∘ f) (a.compFormalMultilinearSeries p) s x r :=
a.comp_hasFPowerSeriesWithinOnBall h
have Z := (this.fderivWithin hu).hasSum h'y (by simpa [edist_zero_eq_enorm] using hy)
have : fderivWithin 𝕜 (a ∘ f) (insert x s) (x + y) = a ∘L f' :=
by
apply HasFDerivWithinAt.fderivWithin _ (hu _ h'y)
exact a.hasFDerivAt.comp_hasFDerivWithinAt (x + y) hf'
rw [this] at Z
convert Z with n
ext v
simp only [FormalMultilinearSeries.derivSeries, ContinuousLinearMap.coe_sum', Finset.sum_apply,
ContinuousLinearMap.compFormalMultilinearSeries_apply, FormalMultilinearSeries.changeOriginSeries,
ContinuousLinearMap.compContinuousMultilinearMap_coe, ContinuousLinearEquiv.coe_coe, LinearIsometryEquiv.coe_coe,
Function.comp_apply, ContinuousMultilinearMap.sum_apply, map_sum]
rfl
