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. AnalyticWithinOn 𝕜 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. Requiring ContinuousWithinAt is essential if x ∉ s: it is required for composition and smoothness to follow without extra hypotheses (we could alternately require convergence at x even if x ∉ s).

Here we prove basic properties of these definitions. Where convenient we assume completeness of the ambient space, which allows us to related 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 AnalyticWithinOn.continuousOn {𝕜 : 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 : AnalyticWithinOn 𝕜 f s) : ContinuousOn f s

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 ∧ AnalyticWithinOn 𝕜 f (s ∩ u)) : AnalyticWithinOn 𝕜 f s

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

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) : AnalyticWithinOn 𝕜 f s ↔ AnalyticOn 𝕜 f s

On open sets, AnalyticOn and AnalyticWithinOn 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 AnalyticWithinOn, 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.

Congruence

theorem HasFPowerSeriesWithinOnBall.congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {g : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} {r : ENNReal} (h : HasFPowerSeriesWithinOnBall f p s x r) (h' : Set.EqOn g f (s ∩ EMetric.ball x r)) (h'' : g x = f x) : HasFPowerSeriesWithinOnBall g p s x r

theorem HasFPowerSeriesWithinAt.congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {g : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {x : E} (h : HasFPowerSeriesWithinAt f p s x) (h' : g =ᶠ[nhdsWithin x s] f) (h'' : g x = f x) : HasFPowerSeriesWithinAt g p s x

theorem AnalyticWithinAt.congr_of_eventuallyEq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {g : E → F} {s : Set E} {x : E} (hf : AnalyticWithinAt 𝕜 f s x) (hs : g =ᶠ[nhdsWithin x s] f) (hx : g x = f x) : AnalyticWithinAt 𝕜 g s x

theorem AnalyticWithinAt.congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {g : E → F} {s : Set E} {x : E} (hf : AnalyticWithinAt 𝕜 f s x) (hs : Set.EqOn g f s) (hx : g x = f x) : AnalyticWithinAt 𝕜 g s x

theorem AnalyticWithinOn.congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {g : E → F} {s : Set E} (hf : AnalyticWithinOn 𝕜 f s) (hs : Set.EqOn g f s) : AnalyticWithinOn 𝕜 g s

Monotonicity w.r.t. the set we're analytic within

theorem AnalyticWithinOn.mono {𝕜 : 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} {t : Set E} (h : AnalyticWithinOn 𝕜 f t) (hs : s ⊆ t) : AnalyticWithinOn 𝕜 f s

Analyticity within respects composition

Currently we require CompleteSpaces to use equivalence to local extensions, but this is not essential.

theorem AnalyticWithinAt.comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [CompleteSpace F] [CompleteSpace G] {f : F → G} {g : E → F} {s : Set F} {t : Set E} {x : E} (hf : AnalyticWithinAt 𝕜 f s (g x)) (hg : AnalyticWithinAt 𝕜 g t x) (h : Set.MapsTo g t s) : AnalyticWithinAt 𝕜 (f ∘ g) t x

theorem AnalyticWithinOn.comp {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] [CompleteSpace F] [CompleteSpace G] {f : F → G} {g : E → F} {s : Set F} {t : Set E} (hf : AnalyticWithinOn 𝕜 f s) (hg : AnalyticWithinOn 𝕜 g t) (h : Set.MapsTo g t s) : AnalyticWithinOn 𝕜 (f ∘ g) t

Analyticity within implies smoothness

theorem AnalyticWithinAt.contDiffWithinAt {𝕜 : 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) {n : ℕ∞} : ContDiffWithinAt 𝕜 n f s x

theorem AnalyticWithinOn.contDiffOn {𝕜 : 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} (h : AnalyticWithinOn 𝕜 f s) {n : ℕ∞} : ContDiffOn 𝕜 n f s

Analyticity within respects products

theorem HasFPowerSeriesWithinOnBall.prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {e : E} {f : E → F} {g : E → G} {s : Set E} {r : ENNReal} {t : ENNReal} {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜 E G} (hf : HasFPowerSeriesWithinOnBall f p s e r) (hg : HasFPowerSeriesWithinOnBall g q s e t) : HasFPowerSeriesWithinOnBall (fun (x : E) => (f x, g x)) (p.prod q) s e (min r t)

theorem HasFPowerSeriesWithinAt.prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {e : E} {f : E → F} {g : E → G} {s : Set E} {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜 E G} (hf : HasFPowerSeriesWithinAt f p s e) (hg : HasFPowerSeriesWithinAt g q s e) : HasFPowerSeriesWithinAt (fun (x : E) => (f x, g x)) (p.prod q) s e

theorem AnalyticWithinAt.prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {e : E} {f : E → F} {g : E → G} {s : Set E} (hf : AnalyticWithinAt 𝕜 f s e) (hg : AnalyticWithinAt 𝕜 g s e) : AnalyticWithinAt 𝕜 (fun (x : E) => (f x, g x)) s e

theorem AnalyticWithinOn.prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} {G : Type u_4} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedAddCommGroup G] [NormedSpace 𝕜 G] {f : E → F} {g : E → G} {s : Set E} (hf : AnalyticWithinOn 𝕜 f s) (hg : AnalyticWithinOn 𝕜 g s) : AnalyticWithinOn 𝕜 (fun (x : E) => (f x, g x)) s