Properties of analyticity restricted to a set #
From Mathlib.Analysis.Analytic.Basic
, we have the definitions
AnalyticWithinAt ๐ f s x
means a power series atx
converges tof
on๐[s] x
, andf
is continuous withins
atx
.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 #
AnalyticWithinAt
is trivial if {x} โ ๐[s] x
Analyticity implies analyticity within any s
Analyticity on s
implies analyticity within s
If f
is AnalyticWithinOn
near each point in a set, it is AnalyticWithinOn
the set
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.
f
has power series p
at x
iff some local extension of f
has that series
f
has power series p
at x
iff some local extension of f
has that series
f
is analytic within s
at x
iff some local extension of f
is analytic at 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.
Monotonicity w.r.t. the set we're analytic within #
Analyticity within respects composition #
Currently we require CompleteSpace
s to use equivalence to local extensions, but this is not
essential.