Montel's theorem: local boundedness is relative compactness

Layer L1 (normal families / Montel) of the conformal-mapping roadmap (TauCetiRoadmap/ConformalMapping/README.md) states its milestone as

locally bounded ⇒ precompact for TendstoLocallyUniformlyOn,

and Conformal/Montel/Basic.lean records the selection consequence: every sequence drawn from a locally bounded family of holomorphic functions has a locally uniformly convergent subsequence. This file isolates the compactness statement that selection consequence rests on, in the space where "precompact" literally means precompact — the space C(↥Ω, E) of continuous maps on the domain with its compact-open topology, whose convergence is locally uniform convergence — and shows that local boundedness is not merely sufficient for it but equivalent to it.

The two directions

A family F : ι → ℂ → E of functions holomorphic on an open Ω restricts to a family f : ι → C(↥Ω, E); the theorems below take that restriction as a hypothesis ⇑(f i) = Ω.domRestrict (F i) rather than fixing one bundling, so that a caller which already carries such an f may use them directly. The hypothesis constrains nothing: a caller holding hF : ∀ i, ContinuousOn (F i) Ω and no f of its own takes fun i => ⟨Ω.domRestrict (F i), (hF i).domRestrict⟩, for which it holds by rfl.

Locally bounded ⇒ relatively compact is Mathlib's compact-open Arzelà–Ascoli framework. The family sits inside the uniform-on-compacts function space as a closed subspace (ContinuousMap.isUniformEmbedding_toUniformOnFunIsCompact together with UniformOnFun.isClosed_setOfPred_continuous), so ArzelaAscoli.isCompact_closure_of_isClosedEmbedding applies: equicontinuity on each compact is TauCeti.IsLocallyBoundedOn.equicontinuousOn, which is Cauchy's estimate, and pointwise relative compactness is local boundedness at a single point. This is the direction with analytic content — holomorphy enters only through the Cauchy estimate behind the equicontinuity.

That pointwise step is also the only place the target matters: a norm bound confines the values to a closed ball, and for the ball to be compact E must be proper. So this direction is stated for a proper E — for a normed space over ℂ that is exactly finite-dimensionality — and the converse, which merely reads a bound off a compact set, for an arbitrary one.

Relatively compact ⇒ locally bounded is a soft argument and needs no holomorphy at all, nor even openness of Ω or a complex domain: it is stated for a set Ω in an arbitrary topological space, because local compactness of the subtype ↥Ω is all it uses. On a compact K ⊆ Ω the product closure (range f) ×ˢ (Subtype.val ⁻¹' K) is compact, local compactness of ↥Ω makes evaluation C(↥Ω, E) × ↥Ω → E continuous in both variables at once, and a continuous real function on a compact set is bounded. The bound obtained is uniform in the index, which is exactly TauCeti.IsLocallyBoundedOn.

Together they give TauCeti.isCompact_closure_range_iff_isLocallyBoundedOn: for a family of holomorphic maps of an open set into a proper E, relative compactness in C(↥Ω, E) and local boundedness are the same condition.

Main results

• TauCeti.isCompact_closure_range_of_isLocallyBoundedOn — a locally bounded family of holomorphic maps of an open set into a proper E is relatively compact in C(↥Ω, E).
• TauCeti.isLocallyBoundedOn_of_isCompact_closure_range — the converse, for any family of maps on a set in a topological space whose subtype is locally compact.
• TauCeti.isCompact_closure_range_iff_isLocallyBoundedOn — the two are equivalent.

Coordination with upstream Mathlib

Per the Coordination with upstream Mathlib section of ConformalMapping/README.md, L0–L3 material overlaps mathlib4#33505, the in-progress human-curated Riemann-mapping-theorem effort, which proves a Montel equicontinuity statement internally as a private lemma. Like Conformal/Montel/Basic.lean, this file is therefore a temporary shim: once the corresponding Mathlib results land, these statements should be backed by them — or deleted and their consumers refactored — rather than maintained as an independent re-proof. What Tau Ceti adds at L1 is named, discoverable API, not first proof.

This is the analytic normal-families theorem; it is deliberately not routed through Mathlib's Analysis/LocallyConvex/Montel.lean (MontelSpace), which is an unrelated notion.

References

• L. Ahlfors, Complex Analysis, Ch. 5 §5.
• J. B. Conway, Functions of One Complex Variable I (GTM 11), Ch. VII §2.

theorem TauCeti.isCompact_closure_range_of_isLocallyBoundedOn {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {Ω : Set ℂ} {F : ι → ℂ → E} {f : ι → C(↑Ω, E)} [ProperSpace E] (hΩ : IsOpen Ω) (hF : ∀ (i : ι), DifferentiableOn ℂ (F i) Ω) (hb : IsLocallyBoundedOn F Ω) (hf : ∀ (i : ι), ⇑(f i) = Ω.domRestrict (F i)) : IsCompact (closure (Set.range f))

Montel's theorem, relative-compactness form. A locally bounded family of holomorphic maps of an open set Ω ⊆ ℂ into a proper complex normed space E restricts to a relatively compact family in the space C(↥Ω, E) of continuous maps with the compact-open topology.

This is the precompactness the roadmap's L1 milestone asks for; TauCeti.montel is the sequential selection statement extracted from it. The local boundedness hypothesis cannot be dropped once E is nontrivial: on a nonempty open Ω the holomorphic family F n z = n • v, for a unit vector v : E, restricts to a closed discrete — hence non-relatively-compact — family. On Ω = ∅, or on the trivial E = 0 where no unit vector exists, the conclusion holds regardless, so there is no counterexample in those two degenerate cases. Properness of E cannot be dropped either: it is what turns the pointwise norm bound into pointwise relative compactness, and for a normed space over ℂ it says exactly that E is finite-dimensional.

theorem TauCeti.isLocallyBoundedOn_of_isCompact_closure_range {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] {X : Type u_3} [TopologicalSpace X] {Ω : Set X} {F : ι → X → E} {f : ι → C(↑Ω, E)} [LocallyCompactSpace ↑Ω] (hf : ∀ (i : ι), ⇑(f i) = Ω.domRestrict (F i)) (hcpt : IsCompact (closure (Set.range f))) : IsLocallyBoundedOn F Ω

The converse of Montel's theorem. A family of maps on a set Ω with locally compact subtype whose restrictions are relatively compact in C(↥Ω, E) is locally bounded on Ω.

No holomorphy is needed — not even a complex domain, nor continuity beyond what the restrictions already carry — and no properness of the target: evaluation is continuous in the map and the point together as soon as ↥Ω is locally compact (for an open Ω ⊆ ℂ the instance is IsOpen.locallyCompactSpace), so a continuous real function on the compact product closure (Set.range f) ×ˢ (Subtype.val ⁻¹' K) is bounded — and its bound is uniform in the index, which is what local boundedness asserts.

theorem TauCeti.isCompact_closure_range_iff_isLocallyBoundedOn {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℂ E] {Ω : Set ℂ} {F : ι → ℂ → E} {f : ι → C(↑Ω, E)} [ProperSpace E] (hΩ : IsOpen Ω) (hF : ∀ (i : ι), DifferentiableOn ℂ (F i) Ω) (hf : ∀ (i : ι), ⇑(f i) = Ω.domRestrict (F i)) : IsCompact (closure (Set.range f)) ↔ IsLocallyBoundedOn F Ω

Montel's theorem as an equivalence. For a family of holomorphic maps of an open set Ω ⊆ ℂ into a proper complex normed space E, being locally bounded on Ω and being relatively compact in C(↥Ω, E) are the same condition.