Analytic continuation along a path

An analytic continuation along a path γ is the classical device that turns a single holomorphic germ into a multi-valued function: one carries the germ along γ, re-expanding it at each parameter time. This file introduces that notion and proves its fundamental property, that a continuation is determined by its initial germ.

A continuation is recorded as a family f : X → ℂ → E of functions indexed by the path parameter, subject to the requirement that f t be analytic at γ t and that the germ of f u at γ u agree with the germ of f t at γ u for all u near t. Equivalently — and this is the way to read the definition — the assignment t ↦ (germ of f t at γ t) is a continuous lift of γ to the étale space of holomorphic germs — literally so, by TauCeti.isAnalyticContinuationAlong_iff_continuousOn_germPoint of Conformal/Continuation/Etale.lean. The classical "chain of overlapping discs" definition is the same condition written with explicit discs; the germ formulation avoids carrying the discs around.

The parameter space X is an arbitrary topological space, and the parameter set s : Set X is constrained only by IsPreconnected where the mathematics needs it. Nothing here uses the order or the field structure of the reals, so the usual X = ℝ with s = Set.Icc 0 1 and Mathlib's Path, whose parameter space is unitInterval, are both directly available.

Generality

The germs carried are germs of maps ℂ → E into a complex normed space E. The generality is free rather than speculative: every analytic fact this file consumes is one Mathlib already states for maps into an arbitrary normed space, so the scalar case is not one line shorter. The uniqueness theorem rests on Mathlib's identity principle AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq and on the openness of the analyticity locus AnalyticAt.exists_ball_analyticOnNhd; DifferentiableOn.analyticOnNhd produces continuations from holomorphy; and the closure lemmas below consume AnalyticAt.deriv, .add and .neg, and AnalyticAt.mul and .pow for the two that multiply germs. In the words of the generality bar of TauCetiRoadmap/ConformalMapping/README.md, these are inputs consumed from Mathlib at whatever generality Mathlib provides; the conformal-mapping theorems that consume this file — the reflection and boundary layers — are scalar and stay scalar, instantiating E = ℂ.

Completeness of E is asked for exactly where those Mathlib inputs ask for it, and nowhere else: the definition itself, the gluing and reparametrisation lemmas, and the closure of continuations under sums and products need none, while everything resting on the identity principle — TauCeti.IsAnalyticContinuationAlong.eventuallyEq and all of its consequences — needs E to be a Banach space.

The domain stays ℂ. That is where the roadmap's scalar bar bites: a path in a higher-dimensional domain is not the object the monodromy theorem and its consumers are about, and deriv — under which continuations are closed below — is one-dimensional. The two closure lemmas that multiply germs, TauCeti.IsAnalyticContinuationAlong.mul and .pow, ask for a complex normed algebra A in place of E, again the generality at which Mathlib states AnalyticAt.mul.

The uniqueness theorem

TauCeti.IsAnalyticContinuationAlong.eventuallyEq: two continuations along the same path over a preconnected parameter set whose germs agree at one parameter time agree at every parameter time.

The proof is the standard connectedness argument. Germ agreement is a locally constant property of the parameter: at a time t, both f t and g t are analytic on a common disc D about γ t, so by the identity principle (AnalyticOnNhd.eqOn_of_preconnected_of_eventuallyEq) their germs agree at one point of D exactly when they agree at every point of D — and for u near t the point γ u lies in D while the germs of f u, g u at γ u are those of f t, g t. A locally constant property on a preconnected parameter set is constant (IsLocallyConstant.apply_eq_of_preconnectedSpace).

Continuability as a property of the initial germ

A continuation is determined by its initial germ, so being continuable is a property of that germ alone. TauCeti.ContinuesAlong records it for a single path of the unit interval, and TauCeti.ContinuesInside for every path inside a domain issuing from a base point; both transport across eventual equality of the initial function (TauCeti.continuesAlong_congr, TauCeti.continuesInside_congr). TauCeti.ContinuesInside is the hypothesis of the monodromy theorem for a simply connected domain (Conformal/GlobalBranch.lean).

Both predicates are closed under the additive and the ring operations and under differentiation, because a continuation of a combination of germs is the corresponding combination of continuations of the parts: the closure lemmas of TauCeti.IsAnalyticContinuationAlong transport to them verbatim, with no choice of continuation to reconcile. A function analytic at every point of a continuous path continues along it via the constant family (TauCeti.ContinuesAlong.of_analyticAt), so continuability is a condition one may check on the pieces of a germ built from simpler ones. They are also closed under concatenating paths, which Continuation/Trans.lean proves.

Relation to the monodromy theorem

This is the L4 prerequisite that the monodromy theorem of the conformal-mapping roadmap needs: uniqueness of the continuation along a fixed path. The monodromy theorem itself compares continuations along homotopic paths, and in the étale-space picture is an instance of Mathlib's abstract IsLocalHomeomorph.monodromy_theorem (Mathlib/Topology/Homotopy/Lifting.lean), whose docstring describes exactly this application; the uniqueness proved here is the concrete form of the separatedness hypothesis that abstract theorem consumes. That étale space is built in TauCeti/Analysis/Complex/HolomorphicSheaf.lean, and Conformal/Continuation/Etale.lean supplies the continuation/lift correspondence needed to apply the abstract theorem to it.

Main definitions and results

• TauCeti.IsAnalyticContinuationAlong — f is an analytic continuation along γ over the parameter set s.
• TauCeti.IsAnalyticContinuationAlong.const, .of_differentiableOn — a holomorphic function continues itself along any path in its domain.
• TauCeti.IsAnalyticContinuationAlong.congr, .congr_path — only the carried germs matter, and only the values of the path on the parameter set.
• TauCeti.IsAnalyticContinuationAlong.union — continuations glue over two closed parameter sets.
• TauCeti.IsAnalyticContinuationAlong.deriv, .add, .mul, .neg, .sub, .pow — continuations are closed under the germ-wise operations.
• TauCeti.IsAnalyticContinuationAlong.reparam — a continuation transports along any reparametrisation of the path by a continuous map into its parameter set, of which restriction to a smaller parameter set (TauCeti.IsAnalyticContinuationAlong.mono) is the identity case.
• TauCeti.IsAnalyticContinuationAlong.eventuallyEq — uniqueness: a continuation over a preconnected parameter set is determined by its germ at a single time.
• TauCeti.IsAnalyticContinuationAlong.eventuallyEq_of_mapsTo — continuing a holomorphic function along a path that stays inside its domain gives that function back.
• TauCeti.ContinuesAlong, TauCeti.ContinuesInside — continuability of a germ along one path, and along every path inside a domain. Neither body is exposed; downstream files use them through TauCeti.continuesAlong_iff_exists, TauCeti.ContinuesInside.continuesAlong and TauCeti.ContinuesInside.of_forall.
• TauCeti.ContinuesAlong.add, .mul, .neg, .sub, .pow, .deriv and their TauCeti.ContinuesInside counterparts — continuability of a germ is inherited by sums, products, differences, powers and derivatives.

References

• L. Ahlfors, Complex Analysis, Ch. 8 §1.
• J. B. Conway, Functions of One Complex Variable I (GTM 11), Ch. IX §2–3.
• W. Rudin, Real and Complex Analysis, Ch. 16.

Germ agreement is a locally constant property

theorem TauCeti.eventuallyEq_nhds_of_analyticOnNhd_ball {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {F G : ℂ → E} {c : ℂ} {r : ℝ} (hF : AnalyticOnNhd ℂ F (Metric.ball c r)) (hG : AnalyticOnNhd ℂ G (Metric.ball c r)) {z w : ℂ} (hz : z ∈ Metric.ball c r) (hw : w ∈ Metric.ball c r) (h : F =ᶠ[nhds z] G) : F =ᶠ[nhds w] G

Two functions analytic on a ball whose germs agree at one point of the ball have equal germs at every point of the ball. This is the identity principle in germ form: the ball is preconnected, so agreement near one of its points propagates to all of it, and the ball is open, so agreement on it is agreement near each of its points.

theorem TauCeti.eventually_eventuallyEq_iff_of_analyticAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] {F G : ℂ → E} {z : ℂ} (hF : AnalyticAt ℂ F z) (hG : AnalyticAt ℂ G z) : ∀ᶠ (w : ℂ) in nhds z, F =ᶠ[nhds w] G ↔ F =ᶠ[nhds z] G

Germ agreement is locally constant. If F and G are both analytic at z, then for all w near z the germs of F and G agree at w exactly when they agree at z.

Analytic continuation along a path

structure TauCeti.IsAnalyticContinuationAlong {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {X : Type u_2} [TopologicalSpace X] (f : X → ℂ → E) (γ : X → ℂ) (s : Set X) : Prop

IsAnalyticContinuationAlong f γ s says that the family f is an analytic continuation along the path γ over the parameter set s: for each parameter time t ∈ s the function f t is analytic at the point γ t, and the germ carried at time t is locally constant in t, in the sense that f u and f t have the same germ at γ u for every u ∈ s close enough to t.

Only the germ of f t at γ t matters; the values of f t away from γ t are unconstrained. Reading the germs as points of the étale space of holomorphic germs over ℂ, the condition says precisely that t ↦ (germ of f t at γ t) is a continuous lift of γ; that is TauCeti.isAnalyticContinuationAlong_iff_continuousOn_germPoint.

• continuousOn : ContinuousOn γ s

  The path is continuous on the parameter set.

• analyticAt (t : X) : t ∈ s → AnalyticAt ℂ (f t) (γ t)

  At each parameter time the carried function is analytic at the corresponding path point.

• locallyEq (t : X) : t ∈ s → ∀ᶠ (u : X) in nhdsWithin t s, f u =ᶠ[nhds (γ u)] f t

  The carried germ varies continuously: nearby parameter times carry the same germ.

theorem TauCeti.IsAnalyticContinuationAlong.reparam {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {X : Type u_2} [TopologicalSpace X] {f : X → ℂ → E} {γ : X → ℂ} {s : Set X} {Y : Type u_3} [TopologicalSpace Y] {φ : Y → X} {s' : Set Y} (hf : IsAnalyticContinuationAlong f γ s) (hφ : ContinuousOn φ s') (hmaps : Set.MapsTo φ s' s) : IsAnalyticContinuationAlong (f ∘ φ) (γ ∘ φ) s'

A continuation transports along a reparametrisation of the path. Precomposing both the family and the path with a map φ of parameters that is continuous on s' and sends s' into s again gives a continuation, over s' and along the reparametrised path γ ∘ φ.

Nothing further is asked of φ — it need not be injective, monotone, or cover s — so this covers restriction (TauCeti.IsAnalyticContinuationAlong.mono, the case φ = id), reversal of a path, and the passage between the parameter conventions X = ℝ with s = Icc 0 1 and X = unitInterval with s = univ that this file's two layers use. Only this direction is claimed: if φ '' s' fails to cover s then part of the original path is dropped, so continuing along γ ∘ φ does not in general continue along γ. The germ carried at a reparametrised time is by construction the germ carried at the original time, so no uniqueness argument is needed: the conclusion is about the same family, read along φ.

theorem TauCeti.IsAnalyticContinuationAlong.mono {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {X : Type u_2} [TopologicalSpace X] {f : X → ℂ → E} {γ : X → ℂ} {s : Set X} (hf : IsAnalyticContinuationAlong f γ s) {s' : Set X} (hs' : s' ⊆ s) : IsAnalyticContinuationAlong f γ s'

A continuation restricts to any smaller parameter set: the case φ = id of TauCeti.IsAnalyticContinuationAlong.reparam.

theorem TauCeti.IsAnalyticContinuationAlong.union {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {X : Type u_2} [TopologicalSpace X] {f : X → ℂ → E} {γ : X → ℂ} {s s' : Set X} (hf : IsAnalyticContinuationAlong f γ s) (hf' : IsAnalyticContinuationAlong f γ s') (hs : IsClosed s) (hs' : IsClosed s') : IsAnalyticContinuationAlong f γ (s ∪ s')

Continuations glue over closed parameter sets. One family of germs that is a continuation along γ over each of two closed parameter sets is a continuation over their union.

Closedness is essential rather than cosmetic. At a parameter time outside the closure of s the locality condition over s is vacuous, so it says nothing about how the germ carried there relates to the germs carried on s; taking both sets closed makes every parameter time of the union cling only to the piece it already lies in.

theorem TauCeti.IsAnalyticContinuationAlong.const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {X : Type u_2} [TopologicalSpace X] {γ : X → ℂ} {s : Set X} {F : ℂ → E} (hγ : ContinuousOn γ s) (hF : ∀ t ∈ s, AnalyticAt ℂ F (γ t)) : IsAnalyticContinuationAlong (fun (x : X) => F) γ s

The constant family is a continuation: a function analytic at every point of the path continues itself along it.

theorem TauCeti.IsAnalyticContinuationAlong.of_differentiableOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {X : Type u_2} [TopologicalSpace X] {γ : X → ℂ} {s : Set X} [CompleteSpace E] {U : Set ℂ} {F : ℂ → E} (hU : IsOpen U) (hF : DifferentiableOn ℂ F U) (hγ : ContinuousOn γ s) (hmem : ∀ t ∈ s, γ t ∈ U) : IsAnalyticContinuationAlong (fun (x : X) => F) γ s

A holomorphic function on an open set continues itself along any path that stays in that set. This is the source of the continuations that a single-valued function admits.

theorem TauCeti.IsAnalyticContinuationAlong.congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {X : Type u_2} [TopologicalSpace X] {f : X → ℂ → E} {γ : X → ℂ} {s : Set X} [CompleteSpace E] (hf : IsAnalyticContinuationAlong f γ s) {f' : X → ℂ → E} (h : ∀ t ∈ s, f' t =ᶠ[nhds (γ t)] f t) : IsAnalyticContinuationAlong f' γ s

A continuation depends only on the germs it carries. Replacing each f t by a function with the same germ at γ t again gives a continuation along γ.

theorem TauCeti.IsAnalyticContinuationAlong.congr_path {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {X : Type u_2} [TopologicalSpace X] {f : X → ℂ → E} {γ : X → ℂ} {s : Set X} (hf : IsAnalyticContinuationAlong f γ s) {γ' : X → ℂ} (h : Set.EqOn γ' γ s) : IsAnalyticContinuationAlong f γ' s

A continuation depends on the path only through its values on the parameter set. This is the path-level companion of TauCeti.IsAnalyticContinuationAlong.congr, which says the same for the family of germs.

theorem TauCeti.IsAnalyticContinuationAlong.deriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {X : Type u_2} [TopologicalSpace X] {f : X → ℂ → E} {γ : X → ℂ} {s : Set X} [CompleteSpace E] (hf : IsAnalyticContinuationAlong f γ s) : IsAnalyticContinuationAlong (fun (t : X) => deriv (f t)) γ s

Differentiating a continuation term by term gives a continuation of the derivative germ.

theorem TauCeti.IsAnalyticContinuationAlong.add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {X : Type u_2} [TopologicalSpace X] {f g : X → ℂ → E} {γ : X → ℂ} {s : Set X} (hf : IsAnalyticContinuationAlong f γ s) (hg : IsAnalyticContinuationAlong g γ s) : IsAnalyticContinuationAlong (f + g) γ s

Continuations add: the pointwise sum family f + g continues along γ as well.

theorem TauCeti.IsAnalyticContinuationAlong.neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {X : Type u_2} [TopologicalSpace X] {f : X → ℂ → E} {γ : X → ℂ} {s : Set X} (hf : IsAnalyticContinuationAlong f γ s) : IsAnalyticContinuationAlong (-f) γ s

Continuations negate: the pointwise negation family -f continues along γ as well.

theorem TauCeti.IsAnalyticContinuationAlong.sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {X : Type u_2} [TopologicalSpace X] {f g : X → ℂ → E} {γ : X → ℂ} {s : Set X} (hf : IsAnalyticContinuationAlong f γ s) (hg : IsAnalyticContinuationAlong g γ s) : IsAnalyticContinuationAlong (f - g) γ s

Continuations subtract: the pointwise difference family f - g continues along γ as well.

theorem TauCeti.IsAnalyticContinuationAlong.mul {X : Type u_2} [TopologicalSpace X] {γ : X → ℂ} {s : Set X} {A : Type u_3} [NormedRing A] [NormedAlgebra ℂ A] {f g : X → ℂ → A} (hf : IsAnalyticContinuationAlong f γ s) (hg : IsAnalyticContinuationAlong g γ s) : IsAnalyticContinuationAlong (f * g) γ s

Continuations multiply: the pointwise product family f * g continues along γ as well.

The germs are allowed to take values in any complex normed algebra, which is the generality at which Mathlib's AnalyticAt.mul is stated.

theorem TauCeti.IsAnalyticContinuationAlong.pow {X : Type u_2} [TopologicalSpace X] {γ : X → ℂ} {s : Set X} {A : Type u_3} [NormedRing A] [NormedAlgebra ℂ A] {f : X → ℂ → A} (hf : IsAnalyticContinuationAlong f γ s) (n : ℕ) : IsAnalyticContinuationAlong (f ^ n) γ s

Continuations take powers: the pointwise power family f ^ n continues along γ as well.

Uniqueness

theorem TauCeti.IsAnalyticContinuationAlong.eventually_eventuallyEq_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {X : Type u_2} [TopologicalSpace X] {f g : X → ℂ → E} {γ : X → ℂ} {s : Set X} [CompleteSpace E] (hf : IsAnalyticContinuationAlong f γ s) (hg : IsAnalyticContinuationAlong g γ s) {t : X} (ht : t ∈ s) : ∀ᶠ (u : X) in nhdsWithin t s, f u =ᶠ[nhds (γ u)] g u ↔ f t =ᶠ[nhds (γ t)] g t

Agreement of two continuations along the same path is a locally constant property of the parameter. This is the local step of the uniqueness theorem.

theorem TauCeti.IsAnalyticContinuationAlong.eventuallyEq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {X : Type u_2} [TopologicalSpace X] {f g : X → ℂ → E} {γ : X → ℂ} {s : Set X} [CompleteSpace E] (hf : IsAnalyticContinuationAlong f γ s) (hg : IsAnalyticContinuationAlong g γ s) (hs : IsPreconnected s) {a b : X} (ha : a ∈ s) (hb : b ∈ s) (hab : f a =ᶠ[nhds (γ a)] g a) : f b =ᶠ[nhds (γ b)] g b

Uniqueness of analytic continuation along a path. Two analytic continuations along the same path, over a preconnected parameter set, that carry the same germ at one parameter time carry the same germ at every parameter time.

Preconnectedness of the parameter set cannot be dropped: over a two-point parameter set the hypotheses put no relation at all between the germs carried at its two points.

theorem TauCeti.IsAnalyticContinuationAlong.eq_of_eventuallyEq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {X : Type u_2} [TopologicalSpace X] {f g : X → ℂ → E} {γ : X → ℂ} {s : Set X} [CompleteSpace E] (hf : IsAnalyticContinuationAlong f γ s) (hg : IsAnalyticContinuationAlong g γ s) (hs : IsPreconnected s) {a b : X} (ha : a ∈ s) (hb : b ∈ s) (hab : f a =ᶠ[nhds (γ a)] g a) : f b (γ b) = g b (γ b)

Two continuations along the same path that carry the same germ at one parameter time take the same value at every parameter time.

theorem TauCeti.IsAnalyticContinuationAlong.eventuallyEq_of_mapsTo {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {X : Type u_2} [TopologicalSpace X] {f : X → ℂ → E} {γ : X → ℂ} {s : Set X} [CompleteSpace E] {U : Set ℂ} {F : ℂ → E} (hf : IsAnalyticContinuationAlong f γ s) (hs : IsPreconnected s) (hU : IsOpen U) (hF : DifferentiableOn ℂ F U) (hmem : ∀ t ∈ s, γ t ∈ U) {a b : X} (ha : a ∈ s) (hb : b ∈ s) (hab : f a =ᶠ[nhds (γ a)] F) : f b =ᶠ[nhds (γ b)] F

A single-valued function is its own continuation. If a path stays inside an open set on which F is holomorphic, then any continuation along that path which starts at the germ of F carries the germ of F throughout. So continuing a holomorphic function inside its domain never produces a new branch: new branches can only appear once the path leaves the domain.

Continuation along a path, as a property of the initial germ

def TauCeti.ContinuesAlong {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f₀ : ℂ → E) (c : ↑unitInterval → ℂ) : Prop

The germ of f₀ at c 0 continues along the path c: there is an analytic continuation along c whose germ at the initial time is that of f₀.

Only the germ of f₀ at c 0 enters, so this is a property of that germ rather than of f₀ (TauCeti.continuesAlong_congr).

Equations

• TauCeti.ContinuesAlong f₀ c = ∃ (f : ↑unitInterval → ℂ → E), TauCeti.IsAnalyticContinuationAlong f c Set.univ ∧ f 0 =ᶠ[nhds (c 0)] f₀

theorem TauCeti.continuesAlong_iff_exists {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f₀ : ℂ → E} {c : ↑unitInterval → ℂ} : ContinuesAlong f₀ c ↔ ∃ (f : ↑unitInterval → ℂ → E), IsAnalyticContinuationAlong f c Set.univ ∧ f 0 =ᶠ[nhds (c 0)] f₀

The defining property of TauCeti.ContinuesAlong: a germ continues along c exactly when some analytic continuation along c starts at it. This is the introduction and elimination rule for the predicate, whose body is not exposed.

theorem TauCeti.ContinuesAlong.analyticAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f₀ : ℂ → E} {c : ↑unitInterval → ℂ} (h : ContinuesAlong f₀ c) : AnalyticAt ℂ f₀ (c 0)

A germ that continues along a path is a germ of an analytic function at the initial point.

theorem TauCeti.ContinuesAlong.congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f₀ g₀ : ℂ → E} {c : ↑unitInterval → ℂ} (h : ContinuesAlong f₀ c) (hfg : f₀ =ᶠ[nhds (c 0)] g₀) : ContinuesAlong g₀ c

Continuability along a path depends only on the initial germ.

theorem TauCeti.ContinuesAlong.of_analyticAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f₀ : ℂ → E} {c : ↑unitInterval → ℂ} (hc : Continuous c) (hf₀ : ∀ (x : ↑unitInterval), AnalyticAt ℂ f₀ (c x)) : ContinuesAlong f₀ c

A function analytic at every point of a path continues itself along it: the constant family is the continuation.

theorem TauCeti.ContinuesAlong.of_differentiableOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set ℂ} {f₀ : ℂ → E} {c : ↑unitInterval → ℂ} [CompleteSpace E] (hUo : IsOpen U) (hf₀ : DifferentiableOn ℂ f₀ U) (hc : Continuous c) (hcU : ∀ (x : ↑unitInterval), c x ∈ U) : ContinuesAlong f₀ c

A function holomorphic on an open set continues along every path that stays in that set.

Closure under the germ-wise operations

Continuing two germs along one path and combining the results is the same as combining first and continuing after: the operations act on the carried germs time by time (TauCeti.IsAnalyticContinuationAlong.add and its companions), so a continuation of the combination is obtained from continuations of the parts, with no new choices to make.

theorem TauCeti.ContinuesAlong.add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f₀ g₀ : ℂ → E} {c : ↑unitInterval → ℂ} (h : ContinuesAlong f₀ c) (h' : ContinuesAlong g₀ c) : ContinuesAlong (f₀ + g₀) c

The sum of two germs that continue along a path continues along it.

theorem TauCeti.ContinuesAlong.neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f₀ : ℂ → E} {c : ↑unitInterval → ℂ} (h : ContinuesAlong f₀ c) : ContinuesAlong (-f₀) c

The negation of a germ that continues along a path continues along it.

theorem TauCeti.ContinuesAlong.sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f₀ g₀ : ℂ → E} {c : ↑unitInterval → ℂ} (h : ContinuesAlong f₀ c) (h' : ContinuesAlong g₀ c) : ContinuesAlong (f₀ - g₀) c

The difference of two germs that continue along a path continues along it.

theorem TauCeti.ContinuesAlong.deriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f₀ : ℂ → E} {c : ↑unitInterval → ℂ} [CompleteSpace E] (h : ContinuesAlong f₀ c) : ContinuesAlong (deriv f₀) c

The derivative of a germ that continues along a path continues along it.

theorem TauCeti.ContinuesAlong.mul {c : ↑unitInterval → ℂ} {A : Type u_3} [NormedRing A] [NormedAlgebra ℂ A] {f₀ g₀ : ℂ → A} (h : ContinuesAlong f₀ c) (h' : ContinuesAlong g₀ c) : ContinuesAlong (f₀ * g₀) c

The product of two germs that continue along a path continues along it.

theorem TauCeti.ContinuesAlong.pow {c : ↑unitInterval → ℂ} {A : Type u_3} [NormedRing A] [NormedAlgebra ℂ A] {f₀ : ℂ → A} (h : ContinuesAlong f₀ c) (n : ℕ) : ContinuesAlong (f₀ ^ n) c

A power of a germ that continues along a path continues along it.

theorem TauCeti.continuesAlong_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f₀ g₀ : ℂ → E} {c : ↑unitInterval → ℂ} (h : f₀ =ᶠ[nhds (c 0)] g₀) : ContinuesAlong f₀ c ↔ ContinuesAlong g₀ c

Continuability along a path is a property of the germ of f₀ at the initial point.

Continuation inside a domain

def TauCeti.ContinuesInside {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] (f₀ : ℂ → E) (U : Set ℂ) (z₀ : ℂ) : Prop

The germ of f₀ at z₀ continues inside U: it continues along every path that starts at z₀ and stays in U.

This is the hypothesis of the monodromy theorem. It is a condition on the germ (TauCeti.continuesInside_congr) and on the domain jointly: the germ of Complex.log at 1 continues inside ℂ \ {0}, and continues inside the slit plane, but is single-valued only on the latter.

Equations

• TauCeti.ContinuesInside f₀ U z₀ = ∀ (c : ↑unitInterval → ℂ), Continuous c → (∀ (x : ↑unitInterval), c x ∈ U) → c 0 = z₀ → TauCeti.ContinuesAlong f₀ c

theorem TauCeti.ContinuesInside.continuesAlong {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set ℂ} {z₀ : ℂ} {f₀ : ℂ → E} {c : ↑unitInterval → ℂ} (H : ContinuesInside f₀ U z₀) (hc : Continuous c) (hcU : ∀ (x : ↑unitInterval), c x ∈ U) (hc0 : c 0 = z₀) : ContinuesAlong f₀ c

Elimination for TauCeti.ContinuesInside: a germ that continues inside U continues along each individual path that starts at z₀ and stays in U.

theorem TauCeti.ContinuesInside.of_forall {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set ℂ} {z₀ : ℂ} {f₀ : ℂ → E} (h : ∀ (c : ↑unitInterval → ℂ), Continuous c → (∀ (x : ↑unitInterval), c x ∈ U) → c 0 = z₀ → ContinuesAlong f₀ c) : ContinuesInside f₀ U z₀

Introduction for TauCeti.ContinuesInside: a germ that continues along every path starting at z₀ and staying in U continues inside U.

theorem TauCeti.ContinuesInside.analyticAt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set ℂ} {z₀ : ℂ} {f₀ : ℂ → E} (H : ContinuesInside f₀ U z₀) (hz₀ : z₀ ∈ U) : AnalyticAt ℂ f₀ z₀

A germ that continues inside U is analytic at the base point, as witnessed by the constant path.

theorem TauCeti.ContinuesInside.congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set ℂ} {z₀ : ℂ} {f₀ g₀ : ℂ → E} (H : ContinuesInside f₀ U z₀) (hfg : f₀ =ᶠ[nhds z₀] g₀) : ContinuesInside g₀ U z₀

Continuability inside a domain depends only on the germ at the base point.

theorem TauCeti.ContinuesInside.of_differentiableOn {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set ℂ} {z₀ : ℂ} {f₀ : ℂ → E} [CompleteSpace E] (hUo : IsOpen U) (hf₀ : DifferentiableOn ℂ f₀ U) : ContinuesInside f₀ U z₀

A function holomorphic on an open set continues inside that set from each of its points.

Closure under the germ-wise operations

Continuability inside U is continuability along each path of U at once, so it inherits the closure properties of TauCeti.ContinuesAlong path by path. Read through the monodromy theorem for a simply connected domain (Conformal/GlobalBranch.lean), these are the statements that a germ assembled from germs extending to U extends to U itself.

theorem TauCeti.ContinuesInside.add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set ℂ} {z₀ : ℂ} {f₀ g₀ : ℂ → E} (H : ContinuesInside f₀ U z₀) (H' : ContinuesInside g₀ U z₀) : ContinuesInside (f₀ + g₀) U z₀

The sum of two germs that continue inside a domain continues inside it.

theorem TauCeti.ContinuesInside.neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set ℂ} {z₀ : ℂ} {f₀ : ℂ → E} (H : ContinuesInside f₀ U z₀) : ContinuesInside (-f₀) U z₀

The negation of a germ that continues inside a domain continues inside it.

theorem TauCeti.ContinuesInside.sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set ℂ} {z₀ : ℂ} {f₀ g₀ : ℂ → E} (H : ContinuesInside f₀ U z₀) (H' : ContinuesInside g₀ U z₀) : ContinuesInside (f₀ - g₀) U z₀

The difference of two germs that continue inside a domain continues inside it.

theorem TauCeti.ContinuesInside.deriv {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set ℂ} {z₀ : ℂ} {f₀ : ℂ → E} [CompleteSpace E] (H : ContinuesInside f₀ U z₀) : ContinuesInside (deriv f₀) U z₀

The derivative of a germ that continues inside a domain continues inside it. If U is open and simply connected and contains z₀, the derivative therefore has a branch of its own on U (TauCeti.ContinuesInside.exists_analyticOnNhd).

theorem TauCeti.ContinuesInside.mul {U : Set ℂ} {z₀ : ℂ} {A : Type u_3} [NormedRing A] [NormedAlgebra ℂ A] {f₀ g₀ : ℂ → A} (H : ContinuesInside f₀ U z₀) (H' : ContinuesInside g₀ U z₀) : ContinuesInside (f₀ * g₀) U z₀

The product of two germs that continue inside a domain continues inside it.

theorem TauCeti.ContinuesInside.pow {U : Set ℂ} {z₀ : ℂ} {A : Type u_3} [NormedRing A] [NormedAlgebra ℂ A] {f₀ : ℂ → A} (H : ContinuesInside f₀ U z₀) (n : ℕ) : ContinuesInside (f₀ ^ n) U z₀

A power of a germ that continues inside a domain continues inside it.

theorem TauCeti.continuesInside_congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {U : Set ℂ} {z₀ : ℂ} {f₀ g₀ : ℂ → E} (h : f₀ =ᶠ[nhds z₀] g₀) : ContinuesInside f₀ U z₀ ↔ ContinuesInside g₀ U z₀

Continuability inside U is a property of the germ of f₀ at the base point.