English
Characterization: HasFTaylorSeriesUpToOn(0) f p s holds exactly when f is continuous on s and the 0-th coefficient p(x,0) equals f(x) for all x in s.
Русский
Характеризация: HasFTaylorSeriesUpToOn(0) f p s эквивалентно непрерывности f на s и равенству нулевого коэффициента p(x,0) и f(x) на каждом x∈s.
LaTeX
$$$$\text{HasFTaylorSeriesUpToOn}(0,f,p,s) \iff \big(\text{ContinuousOn}(f,s) \land \forall x\in s, (p(x,0)).\text{curry0} = f(x)\big).$$$$
Lean4
theorem hasFTaylorSeriesUpToOn_zero_iff :
HasFTaylorSeriesUpToOn 0 f p s ↔ ContinuousOn f s ∧ ∀ x ∈ s, (p x 0).curry0 = f x :=
by
refine
⟨fun H => ⟨H.continuousOn, H.zero_eq⟩, fun H => ⟨H.2, fun m hm => False.elim (not_le.2 hm bot_le), fun m hm ↦ ?_⟩⟩
obtain rfl : m = 0 := mod_cast hm.antisymm (zero_le _)
have : EqOn (p · 0) ((continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) s := fun x hx ↦
(continuousMultilinearCurryFin0 𝕜 E F).eq_symm_apply.2 (H.2 x hx)
rw [continuousOn_congr this, LinearIsometryEquiv.comp_continuousOn_iff]
exact H.1
