Analytic functions are C^∞. #
theorem
AnalyticOnNhd.contDiffOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{s : Set E}
{n : WithTop ℕ∞}
[CompleteSpace F]
(h : AnalyticOnNhd 𝕜 f s)
:
ContDiffOn 𝕜 n f s
An analytic function is infinitely differentiable.
theorem
AnalyticOnNhd.contDiff
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{n : WithTop ℕ∞}
[CompleteSpace F]
(h : AnalyticOnNhd 𝕜 f Set.univ)
:
ContDiff 𝕜 n f
An analytic function on the whole space is infinitely differentiable there.
theorem
AnalyticAt.contDiffAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
{f : E → F}
{x : E}
[CompleteSpace F]
(h : AnalyticAt 𝕜 f x)
{n : ℕ∞}
:
ContDiffAt 𝕜 (↑n) f x
theorem
AnalyticWithinAt.contDiffWithinAt
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{f : E → F}
{s : Set E}
{x : E}
(h : AnalyticWithinAt 𝕜 f s x)
{n : ℕ∞}
:
ContDiffWithinAt 𝕜 (↑n) f s x
theorem
AnalyticOn.contDiffOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{f : E → F}
{s : Set E}
(h : AnalyticOn 𝕜 f s)
{n : ℕ∞}
:
ContDiffOn 𝕜 (↑n) f s
@[deprecated AnalyticOn.contDiffOn]
theorem
AnalyticWithinOn.contDiffOn
{𝕜 : Type u_1}
[NontriviallyNormedField 𝕜]
{E : Type u_2}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
{F : Type u_3}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[CompleteSpace F]
{f : E → F}
{s : Set E}
(h : AnalyticOn 𝕜 f s)
{n : ℕ∞}
:
ContDiffOn 𝕜 (↑n) f s
Alias of AnalyticOn.contDiffOn.