English
ContDiffOn on univ is equivalent to ContDiff.
Русский
ContDiffOn на все множество эквивалентно ContDiff.
LaTeX
$$$contDiffOn_univ\ 𝕜\ n\ f\leftrightarrow ContDiff\ 𝕜\ n\ f$$$
Lean4
theorem contDiffOn_univ : ContDiffOn 𝕜 n f univ ↔ ContDiff 𝕜 n f := by
match n with
| ω =>
constructor
· intro H
use ftaylorSeriesWithin 𝕜 f univ
rw [← hasFTaylorSeriesUpToOn_univ_iff]
refine ⟨H.ftaylorSeriesWithin uniqueDiffOn_univ, fun i ↦ ?_⟩
rw [← analyticOn_univ]
exact H.analyticOn.iteratedFDerivWithin uniqueDiffOn_univ _
· rintro ⟨p, hp, h'p⟩ x _
exact ⟨univ, Filter.univ_sets _, p, (hp.hasFTaylorSeriesUpToOn univ).of_le le_top, fun i ↦ (h'p i).analyticOn⟩
| (n : ℕ∞) =>
constructor
· intro H
use ftaylorSeriesWithin 𝕜 f univ
rw [← hasFTaylorSeriesUpToOn_univ_iff]
exact H.ftaylorSeriesWithin uniqueDiffOn_univ
· rintro ⟨p, hp⟩ x _ m hm
exact ⟨univ, Filter.univ_sets _, p, (hp.hasFTaylorSeriesUpToOn univ).of_le (mod_cast hm)⟩
