Documentation

Mathlib.Analysis.Analytic.Within

Properties of analyticity restricted to a set #

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

AnalyticWithinAt 𝕜 f s x means a power series at x converges to f on 𝓝[s] x, and f is continuous within s at x.
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 #

@[simp]

theorem hasFPowerSeriesWithinOnBall_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal} :

HasFPowerSeriesWithinOnBall f p Set.univ x r ↔ HasFPowerSeriesOnBall f p x r

@[simp]

theorem hasFPowerSeriesWithinAt_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {x : E} :

HasFPowerSeriesWithinAt f p Set.univ x ↔ HasFPowerSeriesAt f p x

@[simp]

theorem analyticWithinAt_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} :

AnalyticWithinAt 𝕜 f Set.univ x ↔ AnalyticAt 𝕜 f x

theorem analyticWithinOn_univ {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} :

AnalyticWithinOn 𝕜 f Set.univ ↔ AnalyticOn 𝕜 f Set.univ

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

ContinuousWithinAt f s x

theorem AnalyticWithinAt.continuousWithinAt {𝕜 : 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 : AnalyticWithinAt 𝕜 f s x) :

ContinuousWithinAt f s x

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 AnalyticAt.analyticWithinAt {𝕜 : 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 : AnalyticAt 𝕜 f x) :

AnalyticWithinAt 𝕜 f s x

Analyticity implies analyticity within any s

theorem AnalyticOn.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 : AnalyticOn 𝕜 f s) :

AnalyticWithinOn 𝕜 f s

Analyticity on s implies analyticity within s

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

@[simp]

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 ↔ ContinuousWithinAt f s x ∧ ∃ (g : E → F), Set.EqOn f g (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 ↔ ContinuousWithinAt f s x ∧ ∃ (g : E → F), f =ᶠ[nhdsWithin 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 ↔ ContinuousWithinAt f s x ∧ ∃ (g : E → F), f =ᶠ[nhdsWithin 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.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} (h : AnalyticWithinAt 𝕜 f s x) :

∃ (g : E → F), f x = g x ∧ f =ᶠ[nhdsWithin x s] g ∧ AnalyticAt 𝕜 g x

If f is analytic within s at x, some local extension of f is analytic at x

Congruence #

We require completeness to use equivalence to locally extensions, but this is nonessential.

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] [CompleteSpace F] {f : E → F} {g : E → F} {s : Set E} {x : E} (hf : AnalyticWithinAt 𝕜 f s x) (hs : f =ᶠ[nhdsWithin x s] g) (hx : f x = g 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] [CompleteSpace F] {f : E → F} {g : E → F} {s : Set E} {x : E} (hf : AnalyticWithinAt 𝕜 f s x) (hs : Set.EqOn f g s) (hx : f x = g 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] [CompleteSpace F] {f : E → F} {g : E → F} {s : Set E} (hf : AnalyticWithinOn 𝕜 f s) (hs : Set.EqOn f g s) :

AnalyticWithinOn 𝕜 g s

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

theorem HasFPowerSeriesWithinOnBall.mono {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {t : Set E} {x : E} {r : ENNReal} (h : HasFPowerSeriesWithinOnBall f p t x r) (hs : s ⊆ t) :

HasFPowerSeriesWithinOnBall f p s x r

theorem HasFPowerSeriesWithinAt.mono {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {p : FormalMultilinearSeries 𝕜 E F} {s : Set E} {t : Set E} {x : E} (h : HasFPowerSeriesWithinAt f p t x) (hs : s ⊆ t) :

HasFPowerSeriesWithinAt f p s x

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

AnalyticWithinAt 𝕜 f s x

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