Analytic continuation along a concatenation of paths

Continuation/Basic.lean carries a holomorphic germ along a single path and proves that the result is determined by the initial germ. This file supplies the other half of the basic calculus of analytic continuation: continuing along γ and then along δ is continuing along the concatenated path γ.trans δ, and conversely a continuation along a concatenation restricts to one along each factor.

The gluing engine

Both directions run on general facts about TauCeti.IsAnalyticContinuationAlong, stated for an arbitrary parameter space in Continuation/Basic.lean and consumed here:

• only the values of the path on the parameter set matter (TauCeti.IsAnalyticContinuationAlong.congr_path);
• one family of germs that continues over each of two closed parameter sets continues over their union (TauCeti.IsAnalyticContinuationAlong.union) — closedness being what makes the gluing true rather than a convenience, since the locality condition over a parameter set is vacuous outside its closure.

The restriction direction needs no gluing at all: reading γ as the first half of γ.trans δ is a reparametrisation, and TauCeti.IsAnalyticContinuationAlong.reparam already transports a continuation along any reparametrisation.

The concatenated family

The family of germs carried along γ.trans δ is written down explicitly, as TauCeti.transFamily: on the first half of the parameter interval it is the family carried along γ, read at twice the parameter, and on the second half the one carried along δ. Assembling two families indexed by the unit interval into one is pure reparametrisation, so TauCeti.transFamily carries values in an arbitrary sort and is specialised to germs only where continuations are concatenated. The two halves are compared at the junction, where TauCeti.transFamily takes the value coming from γ; the hypothesis of TauCeti.IsAnalyticContinuationAlong.trans is exactly that the germ γ delivers there agrees with the germ δ starts from.

Moving the base point

The pay-off is that continuability inside a domain does not depend on the base point: TauCeti.continuesInside_of_isAnalyticContinuationAlong says that if a germ continues inside U from z₀ — the hypothesis the monodromy theorem for a simply connected domain runs on (Conformal/GlobalBranch.lean) — and is continued along a path inside U to a germ at z₁, then that germ continues inside U from z₁. Concatenation supplies the paths issuing from z₁, and restriction plus uniqueness of continuation along a fixed path identify the germ reached halfway.

Transport is in fact an equivalence, TauCeti.continuesInside_iff_of_isAnalyticContinuationAlong: the reversed path p.symm carries the germ back, the family read backwards being a continuation along it by TauCeti.IsAnalyticContinuationAlong.reparam. So no endpoint of the path is distinguished — continuability inside U is a property of the domain and of the branch being carried, and any point the branch reaches may serve as its base point.

Main results

• TauCeti.transFamily — the family of germs carried along a concatenation.
• TauCeti.IsAnalyticContinuationAlong.trans — continuations concatenate: two continuations whose germs match at the junction assemble into a continuation along γ.trans δ.
• TauCeti.continuesAlong_trans — the germ-level form: a germ that continues along γ to a germ that continues along δ continues along γ.trans δ.
• TauCeti.IsAnalyticContinuationAlong.left_of_trans, .right_of_trans — continuations restrict: a continuation along γ.trans δ reads as a continuation along γ and one along δ.
• TauCeti.ContinuesAlong.left_of_trans — the germ-level form of the first of those: a germ that continues along γ.trans δ continues along γ.
• TauCeti.continuesInside_of_isAnalyticContinuationAlong — continuability inside a domain travels with the germ: continuing inside U along a path of U again continues inside U.
• TauCeti.continuesInside_iff_of_isAnalyticContinuationAlong — the equivalence: the two germs at the ends of such a path continue inside U together, or neither does.

Generality

Germs of maps ℂ → E into a complex Banach space, as in Continuation/Basic.lean, where the choice is discussed; the conformal-mapping consumers instantiate E = ℂ. TauCeti.transFamily is pure reparametrisation and is stated for values in an arbitrary sort, and the two restriction lemmas need no completeness, being reparametrisations as well.

Coordination with upstream Mathlib

This is basic API for layer L4 of the conformal-mapping roadmap (TauCetiRoadmap/ConformalMapping/README.md), analytic continuation and the reflection principle. Mathlib has no analytic continuation along a path, and L4 is absent from mathlib4#33505, the in-progress human-curated Riemann-mapping-theorem effort, which stops at the mapping theorem itself. So nothing here is a shim under the roadmap's shim-deletion clause, which covers L0–L3 only. The Path.trans concatenation and its Path.extend calculus are consumed from Mathlib rather than rebuilt.

References

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

The family carried along a concatenation

noncomputable def TauCeti.transFamily {Y : Sort u_1} (F G : ↑unitInterval → Y) (u : ↑unitInterval) : Y

The family carried along a concatenation γ.trans δ of paths, assembled from the family F carried along γ and the family G carried along δ: on the first half of the parameter interval it is F, read at twice the parameter, and on the second half it is G, read at twice the parameter minus one. The junction time 1 / 2 is assigned the value coming from F, matching the convention of Path.trans.

Assembling the two halves is pure reparametrisation of the unit interval, so the values are allowed to lie in an arbitrary sort; the case of interest is Y = ℂ → E, where F and G are families of germs (TauCeti.IsAnalyticContinuationAlong.trans).

Equations

• TauCeti.transFamily F G u = if ↑u ≤ 2⁻¹ then F (Set.projIcc 0 1 TauCeti.transFamily._proof_2✝ (2 * ↑u)) else G (Set.projIcc 0 1 TauCeti.transFamily._proof_2✝ (2 * ↑u - 1))

@[simp]

theorem TauCeti.transFamily_of_le_half {Y : Sort u_1} (F G : ↑unitInterval → Y) {u : ↑unitInterval} (hu : ↑u ≤ 2⁻¹) : transFamily F G u = F (Set.projIcc 0 1 ⋯ (2 * ↑u))

On the first half of the parameter interval the concatenated family is the first family.

@[simp]

theorem TauCeti.transFamily_of_half_lt {Y : Sort u_1} (F G : ↑unitInterval → Y) {u : ↑unitInterval} (hu : 2⁻¹ < ↑u) : transFamily F G u = G (Set.projIcc 0 1 ⋯ (2 * ↑u - 1))

Strictly past the junction the concatenated family is the second family.

theorem TauCeti.transFamily_zero {Y : Sort u_1} (F G : ↑unitInterval → Y) : transFamily F G 0 = F 0

At parameter time 0 the concatenated family is the initial value of the first family: a concatenation starts where its first factor starts.

Not itself a simp lemma: simp already reaches this normal form through TauCeti.transFamily_of_le_half, whose bound it discharges at 0.

@[simp]

theorem TauCeti.transFamily_one {Y : Sort u_1} (F G : ↑unitInterval → Y) : transFamily F G 1 = G 1

At parameter time 1 the concatenated family is the terminal value of the second family: a concatenation ends where its second factor ends.

Concatenating continuations

theorem TauCeti.IsAnalyticContinuationAlong.trans {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {a b c : ℂ} {F G : ↑unitInterval → ℂ → E} [CompleteSpace E] {p : Path a b} {q : Path b c} (hF : IsAnalyticContinuationAlong F (⇑p) Set.univ) (hG : IsAnalyticContinuationAlong G (⇑q) Set.univ) (hFG : F 1 =ᶠ[nhds b] G 0) : IsAnalyticContinuationAlong (transFamily F G) (⇑(p.trans q)) Set.univ

Continuations concatenate. If F continues a germ along p, G continues a germ along q, and the germ F delivers at the end of p is the germ G starts from, then TauCeti.transFamily F G is a continuation along the concatenated path p.trans q.

Its germ at parameter time 0 is that of F 0 and its germ at time 1 is that of G 1 (TauCeti.transFamily_zero, TauCeti.transFamily_one), so continuing along p and then along q carries the initial germ of F to the terminal germ of G.

theorem TauCeti.continuesAlong_trans {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {a b c : ℂ} {f₀ : ℂ → E} {F : ↑unitInterval → ℂ → E} [CompleteSpace E] {p : Path a b} {q : Path b c} (hF : IsAnalyticContinuationAlong F (⇑p) Set.univ) (hF0 : F 0 =ᶠ[nhds a] f₀) (hq : ContinuesAlong (F 1) ⇑q) : ContinuesAlong f₀ ⇑(p.trans q)

Continuability is transitive along a concatenation. If F continues the germ of f₀ along p, and the germ F 1 it delivers at the end of p continues along q, then f₀ continues along p.trans q.

Restricting a continuation to the factors of a concatenation

theorem TauCeti.IsAnalyticContinuationAlong.left_of_trans {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {a b c : ℂ} {H : ↑unitInterval → ℂ → E} {p : Path a b} {q : Path b c} (h : IsAnalyticContinuationAlong H (⇑(p.trans q)) Set.univ) : IsAnalyticContinuationAlong (fun (t : ↑unitInterval) => H (Set.projIcc 0 1 ⋯ (↑t / 2))) (⇑p) Set.univ

A continuation along a concatenation restricts to its first factor. Reading a continuation along p.trans q on the first half of the parameter interval — that is, precomposing with the halving map t ↦ t / 2 — gives a continuation along p.

This is the converse of TauCeti.IsAnalyticContinuationAlong.trans, and needs no gluing: the first half of p.trans q is p reparametrised, so TauCeti.IsAnalyticContinuationAlong.reparam transports the continuation.

theorem TauCeti.IsAnalyticContinuationAlong.right_of_trans {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {a b c : ℂ} {H : ↑unitInterval → ℂ → E} {p : Path a b} {q : Path b c} (h : IsAnalyticContinuationAlong H (⇑(p.trans q)) Set.univ) : IsAnalyticContinuationAlong (fun (t : ↑unitInterval) => H (Set.projIcc 0 1 ⋯ ((↑t + 1) / 2))) (⇑q) Set.univ

A continuation along a concatenation restricts to its second factor. Reading a continuation along p.trans q on the second half of the parameter interval — that is, precomposing with t ↦ (t + 1) / 2 — gives a continuation along q.

theorem TauCeti.ContinuesAlong.left_of_trans {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {a b c : ℂ} {f₀ : ℂ → E} {p : Path a b} {q : Path b c} (h : ContinuesAlong f₀ ⇑(p.trans q)) : ContinuesAlong f₀ ⇑p

Continuability restricts to the first factor of a concatenation. A germ that continues along p.trans q continues along p: the germ-level converse of TauCeti.continuesAlong_trans, obtained by restricting a witness with TauCeti.IsAnalyticContinuationAlong.left_of_trans.

There is no companion for the second factor at this level: q issues from the endpoint of p, so the germ it continues is the one reached at the junction, which TauCeti.ContinuesAlong does not name. Use TauCeti.IsAnalyticContinuationAlong.right_of_trans on a witness instead.

Continuability inside a domain travels with the germ

theorem TauCeti.continuesInside_of_isAnalyticContinuationAlong {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {f₀ : ℂ → E} {F : ↑unitInterval → ℂ → E} [CompleteSpace E] {U : Set ℂ} {z₀ z₁ : ℂ} (H : ContinuesInside f₀ U z₀) {p : Path z₀ z₁} (hpU : ∀ (t : ↑unitInterval), p t ∈ U) (hF : IsAnalyticContinuationAlong F (⇑p) Set.univ) (hF0 : F 0 =ᶠ[nhds z₀] f₀) : ContinuesInside (F 1) U z₁

Continuability inside a domain does not depend on the base point. If the germ of f₀ at z₀ continues inside U, and F continues it along a path p from z₀ to z₁ that stays in U, then the germ F 1 delivered at z₁ continues inside U in its own right.

So TauCeti.ContinuesInside, the hypothesis of the monodromy theorem for a simply connected domain, is a condition on the domain and on the branch being carried, not on the point one starts from: a path issuing from z₁ is continued by prefixing p to it, and uniqueness of continuation along p identifies the germ reached halfway with F 1.

theorem TauCeti.continuesInside_iff_of_isAnalyticContinuationAlong {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : ↑unitInterval → ℂ → E} [CompleteSpace E] {U : Set ℂ} {z₀ z₁ : ℂ} {p : Path z₀ z₁} (hpU : ∀ (t : ↑unitInterval), p t ∈ U) (hF : IsAnalyticContinuationAlong F (⇑p) Set.univ) : ContinuesInside (F 1) U z₁ ↔ ContinuesInside (F 0) U z₀

Continuability inside a fixed domain is invariant under base-point transport along an analytic continuation inside that domain. If F continues a germ along a path p of U from z₀ to z₁, then the germ F 1 delivered at z₁ continues inside U exactly when the germ F 0 it started from does.

This strengthens TauCeti.continuesInside_of_isAnalyticContinuationAlong, its ← direction, to an equivalence, and drops the representative f₀ from the statement; the version with a representative is recovered from TauCeti.continuesInside_congr. The → direction transports the base point back along the reversed path p.symm, along which the family read backwards, F ∘ σ, is again a continuation: reversing the parameter is a reparametrisation of the parameter interval by the central symmetry σ, which TauCeti.IsAnalyticContinuationAlong.reparam transports. So neither endpoint of p is distinguished, and any point the branch reaches inside U may serve as the base point of TauCeti.ContinuesInside, the hypothesis of the monodromy theorem for a simply connected domain (Conformal/GlobalBranch.lean).