Higher smoothness of continuously polynomial functions #
We prove that continuously polynomial functions are C^∞. In particular, this is the case
of continuous multilinear maps.
theorem
CPolynomialOn.contDiffOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{s : Set E}
(h : CPolynomialOn 𝕜 f s)
{n : WithTop ℕ∞}
:
ContDiffOn 𝕜 n f s
A polynomial function is infinitely differentiable.
theorem
CPolynomialAt.contDiffAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{x : E}
(h : CPolynomialAt 𝕜 f x)
{n : WithTop ℕ∞}
:
ContDiffAt 𝕜 n f x
theorem
ContinuousMultilinearMap.contDiffAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{ι : Type u_2}
{E : ι → Type u_3}
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[Fintype ι]
(f : ContinuousMultilinearMap 𝕜 E F)
{n : WithTop ℕ∞}
{x : (i : ι) → E i}
:
ContDiffAt 𝕜 n (⇑f) x
theorem
ContinuousMultilinearMap.contDiff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{F : Type v}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{ι : Type u_2}
{E : ι → Type u_3}
[(i : ι) → NormedAddCommGroup (E i)]
[(i : ι) → NormedSpace 𝕜 (E i)]
[Fintype ι]
(f : ContinuousMultilinearMap 𝕜 E F)
{n : WithTop ℕ∞}
:
ContDiff 𝕜 n ⇑f