Properties of analyticity restricted to a set

From Mathlib.Analysis.Analytic.Basic, we have the definitions

1. AnalyticWithinAt 𝕜 f s x means a power series at x converges to f on 𝓝[insert x s] x.
2. AnalyticOn 𝕜 f s t means ∀ x ∈ t, AnalyticWithinAt 𝕜 f s x.

This means there exists an extension of f which is analytic and agrees with f on s ∪ {x}, but f is allowed to be arbitrary elsewhere.

Here we prove basic properties of these definitions. Where convenient we assume completeness of the ambient space, which allows us to relate AnalyticWithinAt to analyticity of a local extension.

Basic properties

theorem analyticWithinAt_of_singleton_mem {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} {x : E} (h : {x} ∈ nhdsWithin x s) : AnalyticWithinAt 𝕜 f s x

AnalyticWithinAt is trivial if {x} ∈ 𝓝[s] x

theorem analyticOn_of_locally_analyticOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (h : ∀ x ∈ s, ∃ (u : Set E), IsOpen u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)) : AnalyticOn 𝕜 f s

If f is AnalyticOn near each point in a set, it is AnalyticOn the set

@[deprecated analyticOn_of_locally_analyticOn]

theorem analyticWithinOn_of_locally_analyticWithinOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (h : ∀ x ∈ s, ∃ (u : Set E), IsOpen u ∧ x ∈ u ∧ AnalyticOn 𝕜 f (s ∩ u)) : AnalyticOn 𝕜 f s

Alias of analyticOn_of_locally_analyticOn.

---

If f is AnalyticOn near each point in a set, it is AnalyticOn the set

theorem IsOpen.analyticOn_iff_analyticOnNhd {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (hs : IsOpen s) : AnalyticOn 𝕜 f s ↔ AnalyticOnNhd 𝕜 f s

On open sets, AnalyticOnNhd and AnalyticOn coincide

@[deprecated IsOpen.analyticOn_iff_analyticOnNhd]

theorem IsOpen.analyticWithinOn_iff_analyticOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (hs : IsOpen s) : AnalyticOn 𝕜 f s ↔ AnalyticOnNhd 𝕜 f s

Alias of IsOpen.analyticOn_iff_analyticOnNhd.

---

On open sets, AnalyticOnNhd and AnalyticOn coincide

Equivalence to analyticity of a local extension

We show that HasFPowerSeriesWithinOnBall, HasFPowerSeriesWithinAt, and AnalyticWithinAt are equivalent to the existence of a local extension with full analyticity. We do not yet show a result for AnalyticOn, as this requires a bit more work to show that local extensions can be stitched together.

theorem hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} : HasFPowerSeriesWithinOnBall f p s x r ↔ ∃ (g : E → F), Set.EqOn f g (insert x s ∩ EMetric.ball x r) ∧ HasFPowerSeriesOnBall g p x r

f has power series p at x iff some local extension of f has that series

theorem hasFPowerSeriesWithinAt_iff_exists_hasFPowerSeriesAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} : HasFPowerSeriesWithinAt f p s x ↔ ∃ (g : E → F), f =ᶠ[nhdsWithin x (insert x s)] g ∧ HasFPowerSeriesAt g p x

f has power series p at x iff some local extension of f has that series

theorem analyticWithinAt_iff_exists_analyticAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {s : Set E} {x : E} : AnalyticWithinAt 𝕜 f s x ↔ ∃ (g : E → F), f =ᶠ[nhdsWithin x (insert x s)] g ∧ AnalyticAt 𝕜 g x

f is analytic within s at x iff some local extension of f is analytic at x

theorem analyticWithinAt_iff_exists_analyticAt' {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {s : Set E} {x : E} : AnalyticWithinAt 𝕜 f s x ↔ ∃ (g : E → F), f x = g x ∧ Set.EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x

f is analytic within s at x iff some local extension of f is analytic at x. In this version, we make sure that the extension coincides with f on all of insert x s.

theorem AnalyticWithinAt.exists_analyticAt {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {s : Set E} {x : E} : AnalyticWithinAt 𝕜 f s x → ∃ (g : E → F), f x = g x ∧ Set.EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x

Alias of the forward direction of analyticWithinAt_iff_exists_analyticAt'.

---

f is analytic within s at x iff some local extension of f is analytic at x. In this version, we make sure that the extension coincides with f on all of insert x s.

theorem AnalyticWithinAt.exists_mem_nhdsWithin_analyticOn {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {s : Set E} {x : E} (h : AnalyticWithinAt 𝕜 f s x) : ∃ u ∈ nhdsWithin x (insert x s), AnalyticOn 𝕜 f u