English
If n ≠ ∞, then ContDiffOn 𝕜 (n+1) f s iff for every x ∈ s there is a neighborhood u in 𝓝[insert x s] x with (n = ω → AnalyticOn 𝕜 f u) and ∃ f' : E → E →L[𝕜] F such that ∀ x ∈ u HasFDerivWithinAt f (f' x) u x and ContDiffOn 𝕜 n f' u.
Русский
Если n ≠ ∞, то ContDiffOn 𝕜 (n+1) f s эквивалентно тому, что вокруг каждой x ∈ s существует окрестность u в 𝓝[insert x s] x такая что (n = ω → AnalyticOn 𝕜 f u) и существует линейное производное f' по u, удовлетворяющее HasFDerivWithinAt f (f' x) u x и ContDiffOn 𝕜 n f' u.
LaTeX
$$$ContDiffOn\\ 𝕜\\ (n+1)\\ f\\ s\\ \\leftrightarrow\\ (\\forall x\\in s,\\exists u\\in\\mathcal{N}[insert x s] x,\\ (n=ω\\to AnalyticOn\\ 𝕜 f\\ u)\\land \\exists f' : E\\to E\\toL[𝕜] F,\\ (\\forall x\\in u, HasFDerivWithinAt f (f' x) u x) \\land ContDiffOn\\ 𝕜 n\\ f'\\ u)$$$
Lean4
/-- When a function is `C^n` in a set `s` of unique differentiability, it admits
`ftaylorSeriesWithin 𝕜 f s` as a Taylor series up to order `n` in `s`. -/
protected theorem ftaylorSeriesWithin (h : ContDiffOn 𝕜 n f s) (hs : UniqueDiffOn 𝕜 s) :
HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f s) s :=
by
constructor
· intro x _
simp only [ftaylorSeriesWithin, ContinuousMultilinearMap.curry0_apply, iteratedFDerivWithin_zero_apply]
· intro m hm x hx
have : (m + 1 : ℕ) ≤ n := ENat.add_one_natCast_le_withTop_of_lt hm
rcases (h x hx).of_le this _ le_rfl with ⟨u, hu, p, Hp⟩
rw [insert_eq_of_mem hx] at hu
rcases mem_nhdsWithin.1 hu with ⟨o, o_open, xo, ho⟩
rw [inter_comm] at ho
have : p x m.succ = ftaylorSeriesWithin 𝕜 f s x m.succ :=
by
change p x m.succ = iteratedFDerivWithin 𝕜 m.succ f s x
rw [← iteratedFDerivWithin_inter_open o_open xo]
exact (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl (hs.inter o_open) ⟨hx, xo⟩
rw [← this, ← hasFDerivWithinAt_inter (IsOpen.mem_nhds o_open xo)]
have A : ∀ y ∈ s ∩ o, p y m = ftaylorSeriesWithin 𝕜 f s y m :=
by
rintro y ⟨hy, yo⟩
change p y m = iteratedFDerivWithin 𝕜 m f s y
rw [← iteratedFDerivWithin_inter_open o_open yo]
exact (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn (mod_cast Nat.le_succ m) (hs.inter o_open) ⟨hy, yo⟩
exact
((Hp.mono ho).fderivWithin m (mod_cast lt_add_one m) x ⟨hx, xo⟩).congr (fun y hy => (A y hy).symm)
(A x ⟨hx, xo⟩).symm
· intro m hm
apply continuousOn_of_locally_continuousOn
intro x hx
rcases (h x hx).of_le hm _ le_rfl with ⟨u, hu, p, Hp⟩
rcases mem_nhdsWithin.1 hu with ⟨o, o_open, xo, ho⟩
rw [insert_eq_of_mem hx] at ho
rw [inter_comm] at ho
refine ⟨o, o_open, xo, ?_⟩
have A : ∀ y ∈ s ∩ o, p y m = ftaylorSeriesWithin 𝕜 f s y m :=
by
rintro y ⟨hy, yo⟩
change p y m = iteratedFDerivWithin 𝕜 m f s y
rw [← iteratedFDerivWithin_inter_open o_open yo]
exact (Hp.mono ho).eq_iteratedFDerivWithin_of_uniqueDiffOn le_rfl (hs.inter o_open) ⟨hy, yo⟩
exact ((Hp.mono ho).cont m le_rfl).congr fun y hy => (A y hy).symm
